Axiom Math Says Verified Reasoning Can Outscale Informal AI

Carina Hong’s central claim is that formal verification is being misunderstood if it is treated mainly as an antidote to hallucination. For Axiom Math, verification is not primarily a tax imposed by safety-critical industries, nor a way to make weak AI less wrong. Hong frames it as a way to make strong reasoning compound.

The distinction matters because it changes the business, the research agenda, and the model architecture. In the older view, formal verification belongs to domains where failure is unacceptable: aerospace, subway switching systems, aircraft, enterprise infrastructure, hardware, finance. Hong mentioned the Paris trade union demanding formal verification for automatic subway switching; the European Space Agency’s use of formal verification around Ariane; Boeing and Airbus; and AWS’s work on automated reasoning for enterprise customers that need stronger guarantees than testing can provide. That history, she said, made verification feel like “tax and compliance.”

Axiom’s thesis is different. Hong argues that verification should be understood as a mechanism for scaling intelligence. Her example is Ramanujan: an already brilliant mathematician whose intuitions became more powerful once proof writing turned them into theorems that others could build on. The proof did not create the brilliance; it made the brilliance transmissible, checkable, and composable.

That view also explains why Hong does not see Axiom as merely a “math startup,” even though she repeatedly says math is the company’s DNA. Formal math gives Axiom a dense, structured, checkable domain in which to build a reasoning engine, while verification is the first market where that work can become useful. The larger ambition is verified AI: systems whose reasoning can be grounded, decomposed, checked, and reused across domains.

Hong draws a parallel to coding models. When OpenAI’s o1-style reasoning models appeared, she said, Anthropic was known to be working seriously on coding. Many observers treated coding as a vertical B2B play. Her interpretation is that coding turned out to be far more horizontal because structured data and code generation transferred into broader reasoning capability. She believes formal math and Lean may play a similar role: what looks like a niche problem may become an infrastructure layer for verified reasoning.

That is why she pushes back against the idea that Axiom’s total addressable market must be a narrow set of mission-critical industries. “The TAM is all code,” she said, defining it as a “right of first refusal” on AI-generated code: not that every piece of code must be verified, but that verification capability should become good enough, fast enough, and cheap enough that users can choose it when it matters.

For a small startup, the performance argument is as important as the safety argument. Hong said Axiom has less compute and less data than frontier labs, so its advantage must come from better signal. Verified generation, in her telling, provides that signal. In a Lean-based setting, a proof either checks or it does not; the system can use that grounding for reinforcement learning and search in a way that informal natural-language grading cannot easily match.

That is the basis for Hong’s strongest claim about the path to mathematical AGI: she does not believe an informal math system alone will be the solution. Informal systems can produce impressive results, and Hong does not deny that frontier labs with enormous resources can push them far. But she argues that human expert grading does not scale, LLM-as-judge evaluation introduces stochastic judgment, and the number of people capable of evaluating frontier mathematical arguments is itself a bottleneck. Formal systems, she argues, change the sample-efficiency curve.

Axiom’s most visible proof point is its reported score on the 2024 Putnam exam. ? brandon-anderson introduced the company by noting its perfect score on the Putnam and its claim of being the first AI to prove research conjectures using formal verification. The on-screen lower thirds identified Anderson as a staff scientist at Atomic AI and RJ Honicky as CTO of MiraOmics; Anderson said he builds RNA therapeutics at Atomic AI, while Honicky works on spatial transcriptomics. Hong said Axiom competed in real time and scored 120 out of 120. She also said Math Arena found the best LLM at the time, DeepSeek, scored 103 out of 120, while the best human score was 110.

For Carina Hong, the result matters because Axiom’s system was built on orders of magnitude less data than informal large language model approaches. She described the question before the competition as whether a formal math system, with far less data, could even match or beat an informal LLM. The Putnam was the first case, she said, where it beat both the best human score she cited and the best AI system she said Math Arena evaluated.

The result also sits inside a broader technical distinction Hong makes between olympiad-style systems and formal math systems. She described Google DeepMind’s AlphaProof performance at the 2024 International Math Olympiad as the “IMO moment” for her, more than the later 2025 gold-medal result. Her reason was that across 2024 and 2025, she said, AI systems could solve the problems that were not combinatorics. The score difference reflected the composition of the exams: 28 out of 42 in 2024 versus 35 in 2025 because 2025 had only one combinatorics question.

Combinatorics, Hong said, remains unusually difficult because the key steps can be very creative. She described seeing friends who were IMO gold medalists and Putnam fellows perform combinatorial constructions and thinking, after the fact, that the construction was tractable but the idea was hard to imagine. A Lean-based system may struggle precisely at that “very creative” step.

That limitation leads to a second Axiom effort: mathematical discovery. Hong said proof is not enough for math because before proving something, a mathematician often does not know what to prove. They generate examples, look for sequences, search for graph constructions, and form intuitions before they state lemmas or conjectures. Lean can check and help prove formal statements, but constructions and pre-conjectural exploration are a different problem.

Axiom is therefore investing in mathematical discovery tools that do not use Lean. Hong said the company planned to open-source two codebases for mathematicians and theoretical physicists who want to find constructions, such as complicated graph constructions. She described this as a “pre-conjecturing step”: tools to help users form the intuitions and candidate lemmas they might later give to Axiom Prover.

She named François Charton, a member of Axiom’s technical staff, as one of the original figures in this area. Hong said Charton had previously worked on systems that could find counterexamples and disprove a 30-year-old conjecture, and had found a solution to a 130-year-old problem involving a global Lyapunov function in the three-body problem.

The point is not that discovery replaces proof. Hong’s architecture is closer to a division of labor: discovery tools help generate constructions and intuitions; formal proving systems attempt to turn specified claims into checked proofs; informal reasoners may help propose specifications and test cases. Axiom’s bet is that mathematical intelligence requires all of these, with formal verification supplying the checkable substrate for compounding.

Carina Hong describes Lean as central to Axiom’s approach because it turns mathematical proof into executable structure. Lean is a computer program for math proofs: a formal language in the same broad family as Isabelle, Coq or Roc, Dafny, Agda, HOL, and related proof assistants.

Hong’s claim about Lean’s correctness guarantee comes with the safety caveat attached. If a proof written in Lean compiles under safe conditions — without improper use of escape hatches or other “weird things” — then the proof is correct in the relevant formal system. The caveat matters because Lean has mechanisms such as sorry, which allows a proof writer to take a result for granted. Because of such escape hatches, she said, tools are needed to ensure that proofs are safe. She mentioned comparators, SafeVerify, and Axiom’s verify_proof, which she said is about 100 times faster than comparator.

Lean is also more than a proof checker. It is a Turing-complete functional programming language. Hong described a candidate in Axiom’s interview process, now at the Lean FRO, writing Autograd in Lean. This dual identity matters because Lean can sit between code and proof: it can express computation, but its foundations also allow statements and proofs to be checked.

Hong invoked the Curry-Howard correspondence — the relationship under which proofs can be understood as programs — to explain why Lean can operate this way. For Axiom, this makes Lean a bridge between formal math and software verification. The system can use Lean proofs as training data because correctness is not a matter of preference or consensus. The proof either checks or it fails.

That checkability changes the reinforcement learning problem. Axiom uses what Hong called “Lean data”: correct Lean proofs. Its system is an ensemble of multiple models, post-trained with supervised fine-tuning and reinforcement learning. She said the base models may be similar to those used elsewhere, with an inclination toward open-source base models, but Axiom’s post-training and system design are built around formal math.

The system, Axiom Prover, recursively decomposes proof goals into subgoals, learns to backtrack, and scales inference over proof search. Hong said Axiom has found “almost no wall” in scaling inference and has seen Axiom Prover handle proof trees growing from 40 nodes to 4,000 nodes. She described the system as not simply an LLM but an ensemble system of post-trained models plus tooling, including the AXLE tools Axiom released.

The dependence on Lean also creates constraints. Distribution shift is real. If a domain lacks the necessary formal definitions in Lean’s ecosystem, the system has little to build on. Hong contrasted algebra, which she said has been easier to codify in mathlib, with analysis, where definitions around convergence and limits become trickier. She said Axiom likely would not perform well in areas such as differential topology or differential geometry if the relevant definitions are not present.

Where definitions are present, she said, Axiom has seen stronger diversity: number theory, commutative algebra, algebraic geometry, combinatorics, and probability. The system’s performance is therefore not just a function of model capability; it depends on the state of the formalized mathematical substrate.

The hosts repeatedly pressed on the same issue from different angles: even if Lean can check a proof, how does a user know the proof corresponds to the thing they meant to prove?

This is the specification problem, and Carina Hong did not dismiss it. Her strongest formulation was: “If it’s not specified, it’s not proven.” A bank asking for a “safe financial audit” is not yet asking for something formally verifiable, because “safe” must be translated into precise statements. Humans are bad at specifying everything they want. Formal verification can only prove what has been specified.

That boundary is especially visible in code. Hong described two possible Axiom roles. One is as a verification partner: a user already has a program and wants Axiom to verify it. The other, more important to her, is verified generation: Axiom generates the program and the proof together, so the output is not code later inspected for correctness but code accompanied by a formal guarantee.

Her vision is compositional. A high-level coding agent might decompose a complex task into parts. At some point, one component becomes small and precise enough that it can be handed to Axiom. Axiom either returns a formally verified program for that component or says the task is still too hard. Hong described the aspiration, with a caveat around theoretical limits, as: anything that can be defined can be executed; anything that can be specified can be proven.

The hosts raised Rice’s theorem, decidability, incompleteness, and complexity limits. Hong acknowledged the theoretical boundary: not all programs can be formally verified. Her response was pragmatic. The goal is not to verify all possible programs, but to verify a large share of useful ones. Theory does not, in her view, remove the incentive to push practical verification as far as possible.

The key mapping, as Hong described it, is from a program and a statement to verifiability conditions and a proof. The program verification community often supplies the verifiability conditions; Axiom wants to supply the proof. But the quality of the result depends on whether the statement and conditions actually capture the user’s intent.

This led to testing. Hong does not see testing as obsolete in a verified world. Instead, she described testing as a way for an informal reasoner to ask, “Have you thought about this case?” Mutation-based LLM unit-test generation, including work she attributed to Axiom CTO Shubho, becomes useful because it can propose specifications. Tests, input-output pairs, and counterexamples can ground the auto-formalization process.

Auto-formalization is one of the hardest steps. Turning an English coding problem into a formal specification is difficult because, before the problem is solved, there may be little signal that the formalization means the same thing as the English. Test cases can ground a coding specification. Pure math is harder: a Lean theorem statement often does not have numerical input-output examples. A formalized proof can be run, but a formalized statement may still require a human to “eyeball” whether it says the intended thing.

That leaves Hong with an interactive picture of future coding. Informal agents propose specifications and edge cases; humans refine intent; formal systems prove what has been specified; generators produce code and proof together. Verification does not remove judgment. It relocates judgment to specification, decomposition, and choice of what is worth proving.

Axiom’s path from formal math to software verification runs through “code with proof.” Carina Hong discussed Code Verina, which she described as a Lean-friendly code verification benchmark rolled out by Berkeley and Meta researchers in 2025. Each problem has a code part and a proof part: the system must generate code that solves the problem and a proof that the code indeed solves it.

Hong reported that the GPT model version evaluated on the benchmark had low pass rates: roughly 3.6% pass@1 and about 22% with an iterative method. Formal prover systems such as COPRA, DeepSeek Prover, and GOTO Prover were around 11–12% in pass@1-style evaluation, according to her. She said a competitor had released a result of 96% on the proof-only part. Axiom, she said, recently tested the Putnam system without modification and solved 187 of 189 full code-with-proof problems, or 99%.

The reason this matters, in Hong’s argument, is that reinforcement learning over mixed informal objectives is weak. If code is Python and proof is a natural-language mathematical explanation, the objective is messy. If proof is Lean and the code is in a strongly typed language such as Rust, the learning problem becomes more convergent. The verifier can provide a sharper reward.

Software verification is not equally valuable for every program. Hong gave the example of a child vibe-coding a Lovable website: there is no need to formally verify that code. Even with agents, some safety problems can be addressed by limiting the action space rather than proving properties of every action. But for enterprises dealing with regulatory workflows, or systems where correctness failures are expensive, the calculation changes.

Hardware is the clearer “hardcore verification” case. Hong said there is no partial credit for a mostly verified GPU. Verification is all or nothing, and “you do need a perfect prover.” One host added that, in his understanding, the industry-standard ratio of design to verification in an ASIC project is roughly one-to-three or one-to-four. Hong agreed and said that ratio applies to both team size and duration. Her point was that even local grid-problem verification can require hundreds of humans and thousands of licenses.

Axiom’s commercial claim is that improving verification capability — latency, accuracy, robustness, cost — determines whether users can rely on formal verification. Hong does not argue that every user will choose it immediately. She argues that Axiom must make verification good enough that it becomes an available choice.

That framing also explains how Hong talks about the company’s $200 million Series A and reported $1.6 billion valuation. Anderson asked directly how there is a market for such a financing. Hong said the round was preemptive and that investors either “dream the dream” with Axiom or do not. Her conviction is that verification is critical to superintelligence and that if Axiom realizes the vision, the company is worth far more.

Her narrower business answer is that the future of coding will be constrained by verification capability. Formal math is the natural starting point, in her argument, because it provides the most structured, checkable reasoning environment. From there, verification capability can extend across software and hardware.

Axiom is not only building models. It released AXLE, the Axiom Lean Engine, as infrastructure for proof validation and manipulation in Lean. Carina Hong described AXLE as a set of metaprogramming tools built in the language of Lean for large-scale Lean operations. The release was intended to make other people’s Lean work more robust, faster, and scalable.

AXLE is the current artifact: tooling for Lean. Hong said it included 14 tools at the time of the discussion. The first she named was verify_proof, which checks that there is no cheating in Lean code: no illicit assumptions, no axioming out false statements such as n + n = n in order to prove an invalid result. Other tools support generation and repair: broken Lean in, good Lean out. Hong argued that strong engineering can go a long way, sometimes more cheaply and straightforwardly than LLM repair.

She also made adoption claims about the first week after release. Hong said members of the Lean community had already been using AXLE, including people in blockchain, and that Axiom had heard from people using Claude plus AXLE as a go-to setup. She mentioned, as a same-day example, a mathematician who she said used Claude and AXLE to formalize a Donald Knuth Ramsey result.

The broader commercial vision is different from the current open tooling. Hong wants Axiom to become a verification service that other AI systems call when they need checked reasoning. She compared this to frontier labs calling search startups such as Exa or Perplexity rather than owning all search infrastructure themselves. If a lab is focused on consumer products or coding, she argued, it may be more rational to deepen its own code-generation moat and call Axiom for verification than to build an internal Lean verification stack.

The argument is not only technical but organizational. Hong said frontier labs often change direction for reasons beyond a researcher’s control. She pointed to OpenAI’s earlier formal math work — GPT-f and miniF2F — and said those people had left. DeepSeek, she said, had a formal team and later dissolved it because of strategic direction. In her view, a startup with a singular mission can stay focused on a hard problem long enough to make progress.

That singular focus is part of Axiom’s intended moat. Hong does not claim data is a permanent moat. She called proprietary data and the flywheel of generated Lean proofs a “time moat,” a buffer created by executing faster. The deeper differentiation, in her account, is the combination of expert mathematicians, Olympiad-level problem solvers, mathlib contributors and maintainers, Lean metaprogramming experts, applied ML researchers from organizations such as Meta FAIR, and code-generation and compiler talent.

This team structure also shortens the feedback loop. Hong said Axiom’s mathematicians are users of the system being developed, so iteration is fast. AI for math, in her view, is inherently interdisciplinary: it borrows from AI for science, code-generation literature, applied ML, formal methods, and mathematics. Axiom’s claim to advantage is that it has concentrated these skills in one place.

Carina Hong repeatedly returns to collaboration as one of the deeper consequences of formal verification. Mathematics has not historically been as collaborative as software engineering, she said. Projects rarely have hundreds or thousands of contributors. Polymath was an exception. Large formalization projects in Lean show another model: divide work into subtasks, use a shared formal language, and let the checker make integration possible.

But the bottleneck is not merely proving subgoals. It is writing the blueprint. Hong pointed to Terence Tao and Alex Kontorovich’s blueprint-writing process as an example of the human work required to assign tasks and make them fit together. In other formalization results, including work she referenced around sphere packing, she said the blueprint remained human-generated. Auto-generated blueprints are, in her view, a major technical bottleneck.

This becomes important as proof systems scale. A system might produce tens of thousands or even millions of lines of Lean. A host asked whether such outputs would be bad for the mathematical community because humans often value proofs not only for the result but for understanding. Hong acknowledged the concern and described a hypothetical panel discussion at an AI for Math workshop with Leo de Moura, Jeremy Avigad, and others about whether mathematicians might stop trying to understand AI-generated proofs.

Her answer was optimistic. Humans will still try to understand the outputs they consider important because curiosity is a basic human need. But attention becomes the bottleneck. If verified systems produce more correct mathematics than humans can consume, then human taste matters even more: choosing which statements deserve attention, which proofs deserve explanation, and where compute should be spent.

This also leads to the issue of elegance. A host asked whether Axiom might train systems to find multiple conceptually orthogonal proofs, including shorter or more elegant ones. Hong said that may come later, but “elegance” and “taste” look like alignment problems. Humans decide what is elegant, which makes the training signal a matter of human preference rather than purely formal correctness.

There is a further educational tension. If AI systems can formalize and prove too much automatically, people may lose the training process that develops mathematical taste. Hong said some of her friends learned or reviewed undergraduate mathematics by formalizing material in Lean by hand. Auto-formalization can remove that learning process. She compared this to programming: one may not need to know assembly language, but there is still a threshold of practice needed to become a capable programmer. In math, over-reliance on strong AI could prevent people from acquiring the foundation needed for taste and intuition.

Formal verification, then, opens collaboration but does not eliminate human roles. It may make proofs checkable and tasks distributable. It may allow non-experts to participate in formalization or lemma-proving efforts. But the source still places blueprint design, specification, taste, and attention at the center of human contribution.

Axiom’s claimed research-conjecture results also surfaced a cautionary issue: proving a statement is not the same as establishing that the problem was previously unsolved.

A host raised a controversy around an Erdos problem, asking about the relationship between solving a problem, discovering prior work, and formalizing a proof. Carina Hong said Harmonic had publicized solving unsolved Erdos problems numbered 124 and 481. Axiom, then a young company, trusted Harmonic’s literature review and believed the problems were truly unsolved. Axiom wanted to test whether its system could attempt the same problems and did not expect it to solve them. It turned out, she said, that both companies were wrong: the problem had been solved before.

Hong said Axiom should own the mistake. She also mentioned a separate case, “Dead Ends and Square-Free Walks,” involving Professor Miller, where Axiom again failed to identify that a problem had already been solved. In that case, she said, Professor Kannan Soundararajan pointed out that a relevant result traced back through a MathOverflow or StackOverflow post to a 1936 result.

Her broader point was that search and retrieval are hard. The difficulty is not only whether a problem appears in a database as solved. Many problems are not directly solved under the same statement but follow as easy or nearly trivial extensions of other results. Equivalent formulations, old literature, forum posts, and implicit consequences all complicate provenance.

Hong said that after the Erdos issue, Axiom became extremely careful. She also said a knowledge graph or knowledge base is an important component for any company in this area and is not discussed enough. This sits alongside the formal proof system: Lean can check whether a proof follows from definitions and lemmas, but it does not by itself determine whether the claimed novelty of a problem is accurate.

The controversy therefore reinforces the specification problem in a different form. It is not enough to prove a statement. One must know what statement is being claimed, whether it matches the intended problem, whether the result is novel, and how it relates to existing literature. Formal verification can certify derivation; it does not automatically certify provenance.

Carina Hong described Axiom’s origin as an obsession rather than a gradual transition. She had studied neuroscience at Oxford, though she said that year mostly taught her what was hard and impossible rather than what might work. Through the UCL Gatsby Institute, she spent more time around AI than neuroscience. She joked that in the United Kingdom, calling something “brain science” could attract support when calling it AI might not; Gatsby’s computational neuroscience environment was, in her telling, full of people effectively doing AI.

She then entered Stanford’s JD-PhD structure and spent a full residency year in law school. She enjoyed law — criminal law, litigation, appellate reasoning, antitrust, contracts, bankruptcy, tax — and saw some transfer from mathematical reasoning into legal argument. But she also described the year as the first in which she had no science, technology, or math in her life. She began reading post-training papers and thinking constantly about reasoning progress.

Conversations with Shubho intensified the obsession. Hong said she reached a point where she was thinking about AI doing math “literally every minute.” At a Knight-Hennessy event, she asked Julie Zhuo what to do if she wanted both a startup and academia. Zhuo asked how her time was split between the two. Hong answered: 100% startup, 0% academia. Zhuo told her to follow her energy.

1. International Math Olympiad day
   Hong said Axiom was founded on the day of the IMO, making that contest impossible for the new company to target.
2. Four months later
   Axiom targeted the Putnam, which Hong said was harder than that year’s IMO on the MOHS scale.
3. After seven to eight months
   Hong described Axiom as a roughly 30-person company that had just raised a $200 million Series A.

That led Hong to start fundraising almost as soon as she began the math PhD. Her reason for choosing a for-profit startup was that the ambition was broader than mathematical breakthroughs. She saw math reasoning as part of AI scientist systems, recursive self-improvement, and general infrastructure for verified reasoning. The question was not only “solve math, then solve science,” though she accepts that narrative. It was also direct transfer learning: formal mathematical reasoning may improve general reasoning, coding, and verified execution.

This is why Hong insists Axiom is on the infrastructure stack. Code is language, but on the structured end. It bridges informal and formal. Axiom, in her framing, is not choosing between a fully informal system and a fully formal AlphaProof-like approach. It is building systems that bridge informal and formal, high-level and low-level, discovery and proof, specification and execution.

That also explains her view of openness. Verification has often been associated with closed industries: defense, aerospace, regulated systems, mission-critical infrastructure. Hong argues that verified AI can instead open collaboration: human-human collaboration through blueprints and Lean, human-AI collaboration through checked proof and formalized tasks, and eventually agent-agent collaboration grounded by verifiable artifacts.

When asked about the biggest bottleneck facing the field, Carina Hong first answered: fragmentation. She sees a market in which too many people start too many companies rather than joining forces on hard technical missions. That, to her, is a bubble indicator. Some categories are genuine moonshots that look bubbly; others are fragmented because market conditions encourage ego, founder status, and capital parking rather than disciplined execution.

She distinguished AI for math from more fragmented areas. In her view, AI for math is not yet a bubble because strong people are joining forces. She cited Axiom’s ability to put people such as Guillaume and François Charton on the same team, combining benchmark-setting, proving, and discovery capabilities. She also said Harmonic appears to have strong talent joining together. The category’s health, in her view, comes from the absence of fragmentation.

But she expects fragmentation to increase as Axiom and Harmonic establish category leadership. More teams will enter. More capital will chase the area. Talent, especially reinforcement learning talent, is already difficult to attract and retain. She described companies being started and sold months later, with time that could have gone into technical work instead spent on deals. Having gone through two fundraises, she spoke of that cost with some frustration.

The second bottleneck is short-term pressure. Axiom moved quickly because the timing forced it: the company was founded on the day of the International Math Olympiad, making that contest impossible to target, and the next major exam was the Putnam four months later. But she said building a company entirely around four-month goals would make it shortsighted.

The danger for AI for math is that pressure to prove commercial value could distract from core capability improvement. Hong acknowledged that code verification may be the commercial holy grail, and it may be possible that solving code verification also solves math verification with some distribution-shift caveats. But she strongly believes that if the field over-optimizes for near-term commercial proof, it may neglect the deeper work needed for verified reasoning.

The long-term horizon is recursive self-improvement. Hong said she believes recursive self-improvement will happen anyway; Axiom is trying to make formal verification earn its place in that future. Whether formal verification becomes welcomed, deployed, and consensual depends, in her view, on execution. If the problem can be boiled down to execution, she said, then the response is to go for it.