AxiomProver

AxiomProver is an automated theorem-proving system developed by Axiom Math. The company describes it as an autonomous multi-agent system for Lean 4 that translates mathematical tasks into formal statements and generates proof terms checked by Lean. Public information about the system comes mainly from artifact repositories rather than a model card or technical report about the generator itself. Those repositories expose proof source, pinned environments, build instructions, and selected verification metadata, but not AxiomProver's models, training data, prompts, orchestration code, or inference configuration.^[12][13][16]

AxiomProver became publicly associated with Axiom Math's claimed solutions to the 2025 William Lowell Putnam Mathematical Competition, formalizations paired with research papers, the 2026 International Mathematical Olympiad, and an August 2026 formalization of the established bound on recurring small gaps between primes. These projects provide stronger evidence than an informal natural-language answer because their Lean files can be inspected and checked. They do not by themselves verify that the formal statement matches the original problem, that every imported mathematical dependency was proved in the same project, or that the generation process was as autonomous as the publisher describes.^{[2][3][12][13]}

System and access

Axiom Math calls AxiomProver an autonomous multi-agent ensemble theorem prover. The public descriptions do not identify the agents, assign component roles, or explain how they coordinate. Axios separately described an overall workflow in which a natural-language problem is translated into Lean, proved, and checked, but not the ensemble's component-level architecture. The system belongs within AI agents and automated theorem proving, but the available detail is insufficient to reconstruct the ensemble or separate model capability from the surrounding search and verification harness.^[12][13][16]

The generator was not publicly released as of August 19, 2026. The public materials reviewed through that date did not include AxiomProver source code, model checkpoints, model identities, training data, system prompts, a hosted generation API, pricing, or a public evaluation harness. Axiom Math had instead released selected outputs and related infrastructure. This makes the public evidence asymmetric: an outside reviewer can inspect whether a released Lean artifact type-checks in its declared environment, but cannot rerun the original generation process or determine how many unsuccessful attempts preceded a reported success.^{[2][12][13][16]}

Axiom Lean Engine, or AXLE, is a separate public service and client library. Its technical report describes 14 Lean utilities, available through interfaces including an SDK, command-line client, web interface, MCP server, and direct API, for proof verification and source-code manipulation. Its public repository says the service was used in Axiom's research and in AxiomProver workflows. AXLE is therefore part of the surrounding toolchain, not an open release of the AxiomProver generator.^[14][15]

Scroll sideways for more →

Public milestones

The Putnam 2025 repository documents AxiomProver's results on that competition. Axiom Math reported that the system solved eight of the twelve problems by the end of the competition on December 6, 2025, and the remaining four in the following days. The repository lists company-reported generation times, token totals, proof sizes, and SafeVerify instructions for each solution. The sources make clear that four solutions were post-contest; the collection is therefore not a twelve-problem score under one uniform contest-time limit.^[12]

In May 2026, Axios reported that Axiom Math was pairing human-authored mathematical papers with Lean formalizations produced using AxiomProver. The article said Axiom claimed that work had been accepted by five journals and described a workflow in which a natural-language problem is translated into Lean, solved, and checked separately. The journal and autonomy claims in that report came from Axiom and founding mathematician Ken Ono. The reported acceptances concern associated research papers; they are not a standardized evaluation of AxiomProver and do not independently measure its success rate.^[16]

For the July 2026 International Mathematical Olympiad, Axiom Math reported solutions to all six problems and released statement and solution files. Its repository describes the system as an autonomous ensemble and gives company-reported generation times from 24 to 869 minutes. The accompanying metadata also records modeling divergences between several informal questions and their formal encodings. In some determine-the-answer problems, the claimed answer is included in the formal theorem to be proved. Lean can check the proof of that theorem, but the formalization step and the discovery of the answer remain analytically separate.^[13]

These milestones are not directly comparable with one another or with systems such as AlphaProof. They use different problem sets, time rules, model access, formalization policies, dependencies, and verification tooling. A repository containing a complete proof artifact answers whether that artifact can be checked; it does not supply the denominator needed to measure how often the system fails, how much human intervention was available, or how performance changes on a preregistered unseen set.^[12][13][17]

Prime-gaps formalization

On August 18, 2026, Axiom Math announced that AxiomProver and human formalizers had completed a machine-checkable formalization related to the best-known unconditional upper bound on recurring gaps between primes. The public PrimeGapsLib repository had been created four days earlier and was licensed under Apache 2.0. Its README divides the development into mathematical theory, a large numerical certificate, and a library combining the two.^[1][2]

The mathematical result predates AxiomProver. Yitang Zhang's 2013 work established that infinitely many consecutive prime gaps are bounded by a finite constant. James Maynard developed a different sieve approach and obtained a bound of 600. The Polymath8b collaboration then optimized the method to show that the limit inferior of consecutive prime gaps is at most 246. The twin-prime conjecture would require the corresponding value to be 2. A formalization of the 246 result does not improve the bound. It implies that at least one fixed prime-gap size no greater than 246 recurs infinitely often, but it does not identify that size and does not show that 246 itself recurs infinitely often.^[6][7][8]

PrimeGapsLib's main file gives three formulations of the conclusion. The first uses Lean's frequently filter to express arbitrarily late consecutive-prime gaps of at most 246. The second states that the Bombieri-Vinogradov proposition implies arbitrarily large prime pairs whose difference is at most 246. The third states the consecutive-gap result using indices beyond any chosen cutoff. The number is an upper bound, not an assertion that the primes differ by exactly 246. The Lean AI formalization benchmark added a matching prime-pair target on June 21, 2026, before Axiom published PrimeGapsLib.^[4][9]

The project's own metadata gives the result an important qualification. It reports zero sorry placeholders in the main declarations and lists only the standard axioms propext, Classical.choice, and Quot.sound, but it labels its review status self-assessed and records the Bombieri-Vinogradov theorem as a literature dependency. In conventional mathematics, Bombieri-Vinogradov is an established theorem, so using it yields the unconditional 246 conclusion. Within this Lean development, however, the proposition is an antecedent rather than a proof imported from foundational results. PrimeGapsLib is consequently a formalization of the implication and its numerical certificate, not a closed derivation of every analytic-number-theory dependency.^[3][4][6]

The authorship metadata also rules out a purely autonomous interpretation. It says foundational definitions were formalized manually, some definitions autonomously, and most theorems autonomously; it describes the 246 development as collaboration between AxiomProver and human formalizers. The review took place mainly in an internal Axiom repository before the public release. The published files expose the result but do not record a per-declaration provenance trail that would let an outsider assign each step to a human or to the system.^[3]

The pinned public state used Lean 4.33.0-rc1, a fixed Mathlib commit, and a fixed revision of Axiom Math's fork of PrimeNumberTheoremAnd. A GitHub Actions build for the August 18 head completed successfully. The repository also provides a comparator configuration that checks the solution declarations against a self-contained challenge module and restricts permitted axioms. Its README warns that the full comparison may take hours. A successful publisher-hosted continuous-integration run is useful build evidence, but it is not an independent mathematical review or an independently reported full comparator reproduction.^{[2][5][11][18]}

What machine-checkable means

Lean checks whether a proof term has the declared type under the definitions, imported declarations, and accepted axioms in its environment. If the kernel accepts the term and the axiom audit contains only the declared foundations, then each formal inference is justified inside that formal system. This removes many ordinary proof-writing failure modes, such as an unstated algebraic step that does not follow from the hypotheses.^[10]

Kernel checking does not resolve three other questions. First, the formal theorem may not faithfully represent the natural-language problem. Second, an imported declaration or explicit antecedent may carry mathematical work not proved in the local repository. Third, a correct proof can be difficult to read, maintain, or recognize as mathematically explanatory. Axiom's IMO metadata is unusually useful on the first issue because it publishes divergences and modeling choices instead of treating type-checking as a complete semantic audit.^[3][13]

The Lean comparator addresses a narrower integrity problem. A challenge module states the target theorem with an admitted proof, while a solution module imports the completed development. Comparator checks that the declarations align and that the solution does not rely on unpermitted axioms. This helps prevent a project from silently proving an easier statement under the same name. It still depends on the challenge statement being a faithful specification of the intended mathematics.^[2][11]

Formal checking also does not demonstrate that an AI system discovered a result. PrimeGapsLib formalizes published work by Zhang, Maynard, and Polymath rather than a new theorem. Other Axiom projects pair generated formal proofs with new or existing informal mathematics under varying degrees of human contribution. Claims about novelty, autonomy, and attribution therefore require evidence beyond a Lean acceptance result.^{[3][6][7][8][16]}

Evaluation and reception

Independent reporting has treated AxiomProver as part of a broader shift toward AI-assisted research mathematics. Axios documented the system and Axiom's journal strategy, while Quanta described Axiom Math among several organizations developing mathematical AI. Quanta also emphasized a selection problem across the field: public successes can sit among many unreported failures. That caveat is especially relevant when an unreleased system publishes selected solved artifacts without a complete run log or fixed evaluation protocol.^[16][17]

The released repositories offer stronger evidence of individual proof artifacts than screenshots or natural-language claims. They expose source files, dependency versions, stated axioms, and build paths, and several projects include explicit fidelity notes. They provide weaker evidence for aggregate system performance. Company-reported contest scores, token use, wall-clock time, and autonomy cannot be converted into a general success rate without knowing the allowed tools, parallelism, human interventions, unsuccessful samples, formalization policy, and total compute.^[12][13]

AxiomProver also differs from an informal mathematical assistant or AI Co-Mathematician. Its public identity is centered on constructing checkable Lean artifacts. This makes correctness at the formal-proof layer more auditable, while shifting part of the evaluation burden to statement fidelity, dependency review, and provenance. The system's usefulness for professional mathematics cannot be inferred from competition results alone, and its accessibility cannot be inferred from AXLE because the public service provides verification primitives rather than the unreleased generator.^[14][15][17]

Limitations

The public materials reviewed through August 19, 2026 did not include a technical report describing AxiomProver's architecture, component models, training data, search strategy, compute budget, or safety controls. They also did not include a public generator checkpoint or general access program. Public descriptions of an autonomous multi-agent ensemble were consistent across Axiom repositories, but remained publisher descriptions rather than an independently inspected implementation.^[12][13][16]

PrimeGapsLib itself was an evolving, days-old repository at the cutoff. Its main result was self-assessed, conditional in Lean on the Bombieri-Vinogradov proposition, and dependent on pinned external code. The public build and metadata supported the claim that an inspectable formal artifact existed; no independent published line-by-line formal review or full comparator reproduction was identified. These limits do not negate the proof artifact, but they bound claims about completeness, authorship, reproducibility, and the system's general capabilities.^[2][3][5]

References

1. ^Axiom Math. "BGP246 formalization announcement." X, August 18, 2026. x.com/...2089732764279132449
2. ^Axiom Math. "PrimeGapsLib." GitHub, August 2026. github.com/...PrimeGapsLib
3. ^Axiom Math. "PrimeGapsLib formalization metadata." GitHub, commit 1faa7b1, August 18, 2026. github.com/...formalization.yaml
4. ^Axiom Math. "Prime Gaps Bounded by 246." GitHub, commit 1faa7b1, August 18, 2026. github.com/...Bounded246.lean
5. ^Axiom Math. "Lean build for PrimeGapsLib commit 1faa7b1." GitHub Actions, August 18, 2026. github.com/...32171224732
6. ^D. H. J. Polymath. "Variants of the Selberg sieve, and bounded intervals containing many primes." Research in the Mathematical Sciences, 2014. doi.org/...s40687-014-0012-7
7. ^James Maynard. "Small gaps between primes." Annals of Mathematics, 2015. doi.org/...annals.2015.181.1.7
8. ^Yitang Zhang. "Bounded gaps between primes." Annals of Mathematics, 2014. doi.org/...annals.2014.179.3.7
9. ^Lean AI formalization benchmark. "feat: add bounded prime gaps eval problem (Knill §224) (#448)." GitHub, June 21, 2026. github.com/...8bb854b9455ad86a2b22908d32282ebe9fbe
10. ^Lean. "Axioms." Lean Language Reference, accessed August 19, 2026. lean-lang.org/...Axioms
11. ^Lean. "Comparator." GitHub, accessed August 19, 2026. github.com/...comparator
12. ^Axiom Math. "AxiomProver at Putnam 2025." GitHub, 2026. github.com/...Putnam2025
13. ^Axiom Math. "AxiomProver at IMO 2026." GitHub, July 2026. github.com/...IMO2026
14. ^Jimmy Xin et al. "AXLE: A Cloud Infrastructure for Lean 4 Theorem Proving Utilities." arXiv:2606.26442, 2026. arxiv.org/...2606.26442
15. ^Axiom Math. "Axiom Lean Engine." GitHub, accessed August 19, 2026. github.com/...axiom-lean-engine
16. ^Ina Fried. "AI Math startup's proofs land in peer-reviewed journals." Axios, May 26, 2026. axios.com/...axiom-ai-math-journal
17. ^Konstantin Kakaes. "The AI Revolution in Math Has Arrived." Quanta Magazine, April 13, 2026. quantamagazine.org/...in-math-has-arrived-20260413
18. ^Axiom Math. "PrimeGapsLib pinned dependency manifest." GitHub, commit 1faa7b1, August 18, 2026. github.com/...lake-manifest.json