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

https://www.cmu.edu/news/stories/archives/2021/september/hoskinson-center-for-formal-mathematics.html

by calstad • 5 years ago

31 4 5 years ago

cmu.edu

system2• 5 years ago

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

Jxl180• 5 years ago

Is there a center for casual math?

angelzen• 5 years ago

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

qualudeheart• 5 years ago

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

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

Related Stories