The proofs themselves appear to have been checked using the Lean programming language. Before editing my previous post, I confirmed that both of the specific proofs I mentioned have been checked using Lean, and that the Lean source code for those proofs is freely available at github. There does not appear to be a great of doubt concerning the correctness of these AI-generated and Lean-checked proofs.
Automatic theorem proving is a classical area of artificial intelligence. In 1975, I graded for a course in automatic theorem proving taught by
Woody Bledsoe. Several of Bledsoe's graduate students advanced the state of the art. One of those students, Robert S Boyer, collaborated with
J Strother Moore to develop the Boyer-Moore theorem prover, which Moore and his team turned into the
ACL2 prover that (in 1995) was used to prove the correctness of floating point division in the AMD K5 microprocessor.
Lean 4 is both a functional programming language and a proof assistant. It was developed by
Leonardo de Moura, building on the work of previous researchers and systems, notably Coq (now Rocq). Last year, de Moura and three other developers of Lean received
ACM SIGPLAN's Programming Languages Software Award.
Without getting into the
P=NP question, let's just stipulate the intuitively obvious fact that proof checking is easier than finding a correct proof from scratch. In 1929, however,
Kurt Gödel proved his
completeness theorem, which asserts the existence of an algorithm capable of proving any valid statement of first order logic. One way to prove that completeness theorem is to describe a specific algorithm that does so. Here is one such algorithm:
- Start a process that enumerates all possible sequences of Unicode characters. (That process, left to itself, will never terminate.)
- Interrupt that process after each enumerated sequence of characters, and check to see whether that sequence of characters is a proof of the statement you're trying to prove.
- If it is, you've found a proof. Otherwise you keep looking.
As a corollary of Gödel's completeness theorem, it is possible to write a computer program that will find a proof of any
correct valid statement of any recursively axiomatizable first order theory.
Which is not to say the computer program will find a proof quickly, even when a proof exists. If the thing you're trying to prove isn't valid, then there is no proof, and the computer program might run forever.
So proof checking is computationally feasible, but complete proof procedures may not be.
There is a middle ground, known as a proof assistant. A proof assistant assists mathematicians by checking parts of a proof, and by proving things that a human would find tedious to prove, but the proof assistant probably can't prove significant results without guidance from a mathematician (or AI model) in the form of a suggested proof outline.
Lean 4 is a functional programming language, a proof checker, and a proof assistant. You can write computer programs in Lean 4, just as you can write programs in languages such as Haskell or the functional subset of Scheme. As a proof checker, you can ask it to check your proofs. As a proof assistant, it can help you to come up with those proofs.
Lean 4 can check any proof expressed using first order logic, and can venture beyond first order logic into
dependent type theory and a subset of
second order logic. Second order logic is inherently problematic, however; for one thing, there is no analogue of Gödel's completeness theorem for second order logic; even worse, there is no fully general algorithm for checking the correctness of proofs expressed using second order logic.
Anyway, I hope my remarks above will help to explain why mathematicians have a fair degree of confidence in proofs generated by AI and fully checked by Lean 4.
