A 4-hour Interview with Carina Hong: AI for Math, Lean, Proofs from The Book, and Intuition
Carina Hong (洪乐潼), a 24-year-old Chinese-born founder, discusses her company Axiom, which recently closed a $200M Series A at a $1.6B valuation, focusing on AI for Math using formal proof systems like Lean. She shares her journey from competitive math olympiads in Guangzhou to MIT, Oxford, and Stanford, before dropping out to build an AI theorem-proving system that achieved the first-ever perfect score on the Putnam mathematics competition.
Summary
The interview is a comprehensive 4-hour conversation between host Xiaojun and Carina Hong (洪乐潼), founder and CEO of Axiom, conducted at the historic Facebook House in Silicon Valley. Carina, born in 2001 in Guangzhou, describes herself as a 'brute force' rather than 'gifted' mathematician, having struggled with Euclidean geometry in olympiad competitions while excelling at algebraic approaches.
Carina traces her mathematical journey from childhood in Guangzhou, where she attended elite math schools with competitive monthly ranking systems, through reading advanced mathematics textbooks in middle school as an escape from zero-sum competition. She describes developing a 'small tribe' of like-minded friends who would explore mathematics recreationally, playing knight's tour problems on chessboards. At MIT, she studied mathematics and physics as a double major, surrounded by IMO gold medalists she had idolized growing up, which reinforced her self-perception as the 'least talented' person in the room.
Her academic path continued with a Rhodes Scholarship to Oxford for neuroscience, where exposure to Demis Hassabis's computational neuroscience work at the Gatsby Institute redirected her toward AI. She then began a mathematics and law joint PhD at Stanford, where a constitutional law course about AI interpreting legal texts sparked the insight that if AI could parse structured legal language, it could do mathematics using formal proof systems like Lean.
The founding of Axiom is described as emerging from 18 months of conversations with Shubho Sengupta (former director at Meta AI Research) at a Verve coffee shop in Palo Alto, where they met by chance. After reading hundreds of AI for Math papers during the Christmas holiday of 2024, Carina spent two months convincing herself to start the company—she was deeply opposed to the startup culture—before beginning fundraising in January 2025. The seed round closed at a $300M valuation, raising $64M, and within seven months the company achieved a perfect score on the 2025 Putnam Mathematical Competition (the first AI to do so, and only the 6th perfect score in the competition's 98-year history), as well as solving several open research problems in formal mathematics.
On the technical side, Carina explains Axiom's approach: a system combining multiple AI models (trained via post-training/RLHF on Lean formal language data) with deterministic formal verification tools, avoiding expensive Monte Carlo Tree Search in favor of a subagent-based architecture. She identifies three core technical pillars: a Prover (formal theorem proving), a Conjecturer (generating mathematical hypotheses), and Auto-formalization (translating natural language mathematics into Lean code). She argues that math and code are 'twin brothers' linked by the Curry-Howard correspondence, and that formal verification can help solve hallucination problems in AI by providing binary correctness signals.
The team includes notable figures: Ken Ono (former tenured professor, number theorist who worked closely with Ramanujan's legacy), François Charton (pioneering AI for Math researcher from Meta), Evan Chen (US IMO team coach), and Kenny Lau (one of the original builders of Mathlib, Lean's mathematical library). Carina describes intercepting Ken Ono from an OpenAI offer by arguing Axiom was more focused on mathematics as a discipline.
On business model, Carina identifies hardware/chip verification as the most immediate market (citing Amazon's 3-year, 260,000-line formal verification project as evidence of demand), with broader software verification and AI for science as future directions. She envisions a transition from a 'math-poor' to 'math-rich' society, with AI enabling exponential growth in mathematical discovery.
Carina reflects extensively on her personal philosophy: she identifies as a 'visionary' entrepreneur type rather than executor or salesperson, describes being 'addicted to suffering' in the founder way, and traces her motivational shift from deriving energy from team camaraderie to deriving it from the difficulty of the problems themselves (catalyzed by COVID-era isolation at MIT). She concludes by describing herself as a 'student/apprentice' at heart, someone who would rather be a research scientist intern than CEO, and frames Axiom's mission as potentially creating the conditions for recursive self-improvement in AI mathematical reasoning.
Key Insights
- Carina argues that her 'brute force' mathematical style—using complex methods like the complex number method for geometry instead of elegant geometric insight—directly parallels how AlphaGeometry solved IMO geometry problems: by converting geometric figures into symbolic expressions rather than finding the beautiful geometric proof, achieving 81% of historical IMO geometry problems.
- Carina claims that Axiom's AxiomProver achieved a perfect score on the 2025 Putnam Mathematical Competition—the 6th perfect score in the competition's 98-year history and the first ever by an AI—and that for one problem where a human mathematician drew a single elegant diagram that immediately suggested the solution, the AI instead produced thousands of lines of Lean code through brute-force enumeration and case analysis, arriving at a completely different but valid proof.
- Carina describes the key technical insight behind Axiom's approach: that Monte Carlo Tree Search (used by AlphaProof) was too expensive given their seed funding, so they developed a subagent-based architecture that scales proof trees from 40 nodes to 4,000 nodes, and that a good AI theorem prover unexpectedly transfers to strong code verification capability—they achieved 98.93% on the Putnam Benchmark for code verification, compared to the previous SOTA of 11% from an older DeepSeek-Prover.
- Carina recounts that she met Shubho Sengupta (who became Axiom's CTO and co-founder) by coincidence at a Verve coffee shop in Palo Alto—she went there to read law school assignments and watch dogs on weekends—and they talked for 18 months about science and history before she asked if he wanted to co-found Axiom; she says she was too afraid to directly recruit him, preferring to wait until he chose it himself, which he did after many colleagues left Meta.
- Carina argues that auto-formalization—translating existing natural language mathematics into Lean formal code—is at least as hard as, and possibly harder than, theorem proving itself, because almost all existing mathematics lacks Lean definitions, making it impossible to even state many research problems formally; she cites the 'FrontierMath' challenge where Axiom could not attempt the 10 problems because the required mathematical objects weren't defined in Mathlib.
Topics
Full transcript available for MurmurCast members
Sign Up to Access