From prompts to proofs to people

In this talk, I’ll share three stories about how my collaborators and I have solved open problems using AI. These experiences capture a core message: AI can provide a key idea beyond your expertise and deliver a Lean-certified proof you can trust, but then leave you struggling to understand why it works. This motivates a more social approach to math research in which we bring AI-generated breakthroughs to the chalkboard and wrestle with the mathematics together.