Building an AI Mathematician

Carina Hong discusses building systems for mathematical reasoning and machine-verifiable proofs. The conversation explores Lean, the scarcity of formal mathematical training data, and translating natural-language arguments into formal statements. It also examines conjecture-and-proof self-play and applications of formal verification to software and hardware.