Carina Hong | AI That Can Prove It: From Mathematical Discovery to Verified Software

A eureka moment is a two-step process: discovering something new and surprising, and establishing that it is correct. Drawing on our work at Axiom, I 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. I 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.