The AI mathematician that refuses to guess. It conjectures, proves, and checks its own work in Lean - then improves itself and does it again.
A logo for a company that thinks in theorems. The mark is plain; the ambition - a self-improving superintelligent reasoner - is not.
Somewhere on a server in Palo Alto, an algorithm is writing mathematics. Not summarizing it, not autocompleting a Wikipedia paragraph about it - writing it. It proposes a conjecture, constructs a proof, and then hands that proof to a machine called Lean that checks every logical step. If a single line is wrong, the whole thing is rejected. No charm, no confidence, no apology. This is Axiom, and this is the point.
In a year when most AI companies sell fluency, Axiom sells the opposite virtue: being unable to lie about a theorem. The company emerged from stealth in late 2025, raised $264 million across two rounds, and reached a $1.6 billion valuation faster than most startups finish their seed deck. Its product, AxiomProver, has reportedly cracked at least four long-unsolved problems and produced proofs that peer-reviewed journals accepted - with an algorithm as the author.
Large language models are remarkable at sounding right. They are considerably worse at being right. They hallucinate citations, invent functions, and produce code that compiles but quietly breaks. The industry's answer has mostly been to ask the model nicely to try again. Axiom's bet is that politeness is not a verification strategy.
Mathematics offers something the rest of AI lacks: a ground truth that cannot be charmed. A proof is either valid or it isn't, and a formal proof checker like Lean will tell you which - coldly, instantly, every time. If you can teach a machine to reason inside that discipline, you get an AI whose claims are checkable by construction. That is the seam Axiom is prying open.
Carina Hong points to three forces arriving at once: the reasoning ability of modern LLMs, the maturity of formal proof languages like Lean, and breakthroughs in code generation. Individually, each is interesting. Together, they make an AI mathematician suddenly plausible - which is a polite way of saying the window opened, and Axiom climbed through it before the paint was dry.
Carina Hong was, by any reasonable measure, already winning at the conventional path. Morgan Prize winner. Nine peer-reviewed papers as an MIT undergraduate. Rhodes Scholar at Oxford with a neuroscience master's. A joint J.D./Ph.D. spot at Stanford. Most people would have stayed and collected the credentials. She left to build a company instead, on the conviction that math is not a niche of intelligence - it is the load-bearing wall.
"Math is AGI," she has said, which sounds like a slogan until you notice she means it literally. Her thesis: reasoning that can be formally verified is the foundation everything else stands on. Get the mathematician working, and physics, engineering, finance, and software verification follow.
She did not build it alone. The founding bench reads like a reasoning all-star roster: CTO Shubho Sengupta, an eight-year veteran of Meta's FAIR lab; founding mathematician Ken Ono, former VP of the American Mathematical Society; Francois Charton, among the first to apply transformers to mathematics back in 2019; plus FAIR researchers Aram Markosyan and Hugh Leather. Hong's stated hiring rule is to keep recruiting people smarter than herself.
MIT math & physics, Rhodes Scholar, Morgan Prize. Left a Stanford J.D./Ph.D. to start Axiom in 2025.
Eight years at Meta's FAIR AI research lab. Now building the systems behind AxiomProver.
Former Marvin Rosenblum Professor at UVA and VP of the American Mathematical Society.
AxiomProver is not one model but a small society of them. A prover constructs proofs. A conjecturer proposes new questions worth proving. And quietly doing the hardest job is auto-formalization - the work of translating fuzzy human mathematics into the exact, machine-checkable language of Lean. Hong calls auto-formalization a core technology, "at least as important as proving itself, if not more so." It is the unglamorous hinge the whole system swings on.
The loop is the interesting part. Each verified proof becomes training signal for the next attempt, so the system is designed to get better at reasoning the more it reasons. Pair natural language with a verifiable machine language, Hong notes, and you get better sample efficiency - the model learns more from less, because every answer is graded by an oracle that never gets tired.
Generates conjectures, proves results, and auto-formalizes them so each proof is machine-verified in Lean before a human reviews it.
Axiom's reasoning playground at axle.axiommath.ai - test proof verification, extract theorems, transform proofs, and build on the API.
A reasoning lab can say anything. Axiom's defense is that its claims are, by design, checkable. AxiomProver has reportedly solved at least four previously unsolved problems, disproved a 30-year-old conjecture, and contributed to cracking a 130-year-old one. Then there is the economics result Fortune reported in June 2026: a theorem taught to students for roughly fifty years that, it turned out, no one had ever formally proven. The machine did.
The AI mathematician is the wedge, not the goal. Axiom's stated mission is a self-improving, superintelligent reasoner - and Hong is explicit that math is only where reasoning is easiest to verify, not where it ends. "Math alone has enormous applications in areas like financial trading, physics, engineering, and simulation," she notes. The longer game is bridging levels of abstraction: from a formal proof to a verified physical model to provably correct code.
Menlo Ventures framed its investment with a tidy inversion of the usual AI story: AI will write all the code; mathematics will prove it works. If that holds, the company building the prover sits underneath everything else - the unglamorous foundation, which is exactly where the foundations tend to live.
Return to where we started. An algorithm is writing mathematics, and a proof checker is grading it without mercy. A year ago that scene was a research curiosity. Now it has a $1.6 billion valuation, journal acceptances, and a fifty-year-old economics theorem that finally has a proof attached to it.
The skeptic's question is fair: is this a durable foundation for AI, or an elegant demo dressed for a funding round? Axiom's answer is unusual in that it is testable. Every claim the company makes about its core technology is, by construction, something a machine can check. Most AI companies ask you to trust the output. This one built a system whose entire reason for existing is that you shouldn't have to. Whether that becomes the substrate for superintelligence or simply the best math assistant ever built, the bet is refreshingly legible - and, for once, you can ask the machine to prove it.
Press: press@axiommath.ai · General: contact@axiommath.ai