Building an AI Mathematician with Carina Hong - #754

What It Covers

Carina Hong, founder of Acxiom, explains building AI mathematicians through formal verification using Lean programming language, combining auto-formalization, theorem proving, and self-play systems to achieve mathematical reasoning with provable guarantees.

Key Questions Answered

• •Data Scarcity Challenge: Formal math has only 10 million Lean tokens versus one trillion Python tokens, creating a 100,000x data gap that requires auto-formalization and synthetic generation to bridge for effective model training.
• •Three Convergence Factors: AI mathematicians become viable now through post-training reinforcement learning advances, Lean 4 adoption since September 2023, and code generation techniques crossing performance thresholds that transfer to mathematical proving.
• •Self-Play Architecture: Acxiom builds systems where provers and conjecturers interact, with provers providing reward signals for conjectures, creating self-improving loops that expand mathematical knowledge bases through verification and proposal cycles.
• •Auto-Formalization Limitations: Current models struggle to convert natural language proofs longer than five lines into Lean without human intervention, with no established benchmarks for measuring statement formalization accuracy beyond syntax checking.