Axiom Math

Axiom Math develops AxiomProver, an autonomous theorem-proving system, and AXLE, cloud infrastructure for manipulating and verifying Lean proofs. Its work centers on AI-generated reasoning that can be formally checked. In March 2026, the company raised a $200 million Series A to extend its formal mathematics work into what it calls “Verified AI,” applying provable correctness to code, cryptography, and quantitative finance.[3][4][2]

CEO Carina Hong describes verification as “scaling brilliance, compounding brilliance” in a June 2026 Latent Space interview article. The approach uses Lean to check meticulously specified proofs, providing a correctness signal for training and results that later inference and training can build upon. Its practical qualification is specification: a checked proof must still express the problem people intended to solve.[1]

That expansion followed Axiom’s emergence from stealth in October 2025 and its subsequent work on competition mathematics and an open conjecture.[2][3][6]

Axiom emerged from stealth with a foundational team assembled across Meta FAIR, Google Brain, and DeepMind. Its fundraising record dates a $64 million seed round at a $300 million valuation to October 2025; it does not label that valuation as pre-money or post-money.[2]

At Putnam 2025, AxiomProver solved eight of twelve problems by the end of the December 6 competition, then solved the remaining four in the following days. The eventual 12/12 result therefore includes work completed after the competition. The released solutions identify the system as an autonomous multi-agent ensemble theorem prover for Lean 4.21.0 and include proof sources, graphs, and a SafeVerify verification command under an MIT license.[3]

Problem A5 illustrates the size and generation requirements of one released formal proof. Axiom reports 518 prover minutes and 9.1 million tokens for a 2,054-line proof containing 52 theorems and 3,074 tactics. A5 was among the solutions found after the competition.[3]

The Putnam release credits Chris Cummins and GasStationManager as prover leads. Engineering contributors were Dejan Grubisic, Leopold Haller, Andranik Kurghinyan, Aram Markosyan, Manooshree Patel, Gaurang Pendharkar, Vedant Rathi, Alex Schneidman, Volker Seeker, Ishan Sinha, and Jimmy Xin. Mathematics contributors were Evan Chen, Ben Eltschig, Kenny Lau, Ken Ono, and Jujian Zhang; leadership credits went to Carina Hong, Hugh Leather, and Shubho Sengupta.[3]

The collaborative paper “Fel’s Conjecture on Syzygies of Numerical Semigroups”, first submitted February 3, 2026 and revised June 15, describes a proof using exponential generating functions and coefficient extraction. Its authors report that AxiomProver produced the argument automatically from a natural-language statement of the conjecture and that the argument is fully formalized in Lean/Mathlib.[6]

Axiom’s funding record dates its $200 million Series A at a $1.6 billion-plus post-money valuation to March 2026. The company described the financing as supporting an extension from formal mathematics into verified code, cryptography, and quantitative finance—a stated development direction rather than a claim of completed commercial offerings.[2]

AXLE (Axiom Lean Engine) supplies the infrastructure behind Axiom’s proving efforts, including its Putnam work. The June 24, 2026 paper, by Jimmy Xin, Alex Schneidman, Chris Cummins, Karun Ram, Srihari Ganesh, and Jannis Limperg, describes fourteen Lean 4 tools covering strict proof verification, declaration metadata extraction, semantic source manipulation, deterministic proof repair and simplification, and lemma extraction.[4]

AXLE runs as a multi-tenant cloud service with per-request isolation and concurrent support for multiple Lean 4 and Mathlib versions. It offers a Python SDK, command-line interface, web interface, MCP server, and HTTP API. At the paper’s June 2026 submission, the authors described it as publicly available and free, without a local Lean installation, and reported over 500 million cumulative requests. That count includes Axiom’s proving workloads; it measures infrastructure use rather than unique users or paying customers.[4]

Axplorer combines neural learning with classical search. It generates and scores valid examples, retains the best, and trains a decoder-only transformer on them. The model samples new mathematical objects; local search repairs constraint violations and can improve valid samples. The highest-scoring examples become the next epoch’s training data. When sampling produces too many duplicates, the pipeline increases temperature to encourage exploration.[5]

Axplorer’s implemented environments seek graphs without four-cycles, grid point sets without isosceles triangles, and three-dimensional grid point sets with no five points on a sphere. The Apache-2.0 repository credits François Charton, Jordan S. Ellenberg, Adam Zsolt Wagner, and Geordie Williamson for the original PatternBoost code.[5]

In a June 3, 2026 Latent Space interview article, Hong reported a 99% (187/189) result on Verina ProofGen, a task requiring both generated code and a proof of correctness.[1]