Mathematical discovery

Ken Ono surveys how AI systems contribute to mathematical discovery, research-level reasoning and formal verification. Examples include AI-guided searches, progress on longstanding problems and formalization in Lean. The talk also examines reliability, attribution, unequal access, education and the future role of mathematicians. It argues for using AI to extend exploration while retaining mathematical judgment and strengthening trust through machine-checkable proofs.

…artificial intelligence might change mathematical discovery. The conversation also contrasts broad conceptual views with concentrated work on individual problems.

Jordan Ellenberg explores how machine learning might contribute to mathematical discovery. Drawing on collaborative work with DeepMind on a combinatorics problem, he considers the distinction between obeying formal rules and producing ideas that mathematicians judge important or ingenious, and discusses near-term changes to mathematical practice.