ProofForge Uses AI Agents to Produce Kernel-Verified Lean Proofs

Summary

ProofForge is an AI-agent pipeline for turning mathematical problems into machine-verified Lean 4 and Mathlib proofs. Its workflow surveys a known approach, decomposes the problem into atomic lemmas, has agents prove the pieces, runs an adversarial pass that attempts to refute them, and then formalizes the result until Lean compiles it. The Lean kernel rechecks every proof step; the project says `#print axioms` shows only the standard axioms and that `native_decide` is never used. A failed or incorrect proof therefore does not compile, so acceptance comes from the checker rather than trust in an AI-generated claim. The project reports six pull requests merged into Google DeepMind’s `formal-conjectures` repository. They include an upper-bound proof for Erdős #1084, a proof of the 24-digit fifth unitary perfect number for Erdős #1052, formal statements for the Odd Noncototient Conjecture and Green’s open problem #64, a computer-search-assisted proof of Erdős #885’s k=4 case, and a formal statement linked to an external Lean disproof of Erdős #90. The last item is explicitly not the author’s proof. One further pull request, a faster proof of `isUnitaryPerfect_87360`, remained open when the page was written. The repository contains Lean 4 formalization work only; related repositories use SAT/LRAT certificates or an evolutionary LLM coding pipeline for different Erdős problems, rather than Lean proofs. The canonical versions of most contributions live upstream, while the first two Lean sources are included locally.