Mathematicians in the Age of AI
Summary
ArXiv essay explores how AI can prove both formal and informal mathematical results, and the implications for mathematicians, teaching, and collaboration. It discusses developments such as Mathlib, Lean, and AI-driven proving, and weighs concerns about credit, disruption, and how to harness AI to advance mathematics.