Formal Verification is catching up with cutting-edge Mathematics
Formalization has trailed cutting-edge mathematics for some time: the four color theorem was proved in 1976, but it wasn't formally verifed until 2005.
This was one of the objections of the QED manifesto in 1993:
Objection 4. Mechanically checked formality is impossible. There is no evidence that extremely hard proofs can be put into formal form in less than some utterly ridiculous amount of work.
Reply to Objection 4. Based upon discussions with numerous workers in automated reasoning, it is our view that using current proof-checking technology, we can, using a variety of systems and expert users of those systems, check mathematics at within a factor of ten, often much better, of the time it takes a skilled mathematician to write down a proof at the level of an advanced undergraduate textbook. (emphasis mine)
Today I got a github notification that prompted me check in on recent discussion around Metamath, and I learned that one of the greatest living mathematicians is formally verifying his work as he develops it:
... when it comes to formalising mathematics in real time, we now have an even more spectacular data point: Terry Tao led a team which formalised the main result in his breakthrough new paper with Gowers, Green and Manners proving Katalin Marton’s polynomial Freiman-Ruzsa conjecture. The 33 page paper was formalised in just three weeks (before the paper had even been submitted)! -- Lean in 2024 | Xena
My notes show I first looked at Lean back in 2015. I'm trying to remember what I didn't like about it... ah yes... it's written in C++ and the logic is kinda hairy.
The logic does have a kernel, which was written up by someone I recognize from the Metamath community:
- Mario Carneiro, 2019. The Type Theory of Lean.
- The Type Theory of Lean - YouTube
In his mm0 work, he calls it a "very strong axiomatic framework".
I tried to read that paper; it's a little over my head. But Lean can export proof objects and there are independent checkers. tc.rs is the core of a rust implementation; it's over 1000 LOC; over 5000 if you count the modules it imports. Compare with the 362 line otter proof checker. The Type Checking in Lean 4 docs are just about my speed, though. Thanks!