Computers already help mathematicians compute. The article asks whether they can help humans reason about proofs, and whether they might eventually reason on their own.

An expository overview of three developments: neural networks used to discover mathematical patterns, automated and interactive theorem provers, and large language models. The discussion of interactive provers centres on Lean and its library Mathlib, covering the Liquid Tensor Experiment, the sphere eversion formalization, and rapid formalization of additive combinatorics results. It also covers Lean tactics that call external systems (polyrith calls Sage, sagredo calls an LLM) and LLM systems that generate Lean proofs of olympiad-level problems.

Neural networks have helped mathematicians find new theorems and counterexamples. ITPs such as Lean now make it possible to formalize some modern research papers within months. LLMs have so far had little effect beyond school-level mathematics. The author argues that mathematicians should stay involved in guiding this area.