Axiom Math

Axiom Math, which also calls itself Axiom, is an American artificial intelligence company that builds systems for writing mathematical proofs in Lean, a proof language in which a computer checks every step of an argument.^[1][2] Carina Hong founded it in 2025 after leaving graduate study at Stanford University, and its chief technology officer is Shubho Sengupta, formerly a researcher at Meta FAIR.^[3][4] The company is based in Palo Alto, California.^[3] Its prover, AxiomProver, is the system behind the company's reported results on the 2025 Putnam competition and the 2026 International Mathematical Olympiad and behind a series of papers on open research problems, and it contributed to a Lean formalization of the 246 bound on recurring gaps between primes.^[5][6][7][8] Axiom says it wants to carry formally verified reasoning beyond mathematics into code, cryptography and quantitative finance, an aim it calls "Verified AI".^[9] It raised a $64 million seed round led by B Capital in 2025 and a $200 million Series A led by Menlo Ventures in March 2026, which Menlo said valued the company at $1.6 billion post-money.^[3][10]

Overview

History

Founding

Hong, a mathematician who grew up in Guangzhou, China, was a Stanford PhD student when she met Sengupta, then an AI researcher at Meta, at a coffee shop near the Stanford campus. Forbes reported that the two talked for hours about AI and mathematics, and that Hong left Stanford soon afterward to start the company.^[3] Forbes and Business Insider both reported that she founded Axiom Math in March 2025, while Menlo Ventures later wrote that the company "started operating in July 2025".^[3][4][10] Business Insider described Sengupta as the company's first member, and SiliconANGLE described the two of them as co-founders.^[4][14]

Early hiring drew heavily on Meta's Fundamental AI Research lab. When its seed round became public, Axiom had 10 full-time employees, most of them from Meta, according to Forbes; they included François Charton, Aram Markosyan and Hugh Leather.^[3] Hong told Business Insider that she had focused some of her early recruiting on FAIR because "they consistently deliver amazing research work".^[4]

Seed round

Axiom's seed round became public on September 30, 2025. Forbes reported that the company had raised $64 million in a round led by B Capital, with Greycroft, Madrona and Menlo Ventures participating, at a valuation of $300 million.^[3] SiliconANGLE, which gave the company's legal name as Axiom Quant Inc., described the announcement as the company coming out of stealth.^[14] B Capital partner Yan-David Erlich joined the board and Ida Girma became a board observer.^[15] Axiom's own fundraising page lists the round under October 2025 and says the founding team came from Meta FAIR, Google Brain and DeepMind.^[9]

In early December 2025, Business Insider, citing the Wall Street Journal, reported that Hong had hired Ken Ono, a number theorist at the University of Virginia who had mentored her when she was an undergraduate.^[4][13][16] Accounts of Ono's status at Virginia differ: Quanta Magazine described a leave of absence, while Menlo Ventures wrote that he had resigned a tenured professorship and his post as vice provost.^[17][10] By then Axiom had 17 employees and had said it solved two Erdős problems, according to Business Insider.^[4]

Putnam 2025 and the first research papers

On December 6, 2025, Axiom ran AxiomProver on the William Lowell Putnam Mathematical Competition, receiving the problems section by section from a Putnam proctor as the exam went on.^[18] The company reported that the system had produced Lean proofs for 8 of the 12 problems by the end of the exam and for the other 4 in the following days. It released all 12 proofs on GitHub, together with the generation time and token count for each.^[18][5] Axiom and its investors later described the result as a perfect 12/12 score, and Menlo wrote that only five humans had ever achieved a perfect Putnam score.^[9][10][19]

In February 2026 Axiom posted papers on several open problems for which AxiomProver had produced proofs, and Wired described four of them.^[7] In one case, Wired reported, the mathematician Dawei Chen described to Ono at a conference reception a number-theoretic formula that he and Quentin Gendron had been unable to prove, and Ono presented him with a proof from AxiomProver the next morning.^[7] The resulting paper says the proof was obtained by AxiomProver, which also formalized the combinatorial identity at its core in Lean and Mathlib.^[20] A second paper proved a conjecture of Fel on syzygies of numerical semigroups, and states that the argument "was produced automatically by AxiomProver from a natural-language statement of the conjecture".^[21] Axiom's account of that experiment says that after kickoff the team did not steer the prover with hints, add helper lemmas or patch the Lean proof by hand.^[2] A third, "Almost all primes are partially regular", proved a density-one form of a partial Vandiver theorem; Hong wrote that its "main engine" was proved and formalized autonomously by AxiomProver from a natural-language statement.^[22][23]

Series A and "Verified AI"

On March 12, 2026, Axiom announced a $200 million Series A led by Menlo Ventures. Menlo partner Matt Kraning wrote that the round valued Axiom at $1.6 billion post-money and that he was joining the board, while Hong described the valuation as "$1.6 billion+".^[10][24] Axiom lists Greycroft, Madrona, B Capital, Toyota Ventures and Triatomic Capital as participants, and Hong thanked investors from all five firms as existing backers who had "doubled down".^[9][24] Axios later summarized the round, citing the company, as $200 million at a $1.6 billion valuation.^[25]

The round came with a change of emphasis from mathematics alone toward software. Axiom said it raised the money to extend its lead in formal mathematics "into Verified AI", applying provable correctness to code, cryptography and quantitative finance.^[9] Kraning's announcement argued that AI-generated code is not verified and that Lean-checked outputs could guarantee both correctness and safety properties. It also asserted that Axiom had generated "many orders of magnitude more formally verified data than all previously available human-produced sources combined" and had seen early signs of transfer to software verification; these are the investor's statements rather than published results.^[10] Menlo said the money would pay for hiring, larger training runs on verified proofs and verified software, and the company's first products, and that Axiom then had more than 30 employees.^[10]

The same month, Axiom opened its Lean verification service, AXLE, to the public as a free service and released Axplorer as open-source software.^[26][27]

Journals, economics and IMO 2026

In May 2026 Axiom told Axios that proofs produced by its system, paired with human-written papers, had been accepted by five journals, and that it had more papers under review, eight on arXiv and six more in preparation.^[25] Published examples include the Fel's conjecture paper in the Journal of Combinatorial Theory, Series A, the partial-regularity paper in Archiv der Mathematik, and a paper showing that the abc conjecture implies that Ramanujan's tau function misses almost all primes, in Indagationes Mathematicae.^[21][22][28] Ono told Axios that the company was "focused on producing journal mathematics in which human-readable proofs are paired with machine-checkable Lean formalizations and proofs produced by AxiomProver".^[25]

In June 2026 Fortune reported that Axiom was building EconLib, a planned public library of formally verified economic theory, modeled on Mathlib and co-led by Harvard Business School professor Scott Kominers with Axiom's team.^[13] Its first public result was a formalization of Robert Aumann's 1976 agreement theorem; Kominers told Fortune that the work showed the original proof "was implicitly relying on more than people realized".^[13] The accompanying code repository holds AxiomProver's inputs and outputs alongside a "final hand-cleaned formalisation" of the theorem.^[29] Fortune also reported that Axiom then had 40 people and had customers in fields such as finance, cybersecurity, and software and hardware development, which it gave access to its AI systems and formal verification infrastructure.^[13]

For the 2026 International Mathematical Olympiad, held in Shanghai on July 15 and 16, Axiom reported that AxiomProver solved all six problems, and its repository calls this "a perfect score of 42/42".^[6] The score is the company's own assessment. The repository's fidelity notes say that for three of the problems that ask the solver to determine an answer, the answer is "baked into the statement rather than left to be produced", so the formal statement "presupposes the solution".^[30]

Prime gaps and later work

In August 2026 Axiom published PrimeGapsLib, a Lean library whose flagship result is that the Bombieri-Vinogradov theorem implies there are infinitely many pairs of primes separated by no more than 246.^[31][8] The bound of 246 was obtained by the Polymath8b collaboration after Yitang Zhang's 2013 bounded-gaps theorem and James Maynard's bound of 600.^[32] The project metadata says the proof "was generated collaboratively between human formalisers at Axiom Math and AxiomProver" and lists the library's review status as self-assessed; Bombieri-Vinogradov enters as a hypothesis rather than a proved result.^[8] IEEE Spectrum quoted Ono describing the theorem as "the threshold of human knowledge about prime numbers" and presenting proof formalization as a test bed for verifying AI-written code.^[32]

By late October 2026, Axiom's publications page listed 30 papers and preprints.^[33] One October preprint, deposited on the Hexagon repository by Axiom mathematician Kenny Lau, refines a construction by Lech Mazur to give an explicit positive density of integers that reach 1 quickly under the Collatz map; the preprint says AxiomProver "autonomously produced the mathematics in this paper and formalized it in Lean".^[34][5] Hexagon states that it does not perform peer review.^[35]

People

Hong graduated from MIT in 2022 with a double major in mathematics and physics and was president of its Undergraduate Mathematics Association.^[36][3] She received the Association for Women in Mathematics' 2022 Alice T. Schafer Prize and the 2023 AMS-MAA-SIAM Frank and Brennie Morgan Prize, the latter for results in combinatorics, number theory and probability.^[16][36] Her undergraduate research included a Research Experiences for Undergraduates program at Virginia, and in her Schafer Prize statement she thanked Ono for helping her realize her potential.^[16] She then studied at Oxford as a Rhodes Scholar for China, where Forbes reported she earned a master's degree in computational neuroscience.^[36][3] Menlo wrote that she left a Stanford JD/PhD program in mathematics, where she was a Knight-Hennessy scholar, in her first year.^[10] In January 2025, while still a Stanford PhD student, she said publicly that six mathematicians who had contributed significantly to the FrontierMath benchmark told her they had not known that OpenAI would have exclusive access to it, part of wider criticism of Epoch AI for waiting to disclose OpenAI's funding of the benchmark.^[38]

Sengupta's speaker biography says he worked on deep learning for about ten years, first at Baidu's Silicon Valley AI Lab and then at Meta's FAIR lab, on speech models, large reinforcement learning models for playing Go, scaling model training and using language models to build automated software systems, after a decade developing parallel algorithms for general-purpose GPU programming.^[37] B Capital wrote that he led the FAIR teams that built OpenGo and CrypTen, and Menlo described him as a former FAIR research director.^[15][10]

Charton began applying machine learning to mathematics in 2019, according to Quanta.^[17] That year he and Guillaume Lample published "Deep Learning for Symbolic Mathematics", which trained sequence-to-sequence models to do symbolic integration and solve differential equations.^[39] He later co-authored work on using transformers to find Lyapunov functions and the PatternBoost construction-search method, which found a counterexample to a conjecture that had been open for 30 years.^[40][41] Leather co-authored Meta's LLM Compiler paper with Chris Cummins, Volker Seeker and Dejan Grubisic, among others; all three are listed on Axiom's Putnam team, with Cummins as a prover lead.^[42][5] The same team list names Evan Chen, Ben Eltschig, Kenny Lau, Ono and Jujian Zhang as its mathematicians.^[5]

Technology

Approach

Axiom's mission statement describes the goal as an AI mathematician, a reasoning engine capable of mathematical discoveries "at scales and speed previously unimaginable".^[1] The company compares autoformalization, the translation of natural-language mathematics into Lean, to a compiler for natural language, and says it wants the process to run in both directions, with "autoinformalization" turning formal proofs back into human intuition.^[1] It argues that formal verifiers such as Lean "provide perfect ground truth" while model judges fail on genuinely novel proofs, and that "verification gives us efficiently scalable rewards for learning".^[1] The long-term design it describes is a loop between a conjecturer, which proposes new statements, and a prover, which settles them, with both successes and failures feeding a growing formal knowledge base; Axiom calls this "the AlphaGo for mathematics, but with infinite branching".^[1]

AxiomProver

Axiom describes AxiomProver as "an autonomous multi-agent ensemble theorem prover for Lean 4".^[6] Given a conjecture in natural mathematical language together with the relevant definitions, it generates a proof in Lean and Mathlib, and a result is accepted only once the Lean checker accepts it.^[2] The system is in-house: Axiom publishes its outputs as Lean repositories on GitHub, and its January 2026 Putnam post said that a technical report on the prover would follow.^[2][5][18] The separate AxiomProver article discusses the public evidence about the system and its limits.

AXLE

The Axiom Lean Engine (AXLE) is a hosted service for checking and manipulating Lean proofs at scale, with tools such as verify_proof and extract_decls.^[26] Axiom said it had served millions of requests internally, including for training its models, the Putnam run and its work on open conjectures, before the public release on March 5, 2026.^[26] A June 2026 technical report describes 14 Lean 4 tools run as a multi-tenant cloud service with per-request isolation and support for several Lean and Mathlib versions.^[43] Axiom also publishes an MCP server for AXLE. AXLE version 1.9.0, released on October 14, 2026, added environments for CSLib, Physlib and PrimeGapsLib.^[44]

Discovery work and Axplorer

Alongside the prover team, Axiom has a mathematical discovery team that searches for new mathematical objects, such as exceptional graphs or matrices, and connects them back to formal proofs.^[45] Its first public tool is Axplorer, an open-source implementation of PatternBoost that alternates between training a transformer on good candidate constructions and repairing new samples with local search.^[27][41] Axiom reported that on the problem of placing as many edges as possible in a 33-vertex graph without a four-cycle, Axplorer found what it called the optimal solution in 2.5 hours on a single L4 GPU after 2.6 million candidates, where the original PatternBoost run had needed 116.5 million.^[27] Charton also co-authored a November 2025 study of how transformers learn the Collatz sequence, which Axiom lists among its publications.^[46][33]

Funding

The two disclosed rounds total $264 million. Axiom's fundraising page listed no later round as of October 27, 2026.^[9]

Reception and caveats

Wired quoted Kominers, who was familiar with Axiom's technology, calling the autonomous Fel's conjecture proof "pretty astounding"; Fortune later reported that he co-leads EconLib with Axiom's team.^[7][13] Quanta Magazine listed Axiom among the math-focused AI startups that have drawn mathematicians out of academia, alongside Harmonic, Logical Intelligence and Math Inc.^[17] In the same article, Terence Tao cautioned about AI in mathematics generally that models were achieving "scattered successes among a big sea of unreported failures".^[17]

On EconLib, Brian Albrecht, an economist at the International Center for Law and Economics, told Fortune that the major antitrust disputes are not about proving results inside a model, and that there is "just no way around needing different people to approve and verify" new results.^[13]

Several of Axiom's headline results carry qualifications set out in its own materials. Four of the 12 Putnam proofs came after the exam ended.^[5] The IMO score is self-assessed, and three of the formal statements contain their answers.^[30] PrimeGapsLib proves the 246 bound conditional on the Bombieri-Vinogradov theorem, and its review status is self-assessed.^[8] The degree of human involvement also varies from project to project: Axiom described the Fel's conjecture proof as produced with no human steering, the prime-gaps proof as a collaboration with human formalizers, and the published Aumann formalization as hand-cleaned.^[2][8][29]

See also

• AxiomProver
• Lean (Theorem Prover)
• Mathlib
• Automated Theorem Proving
• AlphaProof
• Harmonic (AI)
• Math Inc and Gauss
• List of neolabs
• Neolab

References

1. ^1 ^2 ^3 ^4 ^5Axiom Math, "Mission", company website, accessed October 27, 2026.
2. ^1 ^2 ^3 ^4 ^5Axiom Math, "Proof of Concept", February 5, 2026.
3. ^1 ^2 ^3 ^4 ^5 ^6 ^7 ^8 ^9 ^10 ^11 ^12 ^13 ^14 ^15 ^16Rashi Shrivastava, "Meet The Stanford Dropout Building An AI To Solve Math's Hardest Problems, And Create Harder Ones", Forbes, September 30, 2025.
4. ^1 ^2 ^3 ^4 ^5 ^6 ^7Geoff Weiss, "How a Stanford dropout lured top Meta AI researchers to startup Axiom", Business Insider, December 6, 2025.
5. ^1 ^2 ^3 ^4 ^5 ^6 ^7Axiom Math, "AxiomProver at Putnam 2025", GitHub repository, accessed October 27, 2026.
6. ^1 ^2 ^3 ^4Axiom Math, "AxiomProver at IMO 2026", GitHub repository, July 2026.
7. ^1 ^2 ^3 ^4Will Knight, "A New AI Math Startup Just Cracked 4 Previously Unsolved Problems", Wired, February 4, 2026.
8. ^1 ^2 ^3 ^4 ^5Axiom Math, "PrimeGapsLib formalization.yaml", GitHub, August 2026.
9. ^1 ^2 ^3 ^4 ^5 ^6 ^7 ^8 ^9 ^10Axiom Math, "Fundraising", company website, accessed October 27, 2026.
10. ^1 ^2 ^3 ^4 ^5 ^6 ^7 ^8 ^9 ^10 ^11 ^12 ^13 ^14 ^15Matt Kraning, "AI Will Write All the Code. Mathematics Will Prove It Works.", Menlo Ventures, March 12, 2026.
11. ^Axiom Math, "Member of Technical Staff", careers page, accessed October 27, 2026.
12. ^Axiom Math, "Engineering", company website, accessed October 27, 2026.
13. ^1 ^2 ^3 ^4 ^5 ^6 ^7Nick Lichtenberg, "Exclusive: Economists have been teaching an unproven proof for 50 years. AI just solved it", Fortune, June 1, 2026.
14. ^1 ^2Mike Wheatley, "AI startup Axiom gets $64M to develop new knowledge with advanced mathematics", SiliconANGLE, October 2, 2025.
15. ^1 ^2Ida Girma and Yan-David Erlich, "Toward Mathematical Superintelligence: Why We Invested in Axiom", B Capital, September 30, 2025.
16. ^1 ^2 ^3 ^4Association for Women in Mathematics, "Schafer Prize 2022", accessed October 27, 2026.
17. ^1 ^2 ^3 ^4 ^5Konstantin Kakaes, "The AI Revolution in Math Has Arrived", Quanta Magazine, April 13, 2026.
18. ^1 ^2 ^3Axiom Math, "From Seeing Why to Checking Everything", January 8, 2026.
19. ^Mike Wheatley, "Verifiable AI startup Axiom raises $200M to prove AI-generated code is safe to use", SiliconANGLE, March 2026.
20. ^Dawei Chen, Evan Chen, Kenny Lau, Ken Ono and Jujian Zhang, "Parity of k-differentials in genus zero and one", arXiv:2602.03722, February 3, 2026.
21. ^1 ^2Evan Chen et al., "Fel's Conjecture on Syzygies of Numerical Semigroups", arXiv:2602.03716, February 3, 2026; published in Journal of Combinatorial Theory, Series A, doi:10.1016/j.jcta.2026.106237.
22. ^1 ^2Evan Chen et al., "Almost all primes are partially regular", arXiv:2602.05090, February 4, 2026; published in Archiv der Mathematik, doi:10.1007/s00013-026-02261-y.
23. ^Carina Hong, "Primes: Almost surely, partially, regular", Axiom Math, February 5, 2026.
24. ^1 ^2Carina Hong, "Excited to announce Axiom's Series A", X, March 12, 2026.
25. ^1 ^2 ^3Ina Fried, "Exclusive: AI math startup's proofs land in peer-reviewed journals", Axios, May 26, 2026.
26. ^1 ^2 ^3Alex Schneidman, Jimmy Xin and Chris Cummins, "Releasing AXLE", Axiom Math, March 5, 2026.
27. ^1 ^2 ^3 ^4Alberto Alfarano and François Charton, "Axplorer", Axiom Math, March 25, 2026.
28. ^David Kurniadi Angdinata, Evan Chen, Seewoo Lee, Ken Ono and Jujian Zhang, "ABC implies that Ramanujan's tau function misses almost all primes", Indagationes Mathematicae, 2026.
29. ^1 ^2Axiom Math, "AgreeToDisagree", GitHub repository (Lean files for "We Can't Agree to Disagree, Formally: Aumann's Theorem and Assumption Accounting in Lean"), May 2026.
30. ^1 ^2Axiom Math, "IMO2026 formalization.yaml", GitHub, July 2026.
31. ^Axiom Math, "PrimeGapsLib", GitHub repository, August 2026.
32. ^1 ^2Benjamin Skuse, "Axiom Math Uses AI to Formally Verify 246 Theorem", IEEE Spectrum, August 17, 2026.
33. ^1 ^2Axiom Math, "Publications", company website, accessed October 27, 2026.
34. ^Kenny Lau (contributor), "Explicit positive lower density for the Collatz Conjecture", Hexagon preprint hexagon:2610.00249v1, October 14, 2026.
35. ^Hexagon Mathematics Foundation, "Hexagon", preprint repository home page, accessed October 27, 2026.
36. ^1 ^2 ^3 ^4MIT Department of Mathematics, "Carina Hong '22 Honored With Morgan Prize", November 18, 2022.
37. ^1 ^2RAISE Summit, "Shubho Sengupta", speaker profile, accessed October 27, 2026.
38. ^Kyle Wiggers, "AI benchmarking organization criticized for waiting to disclose funding from OpenAI", TechCrunch, January 19, 2025.
39. ^Guillaume Lample and François Charton, "Deep Learning for Symbolic Mathematics", arXiv:1912.01412, December 2, 2019.
40. ^Alberto Alfarano, François Charton and Amaury Hayat, "Global Lyapunov functions: a long-standing open problem in mathematics, with symbolic transformers", arXiv:2410.08304, October 10, 2024.
41. ^1 ^2François Charton, Jordan S. Ellenberg, Adam Zsolt Wagner and Geordie Williamson, "PatternBoost: Constructions in Mathematics with a Little Help from AI", arXiv:2411.00566, November 1, 2024.
42. ^Chris Cummins, Volker Seeker, Dejan Grubisic, Baptiste Roziere, Jonas Gehring, Gabriel Synnaeve and Hugh Leather, "Meta Large Language Model Compiler: Foundation Models of Compiler Optimization", arXiv:2407.02524, June 27, 2024.
43. ^Jimmy Xin, Alex Schneidman, Chris Cummins, Karun Ram, Srihari Ganesh and Jannis Limperg, "AXLE: A Cloud Infrastructure for Lean 4 Theorem Proving Utilities", arXiv:2606.26442, June 24, 2026.
44. ^Axiom Math, "AXLE - Axiom Lean Engine", accessed October 27, 2026.
45. ^Axiom Math Mathematical Discovery Team, "Attacking Hard Open Problems", Axiom Math, November 23, 2025.
46. ^François Charton and Ashvni Narayanan, "Transformers know more than they can tell: Learning the Collatz sequence", arXiv:2511.10811, November 13, 2025.