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
Independently confirmed the Putnam 2025 score: AxiomProver solved 8 of 12 problems by the competition deadline and the remaining 4 in the following days, for a final 12/12 -- reported as only the sixth perfect Putnam score in 98 years out of over 150,000 attempts (buildmvpfast.com Axiom coverage; corroborated by swimswam.com's reporting on Ken Ono's move to Axiom).
- 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. Parity of k-differentials (Chen-Gendron Conjecture)
Checked directly against the arXiv abstract for 2602.03722 (authors: Dawei Chen, Evan Chen, Kenny Lau, Ken Ono, Jujian Zhang). The paper confirms the Chen-Gendron connection: it proves the number-theoretic hypothesis (the abstract's "Conjecture A.10") that Chen and Gendron's genus-zero/one result depended on, by reformulating it in terms of Jacobi symbols and reducing it to a combinatorial identity plus standard Jacobi-symbol facts -- matching this note's "Key Finding" claim.
| 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. 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. Dead Ends in Square-Free Digit Walks
The density figures are correct (confirmed against the arXiv abstract and HTML for 2602.05095: 1.317e-9 vs. a stochastic-model prediction of ~5.218e-5, a ratio of ~4x10^4). But "previously unsolved" does not hold for this result: per the paper's own comments, after posting the first version the authors learned from K. Soundararajan that the result had already been proven by Mirsky in 1947 -- they had relied on a 2024 paper (Miller et al.) that made no reference to Mirsky and mistakenly took it to represent the state of the art. The authors state they will not submit the paper for publication as a result.
| 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.
Correction: After posting, the authors learned the result was already proven by Mirsky in 1947 – a 2024 paper they had relied on did not cite Mirsky, and they mistook it for the current state of the art. This was not, in fact, a previously unsolved problem; the authors say they will not submit the paper for publication.
2.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
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
Could not find this exact quote in any primary source. Independently found two different, similarly-themed Carina Hong quotes on math as an AI sandbox -- "We see math as a sandbox for reality. If you want to build a world model, it's one of the best places to start." and, per Forbes, "Mathematics is the perfect sandbox for building superintelligence" -- but neither matches "Math is really the great test ground and sandbox for reality" verbatim, and the specific source for this wording was not located.
"Math is really the great test ground and sandbox for reality." - Carina Hong
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