Mathematical reasoning and the computer
Kevin Buzzard
TL;DR
The paper surveys how computers have evolved from enabling calculation to supporting mathematical reasoning and potential proof-generation. It organizes the landscape into three pillars: neural networks as search aids and evidence providers, automated and interactive theorem provers that formalize and verify results, and large language models whose current capabilities may extend to mathematics with proper alignment to formal languages. Demonstrated successes include neural networks aiding knot theory and representation theory alongside reinforcement-learning–driven counterexample search, and landmark verifications by ITPs such as the Four Color Theorem and the Feit–Thompson theorem, with Lean's mathlib enabling near real-time formalization. The work emphasizes a future where interactive textbooks, domain-specific mathematical chatbots, and AI-assisted formalization become practical, while highlighting the need for human guidance to ensure correctness and relevance across subfields.
Abstract
Computers have already changed the way that humans do mathematics: they enable us to compute efficiently. But will they soon be helping us to reason? And will they one day start reasoning themselves? We give an overview of recent developments in neural networks, computer theorem provers and large language models.