AxiomProver: AI-Generated Mathematical Proofs (2026)
Table of Contents
1. Overview
AxiomProver is an autonomous multi-agent ensemble theorem prover for Lean 4, developed by Axiom Math. In early 2026, it solved four previously unsolved mathematical problems, generating complete formal proofs verified in Lean/Mathlib.
1.1. Key Achievements
- Putnam 2025: Solved all 12 problems (8 during competition, 4 afterward)
- Four Open Conjectures: Solved problems that had stumped mathematicians for years
- Fully Automated: Proofs generated from natural language statements
- Formally Verified: All proofs verified in Lean 4/Mathlib
1.2. Team
- Ken Ono - Founding Mathematician (former STEM Advisor at UVA)
- Carina Hong - CEO (Ono's former student)
- Evan Chen - Research
- Kenny Lau - Research
- Jujian Zhang - Research
2. Published Papers
2.1. 1. Parity of k-differentials (Chen-Gendron Conjecture)
| Field | Value |
|---|---|
| arXiv | 2602.03722 |
| Title | Parity of k-differentials in genus zero and one |
| Conjecture | Chen-Gendron (2021) |
| Lean | 4.26.0 |
| Mathlib | v4.26.0 |
| Repository | AxiomMath/parity-differential |
Background: Mathematicians Dawei Chen and Quentin Gendron were studying differentials in algebraic geometry. Their argument depended on an unsolved number-theoretic formula. Chen met Ken Ono at a conference, and AxiomProver produced a proof overnight.
Key Finding: AxiomProver found a connection between the problem and Jacobi symbols, a 19th-century numerical phenomenon that humans had missed.
2.2. 2. Fel's Conjecture on Syzygies
| Field | Value |
|---|---|
| arXiv | 2602.03716 |
| Title | Fel's Conjecture on Syzygies of Numerical Semigroups |
| Conjecture | Fel (decade-old) |
| Lean | 4.26.0 (estimated) |
| Repository | AxiomMath/fel-polynomial |
Background: Fel's Conjecture concerns syzygies (mathematical expressions where numbers align in algebra). The conjecture involves formulas originally discovered in Ramanujan's notebooks over 100 years ago.
Significance: This proof was generated entirely by AxiomProver with zero human input - a first in mathematical history.
2.3. 3. Dead Ends in Square-Free Digit Walks
| Field | Value |
|---|---|
| arXiv | 2602.05095 |
| Title | Dead ends in square-free digit walks |
| Authors | 21 authors including Chen, Ono |
| Lean | Lean/Mathlib |
Result: The asymptotic density of dead ends in base 10 is ~1.317 x 10-9, roughly 40,000 times smaller than the stochastic independence model predicted.
2.4. 4. Fermat's Last Theorem Techniques
| Field | Value |
|---|---|
| Status | Paper pending (mentioned in Wired article) |
| Topic | Applications of modular forms techniques from FLT |
Note: This fourth paper draws on mathematical tools developed for proving Fermat's Last Theorem. Full details pending publication.
3. Technical Approach
3.1. Architecture
AxiomProver is described as a "multi-agent ensemble" that:
- Accepts natural-language problem statements
- Translates to formal Lean specifications
- Searches for proofs using learned strategies
- Verifies proofs in Lean/Mathlib
- Refines and iterates until verified
3.2. Verification Language
All proofs are formalized in Lean 4 with Mathlib, ensuring:
- Machine-checkable correctness
- No gaps in reasoning
- Reproducible verification
3.3. Differences from AlphaProof
While Google's AlphaProof (2024) demonstrated similar ideas, Axiom claims AxiomProver incorporates "several significant advances and newer techniques."
4. Validation Status
Attempting to verify these proofs on FreeBSD 15.0:
| Paper | Lean Version | FreeBSD Status | Notes |
|---|---|---|---|
| parity-differential | 4.26.0 | Blocked | elan 4.1.2 bug |
| fel-polynomial | TBD | Not attempted | |
| dead-ends | TBD | Not attempted |
4.1. FreeBSD Toolchain Issues
# elan 4.1.2 panics on toolchain install thread 'main' panicked at src/elan-dist/src/manifestation.rs:90:13: internal error: entered unreachable code # lean4 pkg version mismatch pkg: lean4-4.25.2.20251201 binary: Lean (version 4.27.0-pre) required: leanprover/lean4:v4.26.0
See Lean 4.26.0 on FreeBSD 15.0 for detailed workaround attempts.
5. Implications
5.1. For Mathematics
"This is a new paradigm for proving theorems." - Ken Ono
- AI can find connections humans miss
- Formal verification eliminates doubt
- Collaboration between human intuition and AI search
5.2. For Software Engineering
The same techniques can be applied to:
- Code verification: Proving software is provably correct
- Cybersecurity: Verifying code is resilient to certain attacks
- Critical systems: Formal guarantees for safety-critical software
5.3. For AI Research
"Math is really the great test ground and sandbox for reality." - Carina Hong
Mathematical reasoning serves as a benchmark for general AI capabilities.
6. Related Resources
6.1. Axiom Math
6.2. Press Coverage
6.3. Lean/Mathlib
6.4. Related wal.sh Research
7. Appendix: Repository Cloning
# Clone the proof repositories ghq get github.com/AxiomMath/parity-differential ghq get github.com/AxiomMath/fel-polynomial ghq get github.com/leanprover/lean4 ghq get github.com/leanprover/elan
8. Appendix: Proof Snippet (Parity Differential)
From solution.lean:
theorem main_theorem (k : ℕ) (n : ℕ) (hk_ge : 3 ≤ k) (hk_odd : Odd k) (_hn_coprime : Nat.Coprime n k) (_hn1_coprime : Nat.Coprime (n + 1) k) : (countingFunctionN k n : ℤ) = (floorSumF k (n + 1) : ℤ) - (floorSumF k n : ℤ) := by rw [cast_floorSum_diff k n, floorSum_diff_eq_sum k n hk_ge, countingN_eq_sum k n hk_ge hk_odd]
The proof uses:
- Combinatorial rewriting (
countingN_as_sum_over_i) - Indicator function conversion (
floor_term_eq_indicator) - Modular arithmetic properties
- Finset sum manipulation