Software:List of mathematical discoveries by artificial intelligence

From HandWiki
Short description: none

Template:Use dmy Beginning in the mid-2020s, large language models, including reasoning models, have made increasing progress in generating mathematical proofs at research level.[1][2][3] Most such proofs have been conducted using models from OpenAI and Anthropic. This is a list of notable discoveries conducted primarily by such models.

The degree of human intervention in AI-generated mathematical proofs may vary and remain unclear. Subjects responsible for publishing such proofs, including individuals and AI companies such as OpenAI, often fail to disclose used prompts, structure of pipelines used as a model workflow, or specific models used for generating proofs. The publication of such proofs may not satisfy standards of science articles. It may not have passed independent review or peer review, and instead be published on corporate websites, personal websites, or social media.

2023

2024

  • In October 2024, researchers at Meta and the Ecole des Ponts et Chaussees found pre-trained Seq2seq transformers could discover new global Lyapunov functions at a higher rate than non-AI systems.[6]

2025

  • In May 2025, Google DeepMind's AlphaEvolve agent discovered an optimization for the Strassen algorithm, reducing the scalar multiplications needed for 4x4 matrices from 49 to 48. It also improved the lower bounds for 11 kissing numbers.[7]
  • In September 2025, Math Inc.'s Gauss agent formalized the strong prime number theorem in Lean, producing ~25,000 lines of code and formally proving >1,000 theorems.[8]
  • In November 2025, researchers at Chinese universities constructed a reinforcement learning algorithm which improved the lower and upper bounds for 15 kissing numbers.[9]

2026

Q1

Q2

  • In May 2026, Google DeepMind used an AlphaEvolve-like model, adapted for mathematical proofs, to prove nine Erdős problems and 44 out of 492 formalized OEIS conjectures.[14] Epoch AI then used various LLMs to prove/disprove 147 of these 492 OEIS conjectures.[15]
  • In May 2026, OpenAI announced an internal model produced a disproof of the unit distance problem,[16] and several mathematicians collaborated to produce a verification and exposition of the result.[17]
  • In May 2026, Max Grinzstajn prompted GPT-5.5 Pro to discover a counterexample for Borsuk's conjecture in dimension n = 63, the smallest dimension for which a counterexample is known.[18][19]

Q3

Time period AI provenance Area of mathematics Topic People Formal status Source
July 2026 GPT-5.6 Sol Ultra graph theory proof of the cycle double cover conjecture OpenAI Sang-il Oum and Jim Geelen published independent expositions of the argument.[20][21] OpenAI published an article which proved the conjecture which states that every bridgeless graph has a collection of cycles covering every edge exactly twice.[22]
July 2026 GPT-5.6 Pro combinatorial optimisation counterexample to the Dinitz–Garg–Goemans conjecture Dmitry Rybin Counterexample published. On 22 July, Rybin presented on X a counterexample[23][24] in which a fractional flow of 58 exists, yet every unsplittable flow that meets the capacity bound costs at least 60. The disproof establishes that the theorem's capacity guarantee and a matching cost guarantee cannot always be achieved simultaneously by a single flow.[25]
July 2026 GPT-5.6 Sol matrix analysis proof of Crouzeix's conjecture Shanmu Jin Anne Greenbaum, Alex Townsend and Michel Crouzeix reviewed the proof and considered it to be correct.[26] An independent proof by Emiel Lorist and Felix Schwenninger, also developed with AI assistance, was published a week later.[27] On 27 July, Jin posted a preprint claiming a proof of Crouzeix's conjecture.[28] Three days later, Alex Townsend found the preprint using GPT 5.6 and checked the proof.[26]
August 2026 unreleased version of GPT-6 Astra group theory construction establishing the existence of non-sofic groups OpenAI Lean formalization[29] On 1 August, OpenAI posted a proof that the unit group L𝔽2(1,2)×of the binary Leavitt path algebra is non-sofic.[30]
August 2026 unreleased version of GPT-6 Astra geometry partial proof of Ehrhart's volume conjecture OpenAI Lean formalization[29] On 1 August, OpenAI posted a proof establishing the upper bound to Ehrhart's volume conjecture, that Vol⁡(K)≤(n+1)n/n!.[30] The equality case is still open.
August 2026 unreleased version of GPT-6 Astra complexity theory proof of the NP-hardness of the closest vector problem OpenAI Lean formalization[29] On 1 August, OpenAI posted a proof that approximating the Euclidean closest vector problem in dimension n within a factor of n1/400 is NP-hard.[30]
August 2026 OpenAI GPT-5.6 Pro[31] complex analysis proof of Sendov's conjecture for all degrees n ≥ 2 Lech Mazur Lean formalization[32] On 3 August, Mazur posted a paper on X claiming a proof of Sendov's conjecture for all degrees n≥2.[33] Terence Tao examined and streamlined the argument, produced a separate and shorter Lean formalization, and noted the proof also established the stronger Phelps–Rodriguez conjecture.[34][35]
August 2026 unreleased research version of Claude analytic number theory proven share of Riemann zeta function zeros on the critical line increased from 41.6% to 67.25% Jarred Sumner and Anthropic Lean formalization[36] On 10 August, Anthropic announced that it had made progress on increasing the bound for the fraction of zeroes of the Riemann zeta function from 41.6% to 67.25%.[37][38][39]
August 2026 unreleased version of Claude combinatorics Hadamard matrices constructed for the twelve orders below 2000 for which none were previously known Levent Alpöge, Philippe Voinov and Saul Reynolds-Haertle Computer-verified constructions On 12 August, Alpöge posted constructions for Hadamard matrices for twelve unresolved orders: 668, 716, 892, 1132, 1244, 1388, 1436, 1676, 1772, 1916, 1948 and 1964. The smallest of those, 668, had been the smallest open case of the Hadamard conjecture since 2005. The conjecture itself, which concerns all orders divisible by four, remains open.[40][41]
August 2026 unreleased version of Claude diophantine geometry two elliptic curves with the largest known rank (at least 30 and 31, respectively Levent Alpöge and Ava Howell The elliptic curves have the 30 and 31 independent basis points with infinite order listed.[42][43] On 20 August, an elliptic curve of rank at least 30 was posted to the Elliptic Curve Rank Leaderboard, with the solution credited to Alpöge and Howell. On 23 August, an elliptic curve of rank at least 31 was posted. These curves broke the previous known record of rank at least 29.[44][45]
August 2026 Claude complex manifolds the 6-sphere admits a complex structure Levent Alpöge the claim has not yet been independently verified If confirmed, this would resolve the old Hopf problem.[46]
August 2026 GPT-5.6 Sol prime numbers an improvement on the Erdős–Rankin conjecture (Erdős Problem 4). DottedCalculator (pseudonym) claiming authorship of a paper by uploaded a paper to Github Lean formalization According to the paper, there are infinitely many gaps gn=pn+1−pn between primes such that gn>c log⁡n log⁡log⁡nlog⁡log⁡log⁡log⁡n for some constant c>0. This improves on the original proof of the conjecture by Ford, Green, Konyagin, Maynard and Tao from 2014. According to Green, the new result uses a new but relatively elementary approach that would have been strong enough to independently solve the original problem without their 2014 paper, but which could have been discovered in the 1960s.[47][48]
August 2026 OpenAI prime numbers progress on prime gaps ? result has not yet been independently verified Claim to have proved there are infinitely many prime numbers that are at most 186 apart, an improvement on the previous bound of 246 that was established in 2014 by the Polymath Project. The OpenAI r.[49]
September 2026 Anthropic percolation theory proof of the dying percolation conjecture Ahmed Bou-Rabee Lean formalization[50] The result was obtained by proving an equivalent conjecture by Gady Kozma and Shaha Nitzan. Building on the result, Ahmed Bou-Rabee from the University of Pennsylvania published a claimed proof of the remaining Kozma-Nitzan conjectures, which he found the following day with ChatGPT Sol 5.6 Ultra and formalized in Lean with Claude Fable 5.1.[51]
September 2026 Anthropic, Claude number theory complete computer-checked proof of Fermat's Last Theorem Peng Tianyi Lean formalization Written over 11 days. It formalizes a simplified version of the original proof found by Andrew Wiles in 1994. Work on formalizing the theorem had started early in the century. The proof in Lean is 13 million lines long, the largest Lean proof written to date, and 29,500 theorems were formally proved for this task.[52][53][54]
September 2026 Epoch AI, GPT-6 Astra ring theory disproof of the Köthe conjecture Tom Adamczewski, Bernhard Böhmler, Rene Marczinzik Lean formalization[55] An exposition of the proof was posted by ring theorists Bernhard Böhmler and Rene Marczinzik.[56][57]
September 2026 Epoch AI, GPT-6 Astra probability theory disproof of the Ibragimov–Iosifescu conjecture for φ-mixing sequences Tom Adamczewski Lean formalization[58]; independent review pending GitHub repository
September 2026 Epoch AI, GPT-6 Astra graph theory counterexample to an eternal domination conjecture William Klostermeyer ? [59]
September 2026 Epoch AI, GPT-6 Astra combinatorics proof of the Dittert conjecture Tom Adamczewski Lean formalization[60]
September 2026 Epoch AI, GPT-6 Astra number theory counterexample to the n = 4 case of the N conjecture Tom Adamczewski Lean formalization[61] the only remaining open case
Further information: Navier–Stokes priority controversy

In September 2026, OpenAI claimed an internal model more powerful than GPT-6 Astra had solved the Navier–Stokes existence and smoothness problem, one of the Millennium Prize Problems. The claim has not been verified by the wider mathematical community. The credit for the discovery is disputed.[62][63]

See also

References

  1. ↑ "The Open Proof Corpus: A Large-Scale Study of LLM-Generated Mathematical Proofs" (in en). 14 January 2026. https://arxiv.org/html/2506.21621v2. 
  2. ↑ Chojecki, Przemyslaw (2025-12-08). "Mathematics in the Age of Large Language Models". https://www.ulam.ai/research/deepalgebra2.pdf. 
  3. ↑ Lee, Melissa (2026-08-09). "Generative AI has changed mathematics forever. Where to from here?" (in en-US). https://theconversation.com/generative-ai-has-changed-mathematics-forever-where-to-from-here-288954. 
  4. ↑ Romera-Paredes, Bernardino; Barekatain, Mohammadamin; Novikov, Alexander; Balog, Matej; Kumar, M. Pawan; Dupont, Emilien; Ruiz, Francisco J. R.; Ellenberg, Jordan S. et al. (14 December 2023). "Mathematical discoveries from program search with large language models" (in en). Nature (Nature Publishing Group) 625 (7995): 468–475. doi:10.1038/s41586-023-06924-6. PMID 38096900. 
  5. ↑ Paredes, Alhussein Fawzi and Bernardino Romera (2023-12-14). "FunSearch: Making new discoveries in mathematical sciences using Large Language Models" (in en). https://deepmind.google/blog/funsearch-making-new-discoveries-in-mathematical-sciences-using-large-language-models/. 
  6. ↑ "Global Lyapunov functions: a long-standing open problem in mathematics, with symbolic transformers" (in en). 10 October 2024. https://arxiv.org/html/2410.08304v1. 
  7. ↑ "AlphaEvolve: A Gemini-powered coding agent for designing advanced algorithms" (in en). 2025-05-14. https://deepmind.google/blog/alphaevolve-a-gemini-powered-coding-agent-for-designing-advanced-algorithms/. 
  8. ↑ "Introducing Gauss, an agent for autoformalization" (in en). https://math.inc/gauss. 
  9. ↑ Ma, Chengdong; Zhaowei, Théo Tao; Li, Pengyu; Liu, Minghao; Chen, Haojun; Mao, Zihao; Li, Bo; Cheng, Yuan; Qi, Yuan (17 November 2025). "Finding Kissing Numbers with Game-theoretic Reinforcement Learning". arXiv:2511.13391v4 [cs.LG].
  10. ↑ "Semi-Autonomous Mathematics Discovery with Gemini:A Case Study on the Erdős Problems". 5 February 2026. https://arxiv.org/html/2601.22401v3. 
  11. ↑ Skuse, Benjamin (2 March 2026). "Watershed Moment for AI–Human Collaboration in Math > Twenty-first-century Fields Medal proof formalized for the first time" (in en). https://spectrum.ieee.org/ai-proof-verification. 
  12. ↑ "Completing the formal proof of higher-dimensional sphere packing" (in en). https://math.inc/sphere-packing. 
  13. ↑ "Reinforced Generation of Combinatorial Structures: Ramsey Numbers". 10 March 2026. https://arxiv.org/html/2603.09172v5. 
  14. ↑ "Advancing Mathematics Research with AI-Driven Formal Proof Search" (in en). 21 May 2026. https://arxiv.org/html/2605.22763v1. 
  15. ↑ "OEIS Open: How many conjectures can language models turn into theorems?". 13 August 2026. https://arxiv.org/html/2608.11941. 
  16. ↑ Wexler, Ellen (3 June 2026). "Mathematicians Puzzled Over a Famous Problem for 80 Years. Now, They've Used A.I. to Identify a Clever Solution" (in en). https://www.smithsonianmag.com/smart-news/mathematicians-puzzled-over-a-famous-problem-for-80-years-now-theyve-used-ai-to-identify-a-clever-solution-180988889/. 
  17. ↑ "Remarks on the disproof of the unit distance conjecture". 20 May 2026. https://arxiv.org/html/2605.20695v1. 
  18. ↑ Grinsztajn, Max. "A 63-dimensional counterexample to Borsuk's conjecture". https://github.com/maaxgrin/borsuk-63-counterexample. 
  19. ↑ "Smallest dimension in which Borsuk's conjecture fails" (in en). https://teorth.github.io/optimizationproblems/constants/28a.html. 
  20. ↑ Oum, Sang-il (17 July 2026). "A proof of the cycle double cover conjecture by OpenAI: an exposition". arXiv:2607.16356 [math.CO].
  21. ↑ Geelen, Jim (16 July 2026). "OpenAI's proof of the Cycle Double Cover Theorem". arXiv:2607.15399v1 [math.CO].
  22. ↑ OpenAI (July 2026). "A proof of the cycle double cover conjecture". https://cdn.openai.com/pdf/04d1d1e4-bc75-476a-97cf-49055cd98d31/cdc_proof.pdf. 
  23. ↑ Dmitry, Rybin [@DmitryRybin1] (22 July 2026). "Dinitz-Garg-Goemans conjecture is false. This graph theory problem was open for ~30 years. The graph below has fractional flow cost 58. Any unsplittable flow (with capacity violation <=15) has cost at least 60. Chat with GPT 5.6 Pro where this was found: chatgpt.com/share/6a60b2eb-0b64-83ee-9c76-7931ca1de063". https://twitter.com/DmitryRybin1/status/2079906232069177643. 
  24. ↑ Rybin, Dmitri (2026-07-22). "Counterexample to Dinitz Conjecture". https://chatgpt.com/share/6a60b2eb-0b64-83ee-9c76-7931ca1de063. 
  25. ↑ Sparkes, Matthew (2026-07-23). "Extremely basic AI prompt cracks decades-old maths problem" (in en-GB). New Scientist. https://www.newscientist.com/article/2580932-extremely-basic-ai-prompt-cracks-decades-old-maths-problem/. 
  26. ↑ 26.0 26.1 Townsend, Alex; Greenbaum, Anne (14 August 2026). "The Neurosurgery Resident Who Proved Crouzeix's Conjecture". https://alextownsend.net/essays/SIAMNews_CrouzeixConjecture.pdf. 
  27. ↑ Lorist, Emiel; Schwenninger, Felix (4 August 2026). "A solution to Crouzeix's conjecture". arXiv:2608.03841 [math.CA].
  28. ↑ Jin, Shanmu (27 July 2026). "The Numerical Range Is a 2-Spectral Set". Preprints. doi:10.20944/preprints202607.1919.v1. 
  29. ↑ 29.0 29.1 29.2 "openai/ten-proofs", Github (OpenAI), 2026-09-17, https://github.com/openai/ten-proofs, retrieved 2026-09-20 
  30. ↑ 30.0 30.1 30.2 "Ten advances in mathematics and theoretical computer science" (in en-US). 2026-08-01. https://openai.com/index/ten-advances-in-mathematics/. 
  31. ↑ Mazur, Lech (5 August 2026). "A COMPUTER-ASSISTED PROOF OF SENDOV'S CONJECTURE". https://www.proofatlas.ai/papers/sendov-conjecture/SENDOV_CONJECTURE_PROOF_AUGUST_5_2026.pdf. 
  32. ↑ teorth (2026-08-31), "teorth/sendov", Github, https://github.com/teorth/sendov, retrieved 2026-09-20 
  33. ↑ Lech Mazur [@LechMazur] (3 August 2026). "Quick pre-announcement for people working on Sendov's conjecture: I posted a proof.". https://twitter.com/LechMazur/status/2084155864353521706. 
  34. ↑ Tao, Terence (12 August 2026). "A digestion of the proof of Sendov's conjecture". https://terrytao.wordpress.com/2026/08/12/a-digestion-of-the-proof-of-sendovs-conjecture/. 
  35. ↑ Weisstein, Eric W.. "Sendov Conjecture". https://mathworld.wolfram.com/SendovConjecture.html. 
  36. ↑ anthropics/formal-math, Anthropic, 2026-09-14, https://github.com/anthropics/formal-math, retrieved 2026-09-14 
  37. ↑ "Learning more about Claude's mathematical capabilities" (in en). https://www.anthropic.com/research/riemann-zeta. 
  38. ↑ Markman, Jon (13 August 2026). "Claude Just Broke A Math Record That Stood For 37 Years" (in en). https://www.forbes.com/sites/jonmarkman/2026/08/13/claude-just-broke-a-math-record-that-stood-for-37-years/. 
  39. ↑ Parham, Adrian (2026-08-12). "Claude raises Riemann zeta zeros to 67.2%: two papers no one had combined" (in en-US). https://www.techtimes.com/articles/324173/20260812/claude-raises-riemann-zeta-zeros-672-two-papers-no-one-had-combined.htm. 
  40. ↑ Weisstein, Eric W.. "Hadamard Matrix". https://mathworld.wolfram.com/HadamardMatrix.html. 
  41. ↑ "Hadamard Matrix of Order 668". https://epoch.ai/frontiermath/open-problems/hadamard. 
  42. ↑ "curve #273" (in en). https://elliptic-rank.icarm.cloud/curve/273. 
  43. ↑ "curve #302" (in en). https://elliptic-rank.icarm.cloud/curve/302. 
  44. ↑ Bischoff, Manon (2026-08-25). "KI findet die bisher komplexeste Kurve" (in de). https://www.spektrum.de/news/claude-anthropic-ki-findet-elliptische-kurve-mit-rang-30-und-31/2341336. 
  45. ↑ Weisstein, Eric W.. "Elliptic Curve Rank" (in en). Wolfram Research, Inc.. https://mathworld.wolfram.com/EllipticCurveRank.html. 
  46. ↑ "Anthropic Researcher Says Claude Helped Build a Complex Structure on S⁶, Taking Aim At The Unsolved Hopf Problem". 2026-08-24. https://officechai.com/ai/anthropic-researcher-says-claude-helped-build-a-complex-structure-on-s%E2%81%B6-taking-aim-at-the-unsolved-hopf-problem/. 
  47. ↑ "A tilted residue-class construction for long prime-free intervals · VibeMathed" (in en). 30 August 2026. https://vibemathed.com/problem/tilted-residue-class-construction-for-long-prime-free-intervals. 
  48. ↑ "Erdős Problems: 4". https://www.erdosproblems.com/forum/thread/4/proof-claims. 
  49. ↑ OpenAI (30 August 2026). "Improved short gaps between primes". https://cdn.openai.com/pdf/51126fac-1b68-4128-9666-c908bcc16033/short_gaps.pdf. 
  50. ↑ Anthropic (3 September 2026). "θ(p_c) = 0 for Bernoulli bond percolation on ℤ^d in all dimensions d ≥ 2, in Lean 4 / Mathlib". https://github.com/anthropics/formal-math/blob/795efb86f191735c5481675763537cfb4ff37e55/percolation/README.md. 
  51. ↑ "Proofs of the Kozma–Nitzan c onjectures". 4 September 2026. https://nitromannitol.github.io/kn1-verification-b80e9/. 
  52. ↑ Anthropic (4 September 2026). "Formalizing Fermat's Last Theorem". https://www.anthropic.com/research/formalizing-fermats-last-theorem. 
  53. ↑ Anthropic. "Formalizing Fermat's Last Theorem in Lean: A timeline and selected excerpts from Claude's reasoning". https://www-cdn.anthropic.com/9e431dff043da6538d99d6c2d231b670aa3da263.pdf. 
  54. ↑ "AI has completed the largest proof in the history of mathematics". 5 September 2026. https://eu.36kr.com/en/p/3969755274883328. 
  55. ↑ "Köthe conjecture: disproof (Krempa's matrix form)". https://github.com/tadamcz/koethe. 
  56. ↑ Adamczewski, Tom; Böhmler, Bernhard; Marczinzik, Rene (7 September 2026). "A counterexample to Köthe's conjecture and a question of Rowen". arXiv:2609.07996v1 [math.RA].
  57. ↑ Adamczewski, Tom (4 September 2026). "X Post". https://x.com/tmkadamcz/status/2095785941193404457. 
  58. ↑ "The Ibragimov–Iosifescu conjecture for φ-mixing sequences". https://github.com/tadamcz/phi-mixing-clt. 
  59. ↑ Adamczewski, Tom; Klostermeyer, William F. (10 September 2026). "A Counterexample to an Eternal Domination Conjecture". arXiv:2609.11500v1 [math.CO].
  60. ↑ "tadamcz/dittert: Lean 4 proof of the full Dittert conjecture, with mathematical exposition". https://github.com/tadamcz/dittert. 
  61. ↑ "Lean 4 counterexample to the n=4 case of the strong N conjecture". https://github.com/tadamcz/n-conjecture-strong. 
  62. ↑ Howlett, Joseph (8 September 2026). "OpenAI claims blockbuster math breakthrough amid swirl of controversy" (in en). https://www.scientificamerican.com/article/openai-claims-blockbuster-math-breakthrough-amid-swirl-of-controversy/. 
  63. ↑ Knight, Will; Zeff, Maxwell (2026-09-08). "OpenAI Just Claimed a Huge Math Discovery. Some Academics Are Crying Foul" (in en-US). Wired. ISSN 1059-1028. https://www.wired.com/story/openai-navier-stokes-math-discovery-academics/. Retrieved 2026-09-09. 



Retrieved from "https://handwiki.org/wiki/index.php?title=Software:List_of_mathematical_discoveries_by_artificial_intelligence&oldid=4634728"