Summary
The episode profiles Carina Hong and Axiom Math’s AxiomProver, which achieved a perfect 12/12 on the Putnam 2025 and produced fully machine-checked proofs for open research conjectures. Central to the conversation is the role of formal verification—using the Lean proof assistant—as a way to eliminate hallucinations and produce 100% checkable mathematical reasoning. They explain the generation+verification loop: large language models and tooling generate candidate steps and Lean verifies them, with verified steps fed back to improve the system. The discussion covers technical challenges (notably auto-formalization from English into Lean), commercialization opportunities in verified code and hardware, and the company’s early-stage cultural and fundraising story that attracted mission-aligned talent.
Key Takeaways
- 1Formal verification via Lean can produce fully machine-checkable, 100% reliable mathematical proofs.
- 2AxiomProver’s Putnam 12/12 and end-to-end verified research proofs demonstrate practical competence under timed, real-world conditions.
- 3Auto-formalization (informal English -> Lean) is the principal technical bottleneck but is key to broad applicability.
- 4The generation + verification loop couples LMs and formal provers to iteratively improve correctness and capability.
- 5Math-first formal verification has clear commercialization pathways in verified code, hardware, and other high-assurance domains.
- 6A mission-driven, niche research culture can attract specialized talent despite early fundraising and visibility challenges.
Notable Quotes
"The system designed to be 100% correct, 100% of the time, effectively solving the AI hallucination problem."
"We announced that Axiom Prover got a perfect score... 12 out of 12."
"That was probably the first AI to solve a research conjecture completely end-to-end and solverified. That means the outputs are fully verified 100% correct."
"Auto-formalization ... is harder than translation because you're translating something that cannot be verified (natural language) into something that can be."
""it's like two whales and just kind of realize that only they can communicate in that like frequency range.""
""fundraising was quite hard ... I'm a nobody no one should trust me with their large amount of money""
""we still feel like secret keeper we still feel like we cannot fully elaborate and emphasize the thing that we are seeing that is the next frontier of AI""
Episode questions
What is Lean and why is it central to Axiom's approach?
Lean is a formal programming language for mathematical proofs (via the Curry-Howard correspondence) that encodes proofs as machine-checkable programs; Axiom uses Lean to produce verifiable certificates of correctness so proofs can be checked automatically rather than trusted heuristically.
How did AxiomProver perform on the Putnam exam and why does that matter?
AxiomProver achieved a perfect 12/12 on the Putnam (with eight problems solved within the time limit) in a real-time run using the actual proctored exam; this matters because the Putnam is a notoriously difficult, timed competition and success demonstrates practical competence under contest conditions.
How does Axiom generate training data given Lean's scarcity?
They synthesize Lean data by auto-formalization of informal mathematics, use repair/fuzzing to create variants, and leverage verified outputs (checked by Lean) so synthetic examples are mathematically valid, mitigating the limited raw Lean corpus.
Can this formal verification approach generalize beyond math?
Yes — because Lean can express both mathematical and program properties, Axiom believes verified math reasoning can extend to code and hardware verification, offering commercial value in domains that require correctness guarantees (e.g., hypervisors, CPU verification, defense).