Mathematical & physical sciences · OECD FoS 1.1 · China MoE 0701 数学
Mathematics
数学
L3Systemic transformation ↑ Rising ↓ from L4 Score 2.90 · Last reviewed 2026-10-22 · Next review 2026-12-20
BIGGEST BREAKTHROUGH 2026-10-11 AI leapField leap
Banks: human-verified, explicit account of the OpenAI proof that Landau–Siegel zeros do not exist (arXiv 2610.15483) ↗
AI: an OpenAI model produced a proof of a near-century-old central problem; Banks verified it line by line, Kerr gave a simpler proof (arXiv 2610.21099), and the Lean formalisation was re-checked by two kernels. Field: Siegel zeros block effective bounds for primes in progressions and class numbers (not yet journal-refereed)
Why this level
Maths has the strongest AI-discovery record: in May 2026 an OpenAI model disproved Erdős’s 1946 unit-distance conjecture (a human-verified write-up by nine mathematicians incl. Alon, Gowers, Sawin), PNAS published AlphaEvolve’s 67-problem study, and a DeepMind agent resolved 9 open Erdős problems in Lean. Broad practitioner adoption and curriculum change have not happened, and openai/math saw withdrawals and push-back, so the composite is L3 (discovery scored 4).
↓ L4 → L3
S = 0.30·method + 0.35·discovery + 0.25·adoption + 0.10·education (education scores 0 when there is no evidence; if empty, the other weights are renormalised)
Sources
Composite 2.5–3.49 (or ≥3.5 with any of method/discovery/adoption below 3): AI is standard infrastructure with multiple independent breakthroughs. All levels →
Research directions
Formal proof (Lean)AutoformalizationLLM reasoning on open problemsEvolutionary search (AlphaEvolve)Competition maths
Papers
- An orthogonality inequality in $\mathbb{RP}^{n-1}$ and the double-cap conjecture
AI: per the abstract, AI assisted the paper and a separate Lean 4 proof of the main results was formalised almost entirely with AI tools. Field: settles the long-open double-cap conjecture and the measurable fractional chromatic number of the spherical orthogonality graph (preprint)
2026-10-20 · arXiv
-
AI leapField leap
On the OpenAI proof that Landau-Siegel zeros do not existAI: an OpenAI model produced a proof of a near-century-old central problem; Banks verified it line by line, Kerr gave a simpler proof (arXiv 2610.21099), and the Lean formalisation was re-checked by two kernels. Field: Siegel zeros block effective bounds for primes in progressions and class numbers (not yet journal-refereed)
2026-10-11 · arXiv
-
Field leap
An $O(1)$ Bound for the KLS ConstantAI: per Microsoft Research a human-directed agentic process explored 100+ approaches (AI role is self-reported). Field: KLS (1995) is a central problem of high-dimensional convex geometry; Bizeul–Klartag–Lehec independently proved it (arXiv 2610.05474), another explicit-constant proof appeared (arXiv 2610.07728), plus a Lean 4 formalisation; all preprints
2026-10-01 · arXiv
- Mathematical discovery and exploration can be done at scale
Large-scale AI maths discovery passes peer review in a top journal
2026-09-30 · Proceedings of the National Academy of Sciences
- Forbidden Sidon subsets of perfect difference sets, featuring a human-assisted proof
Peer-reviewed solution to an Erdős prize problem with a ChatGPT-generated Lean proof
2026-05-22 · Proceedings of the National Academy of Sciences
-
AI leap
Advancing Mathematics Research with AI-Driven Formal Proof SearchFirst large-scale evaluation on open problems with machine-checked Lean proofs at a few hundred dollars per problem
2026-05-21 · arXiv
-
Field leap
Remarks on the disproof of the unit distance conjectureIndependent expert verification is what makes the AI result count as mathematics
2026-05-20 · arXiv
- Olympiad-level formal mathematical reasoning with reinforcement learning
Peer-reviewed AlphaProof method (RL + Lean)
2025-11-12 · Nature
-
AI leap
Mathematical exploration and discovery at scaleCo-authored by Terence Tao; turns AI-driven construction search into a scalable method across fields
2025-11-03 · arXiv
- FrontierMath: A Benchmark for Evaluating Advanced Mathematical Reasoning in AI
Frontier models solved <2% at release; became the main yardstick for research-level AI maths
2024-11-07 · arXiv
- Solving olympiad geometry without human demonstrations
Near-gold olympiad geometry; competition, not research
2024-01-17 · Nature
-
AI leap
Mathematical discoveries from program search with large language modelsFirst LLM-found construction beating best-known human results on an open problem (cap sets)
2023-12-14 · Nature
- Advancing mathematics by guiding human intuition with AI
First top-journal demonstration that AI can help mathematicians conjecture and prove new theorems
2021-12-01 · Nature
- Generating conjectures on fundamental constants with the Ramanujan Machine
Automated conjecture generation for constants; some later proved
2021-02-03 · Nature
- The recent counterexamples to the Eisenbud-Schreyer-Weyman Ulrich problem (2003) and to Hochster's small Cohen-Macaulay conjecture (1973): a survey, with a generalization to arbitrary dimension
Surveys how four preprints and an AI-generated manuscript (Sept 2026) produced counterexamples to the Ulrich problem and Hochster’s small CM conjecture, generalised to all dimensions.
2026-10-21 · arXiv · Cristian Anghel
- An orthogonality inequality in $\mathbb{RP}^{n-1}$ and the double-cap conjecture
Proves caps minimise orthogonal-neighbourhood measure, yielding the double-cap conjecture; a separate Lean 4 proof was formalised almost entirely with AI tools.
2026-10-20 · arXiv · Allen Ibiapina, Carlos Gomes, Alan Pio, Samuel Belo
- Training with ML-labeled Data via Stochastic First- and Zeroth-Order Optimization
Studies training with ML-generated labels instead of costly human ground truth, via stochastic first- and zeroth-order optimisation.
2026-10-19 · arXiv · Maria-Eleni Sfyraki, Jun-Kun Wang
- Beyond Leaderboards: A Method for Application-Specific Capability Profiling of Large Language Models
A method and containerised testbed for profiling LLM capability per application (e.g. a database-migration agent), instead of generic leaderboards.
2026-10-19 · arXiv · Oleg Grynets, Vasyl Lyashkevych, Andrii Salyk, Dmytro Koziuberda
- Rózsa: Certified Equational Reasoning
A solver for the SAIR Mathematics Distillation Challenge that emits Lean certificates; solved 199/200, placing 6th.
2026-10-19 · arXiv · Georgios Kissas
- Studying proof data with proof theory: the case of AI-generated mathematics
Proposes proof-theoretic measures (proof-term size, redundant steps) to analyse large collections of formally verified, AI-generated proofs such as OpenAI’s.
2026-10-18 · arXiv · Safal Raman Aryal
- Gaussian Process Bandits with Paired Auxiliary Observations
AI-GPB uses cheap auxiliary data available beforehand to reduce variance in Bayesian optimisation of noisy black-box functions.
2026-10-17 · arXiv · Weibo Huang, Qing Feng, Ruihao Zhu, Cheng Hua
- An $O(1)$ Bound for the KLS Constant
Proves ψ_n ≤ C for a universal constant, resolving the KLS conjecture, and a universal Poincaré-constant bound; Microsoft says human-directed AI agents were used.
2026-10-01 · arXiv · Zhao Song, Xinzhi Zhang
- From arXiv, bioRxiv, medRxiv and OpenAlex (last ~30 days); summaries written by AIMap from the abstract.
- Kronecker Delta Rule for Long Context Linear Attention 2026-10-19
- MAI-Gym: An Open All-in-One Platform for GUI Agent Evaluation and RL Training across Mobile and Computer Environments 2026-10-14
- Recovering Reliable Supervision via Critique-Guided On-Policy Distillation 2026-10-14
- TPPO: Tracking-Value PPO For Language Model Reasoning 2026-10-12
- Questioning the Questions: Sustaining Self-Evolution in Reasoning Models 2026-10-03
- Sharpening Tax in Post-Training 2026-10-01
- All related papers in the archive →
Milestones 24· 9 leaps
Big glowing nodes are leaps: AI leap cool · Field leap warm · double ring = both
-
Paper ⓘ note
AI-assisted proof of the double-cap conjecture, with a separate Lean 4 proof formalised almost entirely using AI tools (arXiv 2610.27523)AI: per the abstract, AI assisted the paper and a separate Lean 4 proof of the main results was formalised almost entirely with AI tools. Field: settles the long-open double-cap conjecture and the measurable fractional chromatic number of the spherical orthogonality graph (preprint)
arXivPreprint -
Discovery ⓘ note
Quanta: number theorists largely accept OpenAI’s proof of a quasi-Riemann hypothesis (zeros between 1/12 and 11/12)AI: called “the most significant AI-for-math achievement so far” by Lichtman; Field: per Radziwiłł most consequences of RH already follow from quasi-RH. Still a preprint; human write-ups unpublished
Quanta MagazinePreprint -
Policy
Simons Foundation launches a $15M effort to help mathematicians navigate the AI eraA major funder dedicates money to vetting and absorbing AI-produced maths
Terence Tao -
PaperAI leapField leap ⓘ note
Banks: human-verified, explicit account of the OpenAI proof that Landau–Siegel zeros do not exist (arXiv 2610.15483)AI: an OpenAI model produced a proof of a near-century-old central problem; Banks verified it line by line, Kerr gave a simpler proof (arXiv 2610.21099), and the Lean formalisation was re-checked by two kernels. Field: Siegel zeros block effective bounds for primes in progressions and class numbers (not yet journal-refereed)
arXivPreprint -
Dataset
openai/math withdraws 3 manuscripts over a sign error and revises 143 withdrawn and 14 revised the next day
openai/math history -
Dataset
OpenAI releases openai/math on GitHub: 719 manuscripts, 372 families, ~42% Lean-formalized719 AI maths manuscripts, ~42% Lean-backed; withdrawals and push-back
OpenAIVendor claim -
DiscoveryField leap ⓘ note
Song & Zhang prove the 31-year-old Kannan–Lovász–Simonovits conjecture with human-directed AI agents (arXiv 2610.01447); Bizeul–Klartag–Lehec give an independent proof built on their criterion (arXiv 2610.05474)AI: per Microsoft Research a human-directed agentic process explored 100+ approaches (AI role is self-reported). Field: KLS (1995) is a central problem of high-dimensional convex geometry; Bizeul–Klartag–Lehec independently proved it (arXiv 2610.05474), another explicit-constant proof appeared (arXiv 2610.07728), plus a Lean 4 formalisation; all preprints
arXivPreprintVendor claim -
Paper
PNAS publishes the AlphaEvolve mathematical-discovery paper (Tao et al.)Large-scale AI maths discovery passes peer review in a top journal
PNAS -
Competition
IMO 2026: AxiomProver scores 42/42 with Lean proofsPerfect IMO 2026 score with public Lean proofs; IMO results exclude AI
Axiom MathVendor claim -
Competition
IMO 2026: dots-note-3.0 reports committee-graded 42/42Vendor claim only
dots.aiVendor claim -
Paper
PNAS: $1,000 Erdős prize problem resolved, Lean proof generated by ChatGPTPeer-reviewed solution to an Erdős prize problem with a ChatGPT-generated Lean proof
PNAS -
PaperAI leap ⓘ note
DeepMind formal proof-search agent autonomously resolves 9 of 353 open Erdős problems and 44/492 OEIS conjectures in LeanFirst large-scale evaluation on open problems with machine-checked Lean proofs at a few hundred dollars per problem
arXivPreprint -
PaperAI leapField leap ⓘ note
Unit-distance conjecture disproved: an OpenAI general reasoning model constructs point sets with n^{1+ε} unit distances~80-year-old flagship problem; proof checked and rewritten by nine outside mathematicians (arXiv 2605.20695); Sawin improved ε to 0.014
OpenAIVendor claim -
PaperField leap ⓘ note
“Remarks on the disproof of the unit distance conjecture”: human-verified, simplified proof by nine mathematiciansIndependent expert verification is what makes the AI result count as mathematics
arXivPreprint -
Paper
AlphaProof paper: olympiad-level formal reasoning with RL (Nature)Peer-reviewed AlphaProof method (RL + Lean)
Nature -
PaperAI leap ⓘ note
AlphaEvolve at scale: 67 problems, several best-known constructions improved; 11-D kissing number 592→593Co-authored by Terence Tao; turns AI-driven construction search into a scalable method across fields
arXiv（Georgiev、Gómez-Serrano、Tao、Wagner）Preprint -
CompetitionAI leap
Gemini Deep Think officially graded gold at IMO 2025 (35/42)First AI gold officially graded by the IMO (35/42)
Google DeepMind -
SystemAI leap
AlphaEvolve improves 4×4 complex matrix multiplication and dozens of problems48-multiplication 4×4 complex matrix product improves on Strassen (1969)
Google DeepMind -
Benchmark
FrontierMath: research-level maths benchmark written by expert mathematicians (Epoch AI)Frontier models solved <2% at release; became the main yardstick for research-level AI maths
arXivPreprint -
Competition
AlphaProof + AlphaGeometry 2 reach IMO 2024 silver-medal scoreFirst medal-level IMO score (silver), some problems took days
Google DeepMind -
Paper
AlphaGeometry solves olympiad geometry near gold level (Nature)Near-gold olympiad geometry; competition, not research
Nature -
PaperAI leap
FunSearch finds new cap-set constructions with an LLM (Nature)First LLM-found construction beating best-known human results on an open problem (cap sets)
Nature -
Paper
ML guides mathematicians’ intuition to new results in knot theory and representation theory (Nature)First top-journal demonstration that AI can help mathematicians conjecture and prove new theorems
Nature -
Paper
The Ramanujan Machine: algorithmically generated conjectures on fundamental constants (Nature)Automated conjecture generation for constants; some later proved
Nature
No milestones match this filter.
More papers & repos 16
Latest news 12
- The crisis of AI-generated mathematicsarXiv math.HOenPaperPreprint
- Studying proof data with proof theory: the case of AI-generated mathematicsarXiv cs.LOenPaperPreprint
- Formalization of R\'{e}nyi Differential Privacy in Isabelle/HOL (Draft version)arXiv cs.LOenPaperPreprint
- AHM Statement on OpenAI’s October 6 Release of Mathematical DocumentsTerence Tao blogen
- Sharing AI progress in mathematicsOpenAI Newsen
- AI just solved an 80-year-old ‘Erdős problem,’ and mathematicians are amazedScientific Americanen