# ProofForge

An AI-agent pipeline that decomposes a mathematics problem, proves each piece, and formalizes the result in Lean 4 and Mathlib until the Lean kernel accepts it, with six of its proofs already merged into Google DeepMind's formal-conjectures repository.

ProofForge is an AI-agent pipeline that produces machine-verified Lean 4 and Mathlib proofs. Agents decompose a problem into atomic lemmas, attempt to prove each piece, run an adversarial pass that tries to refute the attempted proof, and then formalize the accepted result in Lean, so that a wrong proof simply fails to compile rather than being taken on trust; the project notes that the Lean kernel's own axiom check shows only standard axioms and that a shortcut tactic which can bypass real verification is never used.

Six pull requests produced this way have been merged into Google DeepMind's formal-conjectures repository, covering specific results such as a proved upper bound for an Erdos problem on unit-distance configurations and the formal statement of an open conjecture, with the Lean sources for two of them kept in this repository and the rest living upstream where they were contributed. A separate, related repository in the same series tackles other Erdos problems with SAT solving and a segmented sieve instead of Lean.

Website: https://shulgin.is-a.dev