AI for mathematics: a landscape review
AI is not replacing mathematicians — but it is fundamentally changing the pace and character of mathematical discovery. Three distinct paradigms have matured since 2024: evolutionary search for explicit constructions, machine-checked formal proof, and LLM-assisted reasoning. Each addresses different problems, requires different skills, and is at a different stage of accessibility. For Sheffield, the audience is specialised but the opportunity is real: a small number of researchers in pure mathematics, combinatorics, theoretical CS, and computational physics stand to gain significantly from tools that are either free today or will become generally accessible within two years.
The three paradigms
1. Evolutionary and constructive search — AlphaEvolve
What it does: Uses an LLM-guided evolutionary algorithm to search program space for Python functions that construct mathematical objects satisfying a quantitative scoring criterion. The system proposes, mutates, recombines, and scores thousands of candidates per run.
What it has achieved: Google DeepMind’s alphaevolve has solved 67 open mathematical problems across combinatorics, algebra, and geometry — improving the best-known cap-set bound, tightening matrix multiplication tensor rank, and discovering extremal graph constructions. Results are reproducible: the discovered programs are published under Apache 2.0 on GitHub. The same system has found production optimisations in Google’s TPU scheduling and data-centre routing.
What it cannot do: AlphaEvolve is not a theorem prover and produces no formal proofs. It is limited to constructive existence problems — finding an explicit object that satisfies numerical criteria. Problems requiring a non-constructive argument, or where no computable scoring function exists, are out of scope.
Accessibility: Early Access Programme only; no self-service; no public pricing. Realistic general availability: 2027 or later.
2. Formal proof and verification — Harmonic Aristotle / AlphaProof
What it does: Converts mathematical statements to formal Lean 4 proofs that are machine-checked and hallucination-free. Unlike LLM reasoning, a successful Lean proof is definitionally correct — the proof checker cannot be fooled.
What it has achieved: harmonic-aristotle solved all six IMO 2025 problems. Google DeepMind’s AlphaProof won a silver medal at the 2024 International Mathematical Olympiad (IMO), the first AI result at that level. Both systems demonstrate that automated formal proof has crossed a threshold from research curiosity to genuine research instrument.
What it cannot do: Formal proof systems require problems to be formalised in Lean 4, a non-trivial intellectual step that sits entirely with the human researcher. Coverage of Mathlib (the Lean 4 mathematical library) has gaps — reliability is lower in topology, probability, and functional analysis than in algebra and number theory. Proof jobs for hard results can take hours.
Accessibility: Harmonic Aristotle is free today via API key — the most immediately accessible tool in this space for Sheffield researchers.
3. Reasoning and conjecture assistance — general-purpose LLMs
What it does: LLMs (Claude, ChatGPT, Gemini) serve as interactive research partners for mathematical intuition, literature review, counterexample search, code generation, and LaTeX drafting — what Terence Tao has called a “trustworthy, knowledgeable co-author who never tires”.
What it has achieved: While LLMs cannot reliably produce correct proofs unassisted, mathematicians at the frontier (Tao, Gowers, Lean community) report substantial productivity gains from using them for exploratory work, checking intuitions, and handling the computational labour of formalisation. The key insight from Tao’s public commentary is that LLMs are most valuable not as oracles but as accelerators of iteration — generating ten plausible approaches quickly so the human can identify which one is worth pursuing.
What it cannot do: LLMs hallucinate mathematical content confidently. Every claim in LLM-assisted mathematical work requires independent verification. They are not a substitute for mathematical expertise; they amplify it.
Accessibility: Available now via institutional ChatGPT/Claude licences and free tiers. No specialist setup required.
What has changed since 2024
| Milestone | Date | Significance |
|---|---|---|
| AlphaProof IMO 2024 silver medal | July 2024 | First AI result at IMO level — formal proof, not just pattern matching |
| AlphaEvolve solves 67 open problems | November 2024 (arXiv 2511.02864) | Constructive search at scale; production results in Google infrastructure |
| Harmonic Aristotle IMO 2025 gold | July 2025 | Formal proof surpasses IMO gold standard on all six problems |
| Harmonic $120M Series C | November 2025 | Commercial viability signal; formal proof is not a research curiosity |
| AlphaEvolve public blog / paper | May–June 2025 | First public documentation of the evolutionary search architecture |
The cumulative effect is a step-change in what automated mathematical reasoning can do. Before 2024, AI assistance in mathematics was mostly confined to literature search and code generation. By mid-2025, machine-checked proofs at IMO gold level and automated discovery of previously unknown mathematical constructions are both demonstrated facts.
Relevance to Sheffield
Who benefits now
| Audience | Tool | Why |
|---|---|---|
| Pure mathematicians (algebra, number theory) | harmonic-aristotle | Free, available, best Mathlib coverage in these areas |
| Combinatorists, extremal graph theorists | alphaevolve (when available) | Directly addresses constructive existence problems |
| Formal methods / CS verification groups | harmonic-aristotle | Lean 4 is already a known quantity in this community |
| Computational physicists | get-physics-done | Physics-specific equation solving and simulation assistance |
Who should monitor (12–24 months)
- Applied mathematicians and statisticians — as LLM mathematical reasoning improves and AlphaEvolve broadens its domain coverage
- Engineering researchers — AlphaEvolve’s demonstrated results in algorithm and hardware optimisation are directly relevant
- Mathematics educators — formal proof tools have significant potential for pedagogy and graduate supervision
Barriers to adoption
- Formalisation overhead — using either AlphaEvolve or Harmonic Aristotle requires translating research problems into formal representations (Python evaluation functions or Lean 4 statements). This is non-trivial and requires upfront investment.
- Early access constraints — AlphaEvolve is not self-service. Until general availability, only researchers who apply to the Early Access Programme can evaluate it.
- Governance gaps — both tools involve sending problem statements to US-hosted cloud services. No University of Sheffield DPA review has been performed for either. This matters most for unpublished results and sensitive research data.
- Small specialist audience — unlike general writing or literature review tools, the audience for AI-assisted formal mathematics at Sheffield is probably in the tens, not hundreds. High value per user, but narrow reach.
Recommended actions
Immediate (now)
-
Point relevant staff to harmonic-aristotle — it is free, available today, and the most battle-tested AI formal proof tool. The primary audience is the Mathematics department (algebra, number theory, combinatorics) and the Verification group in Computer Science. No institutional procurement is required; individual researchers can sign up via API key.
-
Share this report with the Mathematics department — the Tao interview transcript and the arXiv 2511.02864 paper together make a compelling case for why now is a good time to engage with these tools. Faculty are likely already aware of the IMO results; this provides institutional context.
Near-term (Q2–Q3 2026)
-
Apply to AlphaEvolve Early Access Programme — identify one or two research groups with suitable problems (combinatorics, theoretical CS, computational physics) and support an application. Even if unsuccessful, this builds awareness and relationship with Google DeepMind.
-
Commission a GDPR/DPA review — before any formal recommendation to use AlphaEvolve or Harmonic Aristotle with unpublished research data, IT Services / Research IT should review the data processing terms for both platforms.
-
Assess get-physics-done for computational physics applications — this tool occupies a complementary niche (simulation and equation solving) and may have wider reach in the Faculty of Engineering.
Strategic (2027+)
- Revisit AlphaEvolve for institutional access once general availability is announced — the research-impact potential is high and the tool is likely to become a standard instrument for quantitative mathematical research.
Cross-references
Tool notes in this catalogue covering the AI-for-mathematics space:
- harmonic-aristotle — formal theorem proving via Lean 4; free, available now;
assess - alphaevolve — evolutionary constructive search; early access only;
assess - get-physics-done — physics-focused equation solving and simulation;
assess - google-co-scientist — general scientific hypothesis generation; stub only
Update — March 2026
Since this report was drafted, Google DeepMind published Aletheia (arXiv:2602.10177), a multi-agent natural-language research system that represents a fourth paradigm beyond the three described here.
Key results from the Aletheia paper:
- First fully AI-generated publication-grade mathematics paper (Feng26, arithmetic geometry) — classified Level A2 under the paper’s own Autonomy Levels taxonomy.
- Four open Erdős conjectures resolved autonomously (from a deployment across 700 open problems).
- 6 of 10 research-level problems solved on the FirstProof benchmark; one at publication grade.
This materially changes the landscape described above. The “reasoning and conjecture assistance” paradigm (Section 3) has advanced significantly further than the characterisation here implies. Aletheia is not publicly available, but the underlying Gemini Deep Think model increasingly is.
See aletheia-autonomous-maths-2026 for full analysis and Sheffield-specific recommendations.
Sources
- arXiv 2511.02864 — Georgiev, Gómez-Serrano, Tao, Wagner: “Mathematical Exploration and Discovery at Scale” (2024)
- arXiv 2506.13131 — AlphaEvolve primary architecture paper (2025)
- DeepMind blog: “AlphaEvolve — a Gemini-powered coding agent for designing advanced algorithms” (May 2025)
- Terence Tao interview with Dwarkesh Patel — views on AI as a mathematical research instrument (2025)
- New Scientist and Wired coverage of AlphaEvolve and AI-for-mathematics (2025)
- GitHub: google-deepmind/alphaevolve-results
- Harmonic Aristotle IMO 2025 results: https://github.com/harmonic-ai/IMO2025
Drafted: 2026-03-24 · Branch: agent/2026-03-24-get-physics-done · Requires human review before promotion to main