Mathematical discovery in the age of artificial intelligence [pdf] (uva.theopenscholar.com)

Naskręcki and Ono argue that AI is already reshaping mathematical practice by automating literature review, calculations, proof checking and—even in some cases—creative problem solving. Recent chatbots (Harmonic’s Aristotle, an undisclosed OpenAI GPT, Google DeepMind’s Gemini) have achieved IMO‑medal performance, while DeepMind’s Alpha projects (AlphaTensor, AlphaEvolve, AlphaProof, AlphaGeometry) and reinforcement‑guided models have optimized algorithms and tackled Olympiad‑level theorems. Parallel advances in formalization—proof assistants such as Lean (with the extensive mathlib), Coq and Isabelle—have even enabled full formalizations of highly technical results (notably a theorem by Peter Scholze), and automated pipelines are beginning to translate papers into machine‑verifiable proofs. The authors highlight a practical roadmap and cautionary constraints: scale up formalization efforts, improve LLMs for rigorous mathematical reasoning, and train mathematicians to operate AI toolchains. Key technical implications include the rise of autoformalization (LLMs translating informal reasoning into formal proofs), a verification bottleneck (machine outputs still need human validation), and emergent, sometimes inexplicable model strategies that experts can verify but not fully explain. Community initiatives (DARPA’s expMath, workshops, benchmarks like Epoch and FrontierMath) aim to keep progress grounded in human creativity. While AI may not imminently resolve deep open problems alone, it promises to make formal verification mainstream, raise standards for correctness, and reframe mathematicians’ roles toward higher‑level insight and oversight.