Mathematical discovery in the age of artificial intelligence (www.nature.com)

Naskręcki and Ono argue that AI tools are already reshaping mathematical research and predict a deeper transformation of mathematical practice as those tools mature. They survey recent milestones — from formal proof efforts like the Lean community’s completion of the liquid tensor experiment and advances in automated deduction, to large-model systems that solve contest-style problems at a silver‑medal IMO level — to show how machine assistance is moving beyond low‑level computation into conjecture generation, proof search, and formal verification. The piece positions these developments as more than conveniences: they are altering what problems are tractable and how results are validated and communicated. Technically, the authors highlight a convergence of methods: symbolic automated theorem provers and proof assistants (for rigorous formalization), heuristic search and learning-based proof search, and large language models that suggest high‑level ideas or draft informal proofs. The implications include faster exploration of ideas, new hybrid workflows where humans curate and formally verify machine proposals, and shifting incentives toward verification, reproducibility, and transparency. Risks discussed include brittle or incorrect outputs, opaque reasoning in large models, and the need for shared benchmarks, tooling, and norms to integrate AI into mathematical rigor without eroding trust.