LeanDojoChatGPT VS set.mm

Check out this paper:

https://leandojo.org/

People have already trained models to assist suggestion tactics. They then linked it up to ChatGPT to interactively solve proofs.

In this scenario, ChatGPT asks the model for tactic suggestions, applies it to the proof and uses the feedback from Lean to then proceed with the next step.

FYI, The programmatic interface to Lean was written by an OpenAI employee who was on the Lean team a few years ago.

Also, check out Lean’s roadmap. They aspire to position Lean to becoming a target for LLMs because it has been designed for verification from the ground up.

As math and compsci nerds contribute to mathlib, all of those proofs are also building up a huge corpus that will likely be leveraged for both verification and optimization.

If AI can make verification a lot easier, then we’re likely going to see verification change programming similarly to the way it changed electronics.

Good questions!

Nowadays, there is indeed a movement towards interoperability between the various proof assistants, one of these bridge-building projects is called Dedukti: https://deducteam.github.io/ It's a challenging project because the different proof assistants which are currently in use differ in their foundational perspectives and their idioms. The question how to best formalize mathematics is still an open research problem, just as the question how to best develop programs, but we already have quite a good understanding of many important issues in this area.

Also, by now there are attempts to use AI for discovering proofs, see for instance https://leandojo.org/ or https://github.com/lean-dojo/LeanDojoChatGPT.

Correct. The good news that Elements still works otherwise, you just need to add the missing axiom.

But many other "proofs" have been found to be false. The book "Metamath: A Computer Language for Mathematical Proofs" (by Norm Megill and yours truly) is available at: https://us.metamath.org/downloads/metamath.pdf - see section 1.2.2, "Trusting the Mathematician". We list just a few of the many examples of proofs that weren't.

Sure, there can be bugs in programs, but there are ways to counter such bugs that give FAR more confidence than can be afforded to humans. Lean's approach is to have a small kernel, and then review the kernel. Metamath is even more serious; the Metamath approach is to have an extremely small language, and then re-implement it many times (so that a bug is unlikely to be reproduced in all implementations). The most popular Metamath database is "set.mm", which uses classical logical logic and ZFC. Every change is verified by 5 different verifiers in 5 different programming languages originally developed by 5 different people:

* metamath.exe aka Cmetamath (the original C verifier by Norman Megill)

* checkmm (a C++ verifier by Eric Schmidt)

* smetamath-rs (smm3) (a Rust verifier by Stefan O'Rear)

* mmj2 (a Java verifier by Mel L. O'Cat and Mario Carneiro)

* mmverify.py (a Python verifier by Raph Levien)

For more on these verifiers, see: https://github.com/metamath/set.mm/blob/develop/verifiers.md