Axiom’s Bet: Make Reasoning Checkable, Then Scale It

Turn mathematical intuition into reusable knowledge

A brilliant mathematical intuition leaves a practical problem: how can someone else build on it? Early in the conversation, Carina Hong uses Ramanujan’s work with Hardy and Littlewood as an illustration. In her telling, proof writing turned exceptional intuitions into theorems that subsequent mathematicians could reuse. Verification makes insight cumulative. Axiom’s ambition is to give AI reasoning that same capacity to be checked, extended, and shared.

The Latent Space conversation opens with a question about the business behind that ambition. Brandon Anderson reports a $200 million financing round; Hong identifies it as a Series A and describes Axiom as roughly seven or eight months old, with about 30 people. She sees formal verification as the first market for Axiom’s mathematical capabilities, with the funding supporting faster execution and exploration of applied domains.

Hong’s broader bet is on transfer from structured training data: capabilities learned in one domain may improve reasoning elsewhere. She draws an analogy with coding and argues that mathematics expressed in Lean could have similarly broad value. Axiom still wants to build a superhuman mathematician, while pursuing the hypothesis that formal mathematical training can support more general verified reasoning.

Competition results help explain her confidence, but scores depend on the problem mix. Hong regards AlphaProof’s 28 out of 42 points at the 2024 International Mathematical Olympiad (IMO) as the decisive milestone. In her account, solving all non-combinatorics problems would have earned 28 points in 2024 and 35 in 2025. Creative combinatorial constructions remained a distinct obstacle.

Lean makes proofs computationally checkable

Lean is a formal language for mathematical proofs and a functional programming language. The connection rests on the Curry–Howard correspondence, which connects proofs and programs and makes type checking a useful entry point for programmers. Lean also supports ordinary programming: an interview candidate reportedly implemented automatic differentiation in it. An introduction to Lean for programmers offers a companion resource at this bridge.

Mathematicians already enforce logical rigor through community scrutiny and peer review. Lean adds computational checking and tactics—tools that automate low-level deductions. Its existing grind tactic can handle substantial proof work without AI. That division of labor lets a mathematician concentrate on the high-level argument while tools handle routine steps.

The guarantee depends on what the checker accepts. Lean’s sorry leaves an assertion provisionally accepted without a proof, allowing collaborators to work around unfinished parts. But an accepted placeholder is still a proof gap. A completed verification must exclude unintended reliance on those placeholders.

Axiom argues that checkable proofs also improve learning efficiency. The guest reports 120/120 on the December 2025 Putnam exam, describing participation in real time, against a reported 103/120 for an unspecified DeepSeek model evaluated by Math Arena and 110/120 for the best human. The company’s Putnam account provides a related resource. The comparison does not specify matched inference budgets, model versions, or grading procedures; the reported top human score is also not tied to an identified student. It supports Axiom’s performance argument without isolating how much of the difference comes from formal verification.

Decompose proof searches; discover constructions

Axiom uses multiple post-trained models, favors open-source base models, and relies heavily on Lean data. Proof checking supplies a correctness signal for reinforcement learning (RL). During inference, the system recursively decomposes proof goals into subgoals and learns to backtrack. The guest reports little sign of a ceiling to inference scaling so far, without giving a scaling curve or tested compute range.

An interviewer asks whether repeated exploration could concentrate capability near the initial training data, leaving other mathematical fields out of reach. The response identifies two different constraints: - Formal definitions must be available. Mathlib, Lean’s mathematical library, supplies material a prover can build on. The guest considers algebra easier to formalize than analysis, where limits and convergence complicate definitions, and expects weaknesses in differential topology and differential geometry because of perceived gaps in that infrastructure. - A construction may need to be invented. In combinatorics, finding an unusual object can be the hard part. Once someone supplies it, the remaining reasoning may become much easier.

The construction problem motivates Axiom’s investment in mathematical discovery tools outside Lean. Discovery here begins before conjecturing: write initial terms of a sequence or construct small graphs with a desired property, then use those examples to develop intuition. At the time of the conversation, Axiom was preparing two discovery codebases for open-source release, with manuals aimed at mathematicians and theoretical physicists.

The proposed research workflow connects discovery to proof: 1. Explore constructions that make a difficult problem concrete. 2. Formulate intermediate lemmas or conjectures suggested by those examples. 3. Give suitable proof tasks to Axiom Prover. The limitation is explicit: the prover cannot simply solve an arbitrary hard conjecture for the researcher.

Generate code with a proof of its specified behavior

The software vision applies decomposition to engineering. A general assistant such as Claude might break down a distributed system and call Axiom for a component it can tackle. Axiom would return a formally verified program—or report that the task remains too difficult. The guest acknowledges theoretical limits on universal verification; the practical ambition is to cover a majority of useful programs.

Axiom describes two possible services: - Verify existing code: a user supplies a program and asks for verification. - Generate code with a proof: the system produces both a program and a formal proof that it meets its specification. In the proposed pipeline, the program and statement of intended behavior give rise to verification conditions, the obligations a proof must establish. Program-verification machinery generates those conditions; Axiom Prover supplies the proof.

The companion identifies the code-with-proof benchmark discussed here as Verina. Each task requires a program that solves a coding problem and a separate proof that it does so. Axiom reports solving 187 of 189 tasks with both code and proofs, using its Putnam system without modification. The guest compares that with a competitor’s reported 96% on the proof portion alone. Those task scopes differ, so the percentages are not a like-for-like ranking.

The guest expects code paired with formal proofs to provide a more coherent learning target than code paired with natural-language mathematics. In particular, Lean proofs alongside a strongly typed language such as Rust are proposed as a better combination for reinforcement learning than Python and informal proofs. This is an expectation, without a measured language comparison.

A correct proof still needs the right specification

An interviewer repeatedly presses on the boundary between the user’s problem and its formal statement: how do you know the proof establishes what you meant? The response calls for inspecting the program, statement, and verification conditions. A complex flight-control system makes the difficulty tangible; so does a bank asking to have a financial audit proven without defining the claim. Properties omitted from the specification are not proven.

Informal reasoning and testing can help propose those missing properties. A system that suggests overlooked cases helps a person decide what to specify, much as examples help a mathematician decide what to conjecture. The prover then establishes the resulting claims. Even an extremely capable verifier would still need guidance about which properties matter.

Autoformalization translates an informal statement into a formal one. For an English-language programming-contest problem, supplied input-output cases can help ground the translation before the problem is solved. Mathematical proof tasks often lack numerical answers that provide the same check. A formalized proof can be checked computationally, while the statement’s correspondence to human intent still needs inspection.

Proof size creates a separate constraint. The guest estimates roughly 20 lines of proof per line of program code, without identifying a program class or knowing how the ratio changes with complexity. Axiom Prover is an ensemble of post-trained models and tools, reported to have handled proof trees growing from 40 to 4,000 nodes. These are observations of larger workloads, without associated success rates or compute costs.

The interviewer asks whether proofs could outgrow context windows and lose essential details through repeated summarization. The guest proposes cyclic consistency as a possible check on explanations: translate Lean into prose, formalize that prose again, and attempt an equivalence proof. An existing informal summarizer is described as working reasonably well, but the proposed round trip is not a demonstrated solution to the context-window concern.

When attention and verification become scarce

Imagine a correct million-line proof arriving faster than a mathematician can understand it. The discussion treats this as hypothetical, then asks what human work would remain. The optimistic answer is that curiosity persists, but attention becomes the bottleneck. Mathematical taste would guide both what people study and which problems deserve finite compute.

An interviewer suggests seeking conceptually different proofs, including elegant alternatives to brute force. The response treats training for elegance as future work: human preferences would define the objective. Yet taste requires some hands-on practice. A programmer need not master assembly, but avoiding proof construction altogether may remove experience essential to mathematical judgment.

The commercial value of verification likewise depends on the application: - Hardware needs completed verification. The guest argues that a mostly verified GPU is insufficient; occasional successful proof searches do not meet that requirement. - Low-stakes websites may not need formal proofs. Verification may add little value to a casually generated site. - Risky agent actions may be constrained directly. Limiting available actions can address some problems without formal verification. - Regulated enterprise agents may justify verification. Adoption would depend on latency, accuracy, and overall performance making it practical.

Axiom’s objection to scaling purely informal mathematics is partly economic: expert evaluation is scarce. The guest points to the difficulty of finding people who can grade a nontrivial result in the Langlands program. Formal and informal reasoning remain complementary in the intended system, but computational proof checking offers a way to reduce dependence on expert grading. The stronger conviction that an informal-only system cannot deliver general mathematical intelligence remains a belief, rather than an impossibility result.

Axiom describes an internal advantage in expert mathematicians using the system they help build. Its team combines research and competition mathematics, Mathlib contributors and maintainers, applied machine learning, code generation, and compiler expertise. The personal motivation offered is familiar to researchers: a problem just beyond reach can be discouraging, and an AI collaborator might help.

The career discussion traces a path through neuroscience, AI research, and law. The guest recalls neuroscience study as teaching more about what is difficult than what might work, while research with faculty at UCL Gatsby made it a productive year of AI study. A combined law-and-doctoral program then required a full year in law school. Law suggested further possibilities for mathematical reasoning—especially appellate argument and the flowchart-like structure of antitrust and some contract law—while exposing how much remains underspecified.

Proof checking does not establish novelty

A valid proof can establish something already known. In Axiom’s account, it tested Erdős problems 124 and 481 after trusting Harmonic’s characterization of them as unsolved, then learned that prior solutions existed. The guest also acknowledges a literature-search failure involving Dead Ends in Square-Free Walks and says Axiom should have checked the prior work itself.

Novelty checking requires more than finding identical wording. An equivalent argument may appear elsewhere, or a problem may follow almost immediately from another result. In the square-free walks account, Kannan Soundararajan directed the researchers to an online post pointing to a result from 1936. Correctness and novelty require different checks: one establishes that an argument works; the other asks what it adds to existing knowledge.

Asked how search fits into the conjecture engine, the guest emphasizes knowledge bases without describing an implementation. The longer-term goal is a feedback loop in which Axiom Prover learns from the mathematics it proves each day. Accumulated proof data is described as a temporary competitive buffer, whose value depends on continued execution; no measured self-improvement result accompanies the proposal.

AXLE validates assumptions and supports shared proof work

AXLE, the Axiom Lean Engine, makes the tooling concrete. At the time of the conversation, it was a newly released collection of roughly 14 proof-validation and manipulation tools, implemented in Lean through metaprogramming and offered free to the community. One interviewer reports using its verification API with Claude Code because it was easier than setting up a local Lean toolchain.

AXLE addresses two kinds of proof engineering: - Validate the assumptions behind success. If generated code introduces an unjustified assumption such as n + n = n, it can derive 2 + 2 = 2. The derivation follows the assumption but fails to establish the intended mathematical result. AXLE checks for such shortcuts. - Repair broken Lean code. Its repair tools aim to turn invalid code into working code, with the hope that direct engineering can make some repairs cheaper and simpler than another language-model attempt.

Shared tools can broaden collaboration, but organizing the work remains difficult. A formalization blueprint specifies subtasks and how their results fit together. The guest highlights blueprint writing in work involving Terence Tao and Alex Kontorovich and identifies automatic blueprint generation as a technical bottleneck. Formalizing a known argument and discovering a new proof also require different contributions.

Automation brings back the educational tradeoff. The guest recalls friends facing difficult doctoral research who used manual Lean formalization to revisit undergraduate mathematics they could still understand. Having a prover do that work can remove part of the learning experience.

A Putnam war-room recollection connects verification latency to what search can accomplish before a deadline. The team received the paper from an official proctor and watched AXLE handle the workload. This later recollection mentions eight problems within the time limit; its relationship to the earlier 120/120 account is left unresolved. The guest credits AXLE’s speed with meeting the deadline, without supplying timings or a measured baseline.

The next proposed use is formal tools as reinforcement-learning reward sources: pass Lean programs directly into the tools and obtain proof-validation results or potentially partial scores. The guest explicitly distinguishes this from first translating an informal proof into Lean. The business proposition follows the same division of labor: other labs could focus on code generation while calling verification infrastructure maintained by a specialist team.

Protect the long research horizon

The founding story returns to the year of law school. The guest recalls independently studying reasoning and post-training papers, becoming absorbed in mathematical AI, and beginning fundraising almost immediately after starting a PhD. Julie Zhuo reportedly asked how the aspiring founder divided time between the startup idea and academia. Nearly all the energy already went into the startup, and her advice was to follow it. The motivation for a company extended beyond mathematical breakthroughs to AI scientists and recursive self-improvement.

The closing technical thesis separates two routes to broader impact: - Learn reasoning that transfers. Bridging informal and formal work, and high-level and low-level reasoning, could improve capabilities beyond mathematics. - Discover mathematics that advances science. New results could supply tools for scientific progress. Axiom emphasizes the first route as an infrastructure opportunity. Theoretical science remains a possible later market, with physical testing and real-world signals supplied elsewhere.

When an interviewer suggests that verification enables recursive self-improvement, the response preserves an important distinction: the guest expects self-improvement to happen anyway. Formal verification must earn adoption through execution. Its proposed role is shared infrastructure for human–AI and eventually agent–agent collaboration, making strong reasoning easier to extend as technological creation accelerates.

The final organizational concerns pull in opposite directions: - Combine complementary expertise. The guest worries about researchers dispersing into separate ventures, while describing AI for mathematics as a comparatively healthy exception. Ken Ono and François Charton working on one team illustrate the value of combining mathematical benchmark expertise with discovery and construction capabilities. - Preserve time for technical work. Funding can sustain long research bets, but deal-making and competition for reinforcement-learning talent consume time that could go into capability improvements.

Axiom’s first benchmark sprint supplies the closing example. The guest says the company was founded on the day of the International Mathematical Olympiad, leaving the subsequent Putnam competition as a target roughly four months away. That deadline gave the team a concrete objective, but a company built only around four-month goals could become shortsighted. Market pressure could push the field toward immediate applications such as chip verification before broader capabilities mature. The closing warning is that proving commercial value can itself become a bottleneck if it distracts from improving the reasoning system.