Episode Summary
Executive Summary: Karina Hong, founder and CEO of Axiom, argues that AI for mathematics is at an inflection point because LLM reasoning, Lean 4 adoption, and code-generation/RL techniques are converging. The conversation centers on turning math into a programmable, verifiable domain via Lean, using auto-formalization and synthetic data to overcome severe data scarcity, and building a self-improving system where proving and conjecturing reinforce each other.
Main Topics: Why AI for math is happening now (Priority: 5/5): Karina says three trends align: stronger LLM reasoning, broader Lean 4 adoption, and code-generation methods that can be repurposed for formal math. Lean as the core formal language (Priority: 5/5): Lean is presented as the bridge that turns mathematical proofs into compilable programs with rigorous verification and feedback from errors. Auto-formalization and the data bottleneck (Priority: 5/5): The discussion emphasizes converting informal math into Lean as both a data-generation strategy and a core capability, but notes the difficulty of scaling it. Reinforcement learning for theorem proving (Priority: 4/5): RL is described as a major driver of recent progress in formal proving, with different labs using varying search and curriculum designs. Self-play, conjecturing, and self-improving AI (Priority: 5/5): Axiom’s vision includes a prover and conjecturer that interact in a loop, using proof success as reward signals and generating progressively harder problems. Mathematical discovery beyond Lean (Priority: 3/5): The team also works on specialized discovery problems and tools like PatternBoost, exploring areas where formalization is less central or insufficient. Commercial and product implications (Priority: 4/5): Karina argues that formal verification can unlock practical markets in software, hardware, and safety-critical systems, while the UI should hide Lean behind a natural-language interface.
Key Arguments: Math has not been ‘turned into programming language yet,’ and doing so will unlock new markets and use cases beyond current coding-focused AI. The convergence of LLM reasoning, Lean 4 adoption, and code-gen/RL methods makes the timing right for AI mathematicians. Lean provides a rigorous, compilable representation of proof steps, enabling provable guarantees when statements are correctly formalized. Auto-formalization is hard, but it is both a data engine and a modeling capability; proving and formalization should be trained together, not separately. The formal math ecosystem suffers from extreme data scarcity compared with code—Axiom cites a massive gap that makes pure scaling insufficient. Reinforcement learning has already produced strong formal-math systems, and curriculum design remains crucial because reward signals are sparse and problems vary in abstraction and creativity. Axiom’s long-term bet is a self-improving loop in which a prover validates conjectures and a conjecturer generates new ones, enabling continuous progress. Mathematics can serve as a sandbox for broader self-improving AI because it combines verification, creativity, and structured knowledge growth. Commercial value will come from formal verification of software and hardware, and potentially from broader safety-critical reasoning once the technology matures.
Data Points: Lean data vs Python data gap: ~10 million Lean tokens vs >1 trillion Python tokens (lower bound) - Used to illustrate the formal-math data scarcity relative to code; Axiom describes this as about a 100,000x gap. Estimated data gap: 100,000x - Axiom’s estimate of the difference between available Python code data and Lean data. Math archive size: 30 to 70 million - Karina estimates the number of statement-proof pairs in the mathematical archive that are not in Lean. Lean 4 release: September 2023 - Karina cites Lean 4’s rollout as a key catalyst for increased adoption and community momentum. Auto-formalizer limitation: ~5 lines - Axiom says an available demo auto-formalizer struggles beyond very short statements/proofs. Research duration example: About 6 months - Karina described being stuck on a hard research problem at MIT for roughly half a year. Time span of open conjectures: 130 years / 30 years - Examples from mathematical discovery problems discussed as being open for decades; one 30-year-old conjecture was found false.
Pivotal Quotes: "Math and coding are two important, or perhaps the two biggest part of digital world. And coding is heavily invested. Math is not." — Sam Charrington (opening framing): Sets up the episode’s thesis that mathematics is under-invested relative to coding despite its importance. "We believe in an AI mathematician being built by bringing three fields together, and that's AI, programming languages, and math." — Karina Hong: Karina summarizes Axiom’s core strategic thesis on the convergence driving the field. "By turning math into programming language, you really need a lot of the code gen techniques." — Karina Hong: Explains why code-generation and reinforcement-learning methods are central to Axiom’s approach.
Implications: AI for math is moving from niche research toward a platform shift: better formal verification, richer theorem-proving tools, and new product categories in software, hardware, and safety-critical systems. The near-term challenge is data and evaluation; the long-term prize is provable, self-improving reasoning systems.