Sanexxxx777/ProofForge
AI-agent pipeline producing machine-verified Lean 4 proofs — four PRs merged into Google DeepMind's formal-conjectures - Sanexxxx777/ProofForge
0 stars · 0 forks
README
ProofForge An AI-agent pipeline that produces machine-verified Lean 4 / Mathlib proofs. Agents decompose a problem, prove the pieces, and formalize them in Lean. The Lean kernel rechecks every step: #print axioms shows only the standard axioms, and native_decide is never used. A wrong proof does not compile — so "the AI proved it" is not something you take on trust; the checker either accepts it or it doesn't. Contributions to Google DeepMind's formal-conjectures Six pull requests merged into google-deepmind/formal-conjectures:
PR Problem What it contributes
#4245 Erdős #1084 f₁(n) = n − 1 for unit-distance configurations on a line — the upper bound proved.
#4244 Erdős #1052 The 5th unitary perfect number, 146361946186458562560000 (24 digits), via multiplicativity of the unitary divisor-sum σ*. It was an unproved sorry in the repo.
#4361 Erdős #418 The Odd Noncototient Conjecture stated formally.
#4364 Green's open problems #64 The Ω(p−2)-odd infinitude question formalized.
#6509 Erdős #885 The k = 4 case proved with an explicit witness found by computer search: four numbers whose factor-difference sets share four elements (Bremner 2019, formalized).
#4379 Erdős #90 The statement linked to an external Lean disproof (Boris Alexeev's formalization of OpenAI's 2026 counterexample), closing issue #4229. Not my proof.
One more is open at the time of writing: #4360 (a faster proof of isUnitaryPerfect_87360). All merged proofs are kernel-verified. The Lean sources for the first two are in proofs/; the rest live upstream in the repository they were contributed to. Related Erdős repositories This repo covers Lean 4 formalization only. Two other repos tackle different Erdős problems with different methods:
erdos-computational-bounds — SAT + LRAT certificate and a segmented sieve for Erdős #273, #385, #647 (no Lean, no ML). erdos-openevolve — an evolutionary LLM coding pipeline reproducing a numerical SOTA bound for the minimum overlap problem; not a formal proof.
How it works
Survey — find the known approach for the problem. Decompose — split it into atomic lemmas. Prove + verify — agents prove each piece; an adversarial pass tries to refute it. Formalize — translate to Lean 4 / Mathlib and compile until the kernel accepts it.
Built by Aleksandr Shulgin (@Aleksandr_NFA) · shulgin.is-a.dev License Apache License 2.0, matching google-deepmind/formal-conjectures, where these proofs were contributed and where their canonical versions live. The Lean files in proofs/ carry the upstream copyright header of The Formal Conjectures Authors.