Carnegie Mellon Receives $20M to Establish Hoskinson Center for Formal Math

I love seeing coin money used for something good other than buzz.

Hoskinson has announced doing this for a while now. Good to see he’s delivered.

Is there a center for casual math?

> "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.