April Fool's Day

Stream: Machine Learning for Theorem Proving

[Leonardo de Moura]

I asked ChatGPT to create an April Fool's Day post about Lean. Here is the output.

---

Sure, here's a post for April Fool's Day about the Lean proof assistant:

Introducing Lean 5.0: The Self-Proving Proof Assistant

The Lean proof assistant has long been the tool of choice for mathematicians and computer scientists looking to formally verify their proofs. But what if Lean could take things one step further and actually prove the correctness of its own proofs?

We're excited to announce the release of Lean 5.0, the self-proving proof assistant. With this new version of Lean, not only can you write and verify your own proofs, but Lean itself will automatically generate and verify proofs of its own correctness.

How does it work? The secret is in the Lean neural network, which has been trained on millions of lines of Lean code to recognize and verify the correctness of patterns in Lean proofs. When you write a proof in Lean 5.0, the neural network springs into action, generating its own proof of correctness and checking it against yours. If the neural network's proof matches yours, you can be confident that your proof is correct, and that Lean itself is working as intended.

But that's not all! Lean 5.0 also includes a new "proof simplification" feature, which automatically simplifies complex proofs into simpler ones. Just click the "simplify proof" button, and Lean will do the rest. And for those times when you're feeling stuck, Lean 5.0 now includes a "proof suggestion" feature, which suggests possible next steps in your proof based on the patterns it has learned from its vast database of Lean proofs.

So why wait? Try Lean 5.0 today, and experience the future of proof assistants. Because in the world of formal verification, it's not enough to be confident in your proofs – you should be confident in your proof assistant too.

[Junyan Xu]

MM0 vibes :)

The goal of this project is to build a formally verified (in MM0) verifier for MM0, down to the hardware, to build a strong trust base on which to build verifiers for more mainstream languages or other verified programs.

"Proof simplification" reminds me of Venkatesh's Aleph Zero essay, which contains an analysis of the impact of mechanization on mathematics (see picture below). AFAIK This essay hasn't be discussed here, but it was the theme of the 2022 Fields Medal Symposium, which Kevin Buzzard co-organized and where Johan Commelin gave a talk (I learned about the symposium because Leo mentioned Johan's talk in his IPAM talk); Michael Harris collected participants' impressions here. The symposium was pre-ChatGPT, and now, 5 months later, people are already discussing the impact of AI on humanity, not just mathematics.
image.png