> "formal mathematics" works on mathematical theorems and proofs after they are stated in a formal language, which in turn allows us to develop computer programs to assist in discovering proofs, verifying the steps humans enter, and certifying the correctness of any proof that can be so formalized.

Pretty much every math center ever have been doing 'casual math'. Formal math is specifically about using formal proof assistants extensivelly. Such an approach traditionally has been seen as too tedious and time consuming for most serious mathematicians.

Thinks pseudocode vs. actual working implementation.