🔬Scaling Past Informal AI - Carina Hong, Axiom Math
June 3, 2026
AI Summary
5 min readAxiom Math: Formal Verification as a Path to Superintelligence
Carina Hong, CEO and founder of Axiom Math, joined the Latent Space podcast to explain why her company believes formal verification — long viewed as a tedious compliance tool — is actually the key to scaling AI reasoning capabilities. Axiom, which raised a $200 million Series A at a $1.6 billion valuation just seven months after founding, has positioned itself at the intersection of mathematics and AI, with a system that achieved a perfect score on the 2025 Putnam exam and became the first AI to prove research conjectures using formal verification.
What Formal Verification Actually Is
Lean is a formal language and proof assistant — a computer program where mathematical proofs can be written and mechanically checked for correctness. Unlike informal mathematical proofs written in natural language, Lean proofs compile like code. If the program compiles without errors, the proof is guaranteed correct, assuming no cheating tactics like "sorry" (which lets you take a statement as given without proving it).
Continue reading the full summary in the app — free to try.
Read Full Summary →Free • No credit card required
Never miss an episode of Latent Space: The AI Engineer Podcast
Get every new episode summarized in your inbox — free, ~5 minutes to read.
No spam. Unsubscribe anytime.
What you'll learn
- 1 (00:04) **Verified AI: From Human Collaboration to Scaling Brilliance** - Carina introduces the core thesis: verification is not about preventing hallucination but about compounding intelligence and enabling new forms of collaboration (human-AI, agent-agent).
- 2 (01:08) **Welcome and Axiom's Recent Milestones** - Carina Hong is introduced as CEO of Axiom Math, a company that achieved a perfect Putnam score and the first AI-proven research conjectures via formal verification.
- 3 (03:11) **The Market Thesis: Math as a Horizontal Infrastructure Layer** - Carina draws a parallel to early coding-focused AI (like Anthropic) being dismissed as a vertical, only to become a monopoly on reasoning.
- 4 (05:23) **Why Frontier Labs Aren't Doing Formal Verification** - Carina explains that internal politics and shifting strategic directions at big labs often prevent sustained focus on a long-term problem like formal verification.
- 5 (06:50) **What is Formal Verification? The Lean Proof Assistant** - Carina defines Lean as a formal language and proof assistant, distinct from its cousins like Isabelle or COQ.
- 6 (10:52) **Why Mathematicians Use Lean: Beyond Peer Review** - Carina explains that even though human peer review exists, Lean's tactics automate the "grind" of low-level proof steps, allowing mathematicians to focus on high-level intuition.
- 7 (11:56) **Lean as a Full Programming Language** - Carina clarifies that Lean is a complete functional programming language, not just a proof tool.
+ Full timestamped outline available in the app
Guests on this episode
Show Notes
In 2025, seven-month-old startup Axiom solved all 12 of the problems Putnam exam (scoring 8/12 in the time limit) a prestigious undergraduate math exam. The 12/12 score is better than the top undergraduates (110/120) and the closest AI system that reported a result (DeepSeek 103/120), although it is unclear what the people and other systems would have scored with more time. Nonetheless, the Putnam exam is legendary for its difficulty, with the median score typically being 0 or 1 points. Taken by itself, this seems like a minor feather in the cap of AI; one of a long series of accomplishments by AI systems in elite competitions with humans, starting with Deep Blue beating Kasparov.
Fast forward to mid-2026, and Claude Code is eating the world. In 2024 Anthropic’s bet on code and enterprise looked like a more pragmatic niche play vs. OpenAI’s better models and massive consume scale. Today, Amodei’s all in bet on acceleration via code (images and video be damned) seems prescient.
Despite Anthropic’s growing momentum, however, Axiom CEO Carina Hong sees coding ability as a necessary but not sufficient milestone on the path to AGI. Code arguably pushes the jagged frontier to the point of super intelligence in some domains outside of coding, but there are surprising gaps (link) that Carina believes will bottleneck AI progress. (Stats on math benchmarks).
The informal bottleneck
“Verified AI” sounds like eating broccoli (footnote: I actually love broccoli, but then again, I also believe strongly in Test Driven Development, so ¯\(ツ)/¯ ) and paying taxes, but to Axiom it means something very different. “Verification to me is about scaling brilliance, compounding brilliance,” Carina told us.
It actually took a while for me to understand what she means by this. It sounded like marketing-speak to me, until it clicked. Carina emphasizes an story about legendary mathematician Srinivasa Ramanujan to illustrate the point. When G.H. Hardy finally persuaded Ramanujan to formally prove theorems instead of relying on his (formidable) intuition, it reportedly improved his own capabilities. This is presumably because formally proving things forced Ramanujan to articulate the details in a way that open up new lines of thinking, etc. This is one part of “compounding.”
But formally proving things also allowed others to benefit from his intuition: the proofs are way of communicating an intuition and persuading others that the intuition is correct. This is scaling (more people use the result) and compounding (people can learn from and build on his work).
This is the analogy that Carina wants us to focus on.
Verified Generation
There are two ways that Verified AI shows up: in training and in inference.
But a quick detour: to a first approxi