Monday, October 19, 2026 / 12:00pm to 1:00pm Pacific Time
Carina Hong | AI That Can Prove It: From Mathematical Discovery to Verified Software
- Hybrid
- Seminar
The DEL Seminar Series is proud to host a diverse roster of bright minds from around the world to discuss various subjects surrounding economics and technology.
On October 19, 2026, Carina Hong, CEO of Axiom, will stop by the lab for our seminar series.
Abstract
A eureka moment is a two-step process: discovering something new and surprising, and establishing that it is correct. Drawing on her work at Axiom, Carina will discuss the transition from solving mathematical benchmarks to contributing to research, and from proving individual theorems to formalizing mathematical theories in Lean. At this scale, success requires more than proof search: agents must discover useful lemmas, manage dependencies, and assemble independently verified contributions into a coherent whole.
The central theme is verification for generation: using specifications, proof obligations, and verifier feedback to guide generation, not merely check its output. Carina will explore the economics of agent swarms in this setting: how to allocate compute across competing strategies, when additional agents improve performance, and how coordination costs and shared libraries of verified results shape returns to scale.
These questions connect large-scale mathematical formalization to the future of software engineering, where agents develop specifications, implementations, and correctness proofs together. The goal is not simply to generate more code, but to build systems whose components can be composed, optimized, and maintained while preserving explicit correctness guarantees. Human judgment remains central: choosing the right abstractions, specifying intended behavior, and ensuring that what we prove is what we actually need to know.
Carina Hong
Founder, Axiom Math
Carina Hong is the founder and CEO of Axiom, an AI company building a self-improving, superintelligent reasoner, starting with an AI mathematician. As a Rhodes Scholar at Oxford’s Hertford College, she earned a neuroscience master’s with dissertation distinctions and conducted deep learning research at UCL Sainsbury Wellcome Center Gatsby Unit. As an MIT math and physics undergrad, she published 9 papers in peer-reviewed journals spanning number theory, combinatorics, theoretical computer science, and probability. Carina won the AMS-MAA-SIAM Morgan Prize (the world’s highest honor for undergraduate mathematics research) and the AWM Schafer Prize (awarded to one undergraduate woman in math in North America).