🔬Scaling Past Informal AI - Carina Hong, Axiom Math

What It Covers

Carina Hong, CEO of Axiom Math, explains how formal verification using the Lean proof language enables verified AI reasoning rather than merely correcting hallucinations. Axiom scored 120/120 on the 2025 Putnam exam, raised $200M at a $1.6B valuation, and argues formal math provides transfer learning advantages that informal LLM scaling cannot replicate at superintelligence scale.

Key Questions Answered

• •Verified Generation as Performance Gain: Formal verification is not a quality-control tax but a direct performance multiplier. Axiom's system scored 120/120 on the 2025 Putnam exam, outperforming the best human score of 110 and DeepSeek's 103, using orders of magnitude less compute and data than frontier labs. This demonstrates that verified generation produces higher sample efficiency, allowing smaller teams to exceed frontier lab benchmarks on structured reasoning tasks.
• •Lean as Dual-Purpose Infrastructure: Lean functions simultaneously as a functional programming language and a formal proof checker via the Curry-Howard correspondence, which maps proofs to programs. Developers can write autograd in Lean, verify distributed systems components, or prove mathematical theorems within the same environment. Practitioners building AI reasoning pipelines should evaluate Lean not as a niche academic tool but as a Turing-complete substrate for co-generating code and correctness proofs together.
• •Formal Math Transfer Learning Parallels Coding: Anthropic's coding focus in 2023-2024 was underestimated because structured, formal data transfers horizontally across reasoning domains rather than staying vertical. Axiom applies the same thesis to formal math: Lean proof data provides structured, verifiable training signal that transfers to software verification, hardware verification, and general reasoning. Teams building reasoning systems should prioritize formally verifiable data sources over volume of informal chain-of-thought data.
• •Hardware Verification as Near-Term Revenue Anchor: Chip verification currently requires a 1:3 to 1:4 ratio of engineering time and team size dedicated purely to verification relative to design. There is no partial credit for a mostly-verified GPU. Axiom positions formal proof generation as a direct replacement for manual verification labor in ASIC projects, where a single unverified edge case invalidates the entire design. This represents a concrete, high-value enterprise deployment path beyond pure mathematics research.
• •Axle Tooling Enables Claude-Based Lean Workflows: Axiom released Axle (Axiom Lean Engine), a free suite of 14 Lean meta-programming tools including VerifyProof, which runs 100x faster than the prior standard tool Comparator. On the Verina code-verification benchmark of 189 problems, Axiom's system solved 187 with no benchmark-specific modifications. Developers can integrate Axle directly with Claude Code today to generate and verify Lean proofs without configuring a local Lean toolchain, lowering the barrier to formal verification in production workflows.
• •Blueprint Authorship Remains the Human Bottleneck: Large-scale formalization projects like sphere packing in 8 dimensions still rely on human-authored blueprints that decompose theorems into subtasks assignable across contributors. Auto-generated blueprints — high-level proof sketches that structure collaborative formalization — remain an unsolved technical problem that multiple groups are racing to crack. Mathematicians and AI researchers targeting collaborative theorem proving should focus engineering effort on blueprint generation as the current rate-limiting step, not proof search itself.
• •Specification Gap Limits Enterprise Deployment: Formal verification guarantees correctness only relative to a written specification, and humans consistently underspecify what they want from complex systems. A financial audit system or flight controller cannot be fully verified if the specification omits edge cases. Axiom's near-term mitigation combines mutation-based LLM unit-test generation to surface unspecified cases as conjecture proposals, then feeds confirmed specifications to the prover. Teams adopting formal verification should invest in specification tooling and conjecture generation before expecting end-to-end automated correctness guarantees.