She Raised $64M to Build an AI Math Prodigy | Carina Hong, CEO of Axiom
Summary
Axiom’s $64 million wager is that reliable reasoning needs generation and verification in one self-improving loop, not merely a larger informal model. Hong’s architecture joins a theorem prover, conjecturer, shared knowledge base, and auto-formalization layer, using Lean to combine probabilistic search with deterministic checking: “A proof is a proof.”
The early technical signal is a Putnam 2026 run of eight problems out of 12 within the exam time and a ninth reported two hours after Hong’s initial post, with final scoring still pending. Nine would match the previous year’s top score among roughly 4,000 humans and sit around Putnam Fellow territory, while “the median score is like a zero.” Hong herself scored four and joked about holding a “beat Carina” party.
The commercial wedge is verification labor: hardware design teams may be one-third or one-quarter the size of verification teams, verification can take three years, and Hong thinks AWS spent five years formalizing one hypervisor memory-isolation component. Axiom is targeting chip verification, safety-critical code review, legacy-code equivalence, and database consistency—cases where customers “just want this to not be wrong.”
Axiom does not claim every program should or can be formally verified; Hong divides the market into critical systems, “good to have” cases, and lower-stakes vibe-coded applications. A Lovable website “wouldn’t necessarily need formal verification,” and “you cannot verify all code in Python,” though she argues much of it might still be covered. The harder product problem may be formalizing the correct specification amid ambiguity, not checking the resulting proof.
Hong expects mathematics to shift abstraction rather than disappear, with elite researchers supplying intuition while AI becomes “the diligent grad student or postdoc” proving ideas, constructing examples, and rejecting bad conjectures. Biewald presses that machines might eventually surpass human intuition; she answers “different intuitions” and thinks catching the top 0.00001% of mathematicians will take a long time. Axiom is “not there yet” on P versus NP or the Riemann hypothesis.
The $64 million financing gives runway to a company that is roughly six months old, calls itself “at day zero,” and remains in early conversations with trusted partners. Hong wants Axiom “constantly uncomfortable” around large incumbents, preserving the “small and mighty” hunger she heard in underground Chinese rock bands before later commercialization. The technical milestones are striking; commercialization and specification usability remain the tests ahead.
Deep dive
1. Axiom makes verification part of the reasoning loop
Hong defines Axiom as “a reasoning engine that is self-improving” because it couples generation with verification. Mathematics is the initial testing ground: proofs provide an unusually clean correctness signal and expose the hand-waving that can survive in purely statistical systems.
The architecture contains a prover, a conjecturer, and a shared knowledge base. The prover retrieves established results; the conjecturer uses counterexamples to reject weak ideas before proposing them; auto-formalization connects natural-language mathematics to all three components.
Lean grounds the natural-language model in deterministic checking, enabling what Hong calls “the power of deterministic tooling and probabilistic systems working together.” In an Erdős problem 481 demonstration, the system decomposed its argument into a proof graph whose nodes turned green as subgoals were verified; each node could expose Lean code, which could then be translated back into natural language.
2. Putnam performance supplies Axiom’s first major capability signal
Biewald’s framing establishes the benchmark: the Putnam is an exceptionally difficult undergraduate competition taken by strong mathematics students, and “the median score is like a zero.” Getting even one problem right is meaningful; leading the field is a qualitatively different result.
Within the Putnam 2026 exam limit, Axiom solved eight of 12 problems. A ninth was reported two hours after Hong’s initial tweet, creating an awkward correction; the company still planned to release proofs and its exact final score rather than treating the provisional count as settled.
Hong says nine of 12 matched the previous year’s number-one result among roughly 4,000 human participants and generally corresponds to Putnam Fellow, or top-five, territory—subject to unusually easy years. Her own four of 12 earned a top-250 honorable mention, so Axiom’s eventual score “will potentially triple me.”
Biewald’s useful pushback: ordinary GPT or Gemini can look impressive on Olympiad problems yet fail a simple brainteaser, suggesting machine difficulty does not follow the human hierarchy. Hong’s answer is modular: formal tools excel at fine-grained checking, informal reasoners contribute high-level intuition, and specialized tools handle computation.
3. Formal proofs turn trust into a mechanical property
Hong recalls December 2024 discussions of Putnam solutions generated by “o1 Pro or o3 Pro—I forget,” followed by o3 Preview. Human graders assigned widely different scores, with the eventual consensus that each answer contained a consequential hole the model had hand-waved. “The power of formal systems” is that such gaps cannot pass.
That rigor can look excessive. In analysis problems, Axiom may generate large amounts of Lean code around convergence, limits, or a simple positivity lemma—details a mathematician would dispatch quickly. Hong calls this “almost annoying,” but the heaviest proof node can also be the one supplying the strongest assurance.
Biewald asks whether an AI could produce a 10,000-line proof everyone accepts step by step but nobody intuitively understands. Hong notes that obscure human proofs already require expert panels; after redundant machine steps are removed, she thinks there is a case that a valid proof “might converge to what a human would possibly find,” making AI another collaborator rather than a second-class mathematician.
Their Putnam A3 example shows both overlap and divergence. In the Alice-and-Bob string game, Axiom and humans reach the same clean conclusion—Bob always wins through a strategy requiring little branching. Elsewhere, the machine may brute-force a route humans would avoid or find a proof unlike the one Axiom’s mathematicians expected.
Hong also points to the older AlphaProof system as an “IMO moment”: she says it scored 28, a silver medal against a 29-point gold cutoff, solving every problem except combinatorics. She compares that with the 2025 IMO, where many contestants scored 35 while missing the sole combinatorics problem; for her, the example reinforces the value of combining formal and informal systems.
4. Verification labor creates the initial enterprise wedge
Hong’s economic case starts with imbalance: hardware design teams may be only one-third or one-quarter the size of verification teams, and verification can consume three years. She thinks AWS’s automated-reasoning group spent five years formalizing just the memory-isolation component of a hypervisor—“a shocking number,” not the entire system.
Candidate applications include reviewing agent-generated code, proving edge cases in safety-critical deployments, establishing that migrated code is equivalent to legacy code, lowering dependence on scarce formal-verification specialists, and checking consistency under malicious database actors. At roughly six months old, and after raising $64 million coming out of stealth, Axiom is still holding early discussions with trusted partners rather than claiming broad deployment.
Hong’s more ambitious example unifies generation and verification: auto-formalize a proof of Paxos consistency in Lean, then generate an implementation in a strongly typed language such as Rust from that specification. The commercial promise is not merely finding bugs but making implementation and correctness emerge from the same artifact.
5. Formal methods still face a specification ceiling
Biewald’s pushback is that software correctness is rarely as black-and-white as a theorem. Database markets embraced NoSQL partly by relaxing consistency constraints to operate more efficiently, store user data, and make it queryable; many applications can tolerate trade-offs, so absolute proof may be less valuable than Hong’s mathematics analogy suggests.
Hong responds with three tiers: systems where regulation or deployment risk makes verification essential; cases such as database consistency where it is highly desirable if usability permits; and applications where it is unnecessary. “A Lovable website wouldn’t necessarily need formal verification,” and Hong says the AI mathematician she is building cannot write poetry.
Auto-formalization is therefore a core technology, not merely a data-generation trick. Turning a proof into Lean has checker feedback, but formalizing the statement is harder because the solution does not yet exist. In code, input-output tests can partially ground the intended specification; the system must still resolve ambiguity without confronting users with 500 preference questions.
Hong accepts the boundary raised by Biewald: “You cannot verify all code in Python,” though she thinks a majority might be tractable. Biewald points to reasoning models, stronger code generation, reinforcement learning in verifiable domains, and growing Lean adoption; Hong says these three developments coming together make this a particularly good time. She also cites CSLib under development and Stanford’s Automated Reasoning Group, led by Clark Barrett with support from DeepMind and AWS, as part of efforts to formalize undergraduate computer science and machine learning in Lean.
6. Mathematicians move upward from proof labor to discovery
Hong predicts mathematics will continue, but mathematicians “will learn to work on a different abstraction.” She compares the transition to adopting LaTeX and notes that computer algebra already assists computational research; the new tool would remove more of the manual work of checking every technical lemma.
Her ideal division of labor lets a mathematician such as Terence Tao follow intuition while AI acts as “the diligent grad student or postdoc.” Crucially, discovery also requires constructing examples, spotting patterns, producing counterexamples, proposing conjectures, and feeding the loop with more conjectures and proofs—not just solving a fixed theorem.
Biewald presses the replacement case: why assume the machine will not develop better intuitions or even judge what humans find interesting? Hong’s answer—“different intuitions”—rests on machines and humans having different difficulty curves; she believes reaching the top 0.00001% of human mathematical intuition will take a long time.
The exposure will vary by mathematical style. Problem solvers in domains requiring less deep theory may encounter AI substitution sooner than theory builders who connect literature and open new fields. Axiom is “not there yet” on P versus NP or the Riemann hypothesis, but its unexpected Putnam result is already compressing the builders’ own timeline forecasts.
7. Hong wants an academic engine with an underdog culture
Hong traces her founder temperament to listening, from age five, to politically rebellious underground Chinese rock. She never felt like “the most academic academic” or “the most founder founder”; running Axiom instead feels like “a fish in the water” and “living the rock and roll days every day.”
The team’s three pillars—AI, programming languages, and mathematics—also span chip design, code verification, compilers, and mathematical discovery. Hong says conversations between discovery researchers and formal-proving experts are reshaping ideas about self-improvement, making the company feel “even more academia” because it stretches her intellectual boundaries.
Her cultural metaphor comes from bands whose hungry early songs, written when they were poor, were significantly better than their later work. Axiom therefore tries to remain “constantly uncomfortable,” conscious of large incumbents and its late start, while preserving an underdog mindset, “curiosity like a child,” and a small-and-mighty culture. She compares this phase to graduate school, when mathematicians sometimes produce their best work.