Software:Timeline of artificial intelligence contributions to mathematics

From HandWiki
Short description: Chronology of AI-assisted developments in mathematical research


The timeline of artificial intelligence contributions to mathematics lists selected developments in which artificial intelligence (AI) systems contributed to mathematical proof, conjecture generation, algorithm design, or research discovery. It includes symbolic automated reasoners, heuristic discovery programs, machine-learning-guided proof search, neuro-symbolic systems, and large language models (LLMs).[1][2]

The boundary between AI and other forms of computer-assisted mathematics has shifted over time. The timeline therefore includes a small number of proof assistant and formal-library developments that directly enabled later AI-generated mathematics or supplied machine-checkable verification. It excludes routine numerical computation, computer algebra, and proofs whose search was directed primarily by humans. Results on established competition problems are included as capability benchmarks and are distinguished from work on open research questions.[3]

Precursors before 1950

  • 1928 – David Hilbert and Wilhelm Ackermann formulated the Entscheidungsproblem, asking for a mechanical procedure that could decide the validity of statements in first-order logic. The problem helped establish the idea that mathematical reasoning itself might be made algorithmic.[4]
  • 1936–1937 – Alan Turing formalized computation using the model now called the Turing machine and showed that no general algorithm can decide every instance of the Entscheidungsproblem. The result placed a fundamental limit on fully automatic mathematical reasoning while giving later researchers a precise model of mechanical computation.[5]

1950s

  • 1956 – Allen Newell, Herbert A. Simon, and Cliff Shaw developed the Logic Theorist, one of the earliest programs created specifically to perform automated reasoning and often described as the first AI program. Using heuristic search, it proved 38 of the first 52 theorems in the second chapter of Principia Mathematica and found a shorter proof of one theorem than the proof in the book.[6]
  • 1959 – Herbert Gelernter's Geometry Theorem Machine proved its first theorem in elementary Euclidean geometry on an IBM 704. The program combined symbolic deduction with heuristic use of diagrams and subsequently solved numerous problems drawn from secondary-school textbooks and examinations.[7]

1960s

  • 1965 – J. Alan Robinson introduced the resolution principle, a machine-oriented inference rule for first-order logic. Resolution, together with unification, became a foundation of automated theorem proving and later logic-programming systems.[8]
  • 1968 – Nicolaas Govert de Bruijn began the Automath project, an early computer-implemented system for writing and checking fully formal mathematics. Automath was not an AI discovery system, but its use of a small proof-checking core and a formal mathematical language influenced later proof assistants, including the line of work that led to Coq.[9]

1970s

  • 1971 – Robert S. Boyer and J Strother Moore began developing the Boyer–Moore theorem prover, later known as NQTHM. It automated rewriting and mathematical induction over recursively defined functions and became an influential model of a largely automatic prover for program and arithmetic properties.[10]
  • 1972 – Robin Milner developed the original LCF proof checker at Stanford University. LCF introduced an architecture in which all theorems must be produced through a small trusted kernel while higher-level tactics may automate proof construction. This architecture became foundational for later proof assistants and for safely checking AI-generated proof attempts.[11]
  • 1976–1977 – Douglas Lenat developed AM, a heuristic program intended to form mathematical concepts, generate examples, and propose conjectures. Beginning with elementary set theory, AM rediscovered a number of familiar concepts and relations. Although its mathematical scope was elementary, it established automated theory formation as a distinct AI research program.[12]

1980s

  • 1984–1985 – Siemion Fajtlowicz created Graffiti, an automated conjecture-making program for graph theory. Rather than attempting complete proofs, Graffiti searched databases of graphs for potentially informative inequalities between graph invariants. Its conjectures prompted a substantial body of subsequent mathematical work and helped establish computer-generated conjecturing as a practical research activity.[13][14]

1990s

  • 1996 – William McCune's EQP theorem prover found an automatic proof that every Robbins algebra is a Boolean algebra, resolving the Robbins problem, which had remained open since the 1930s. The proof was generated without a human-supplied proof outline, making the result an early instance of a fully automatic prover resolving a recognized open problem.[15]
  • 1999 – Simon Colton, Alan Bundy, and Toby Walsh presented the HR system, which formed concepts, generated conjectures, and called the Otter theorem prover and MACE model generator to prove or refute them. HR integrated concept formation, conjecture generation, theorem proving, and finite-model search within a single discovery system.[16]

2000s

  • 2007 – Lawrence Paulson and collaborators released Sledgehammer for Isabelle/HOL. Sledgehammer selected potentially relevant facts, translated proof goals for external automated theorem provers, and reconstructed successful results inside Isabelle's trusted environment. It became an influential example of combining powerful but comparatively untrusted search with kernel-checked interactive proof.[17]

2010s

  • 2013–2014 – Leonardo de Moura launched the Lean theorem prover project in 2013, and Lean 0.1 was released in June 2014. The community-maintained mathlib library began in 2017. Lean was not itself an AI system, but its formal language, extensible tactics, mathematical library, and small trusted kernel were later used extensively in machine-learning-based theorem proving and in verification of AI-generated proofs.[18][19]
  • 2016 – DeepMath applied deep neural sequence models to premise selection in the Mizar mathematical corpus. Its authors described it as the first large-scale application of deep learning to theorem proving; the model learned to rank relevant premises instead of relying only on hand-designed relevance heuristics.[20]
  • 2019 – Google researchers released HOList, an open environment and benchmark based on HOL Light, together with the DeepHOL prover. DeepHOL used deep reinforcement learning to guide proof search, making formal higher-order theorem proving a reproducible machine-learning task at substantially larger scale.[21]

2020s

The 2020s saw increasing use of transformers, LLMs, reinforcement learning, synthetic training data, and deterministic proof or program evaluators. Two partially separate approaches developed: systems that generated formal objects checked by proof assistants, and natural-language systems used interactively by mathematicians, with humans responsible for detecting errors and turning suggestions into rigorous arguments.[2][3]

2020–2022

  • 2020 – Stanislas Polu and Ilya Sutskever introduced GPT-f, a transformer-based prover for the Metamath formal language. GPT-f generated new shorter proofs that were accepted into Metamath's main library; the authors described this as the first time proofs produced by a deep-learning system had been adopted by a formal-mathematics community.[22]
  • 2021 – The Ramanujan Machine project published algorithms that automatically generated conjectural continued-fraction identities for fundamental constants. The system supplied numerical conjectures rather than proofs, making its output a source of research questions to be proved or refuted by mathematicians.[23]
  • 2021 – A collaboration between Google DeepMind researchers and mathematicians used supervised machine learning to identify patterns in large mathematical datasets. The analysis guided human researchers to a new conjecture relating algebraic and geometric properties of knots and to a new theorem in representation theory. The work was presented as a human–AI discovery process: learned correlations suggested structure, while mathematicians interpreted the patterns and supplied the proofs.[24]
  • 2022 – OpenAI researchers first released work applying expert iteration and curriculum learning to a transformer prover operating in Lean; it was published at ICLR in 2023. The system achieved then-state-of-the-art results on the miniF2F benchmark and automatically solved several formally stated competition problems.[25]
  • 2022 – Google DeepMind's AlphaTensor used reinforcement learning to search for matrix-multiplication algorithms. Among its results was a method for multiplying two 4-by-4 matrices over the two-element field using 47 scalar multiplications, compared with 49 for two recursive applications of Strassen's algorithm. The result demonstrated that an AI search system could discover new exact algorithms in a well-studied mathematical problem.[26]

2023–2024

  • 2023 – LeanDojo provided an open-source environment, dataset, benchmark, and retrieval-augmented LLM prover for Lean. Its ReProver system retrieved relevant premises from mathlib before generating proof steps, integrating an LLM with a large formal library and Lean's proof checker.[27]
  • December 2023 – Google DeepMind announced FunSearch, with its peer-reviewed paper appearing in Nature in January 2024. FunSearch coupled an LLM that generated computer programs with an evolutionary search process and an automatic evaluator. It found larger constructions for cases of the cap set problem, including an improved asymptotic lower bound, and produced new heuristics for online bin packing. Each candidate program was executable and automatically scored before being returned by the search process.[28]
  • January 2024 – Google DeepMind published AlphaGeometry, a neuro-symbolic system in which a language model proposed auxiliary geometric constructions and a symbolic engine derived proofs. It solved 25 of a benchmark set of 30 olympiad geometry problems, compared with 10 for the previous leading system.[29]
  • July 2024 – At the 2024 International Mathematical Olympiad (IMO), Google DeepMind's AlphaProof found Lean proofs for three non-geometry problems and AlphaGeometry 2 solved the geometry problem. The combined score was 28 out of 42, equivalent to the silver-medal range. The non-geometry problems were manually translated into Lean, and the hardest proofs required multiple days of computation, so the result was a major formal-reasoning benchmark rather than a performance under the same conditions as human contestants.[30]

2025–2026

  • May–November 2025 – Google DeepMind announced AlphaEvolve, an LLM-guided evolutionary coding system with deterministic evaluators. One of its mathematical outputs was a rank-48 bilinear decomposition for multiplying 4-by-4 matrices over the complex numbers, improving on the rank-49 construction obtained by recursively applying Strassen's algorithm in that tensor-rank setting; a subsequent paper derived a related construction using only rational coefficients. A later study applied AlphaEvolve to 67 problems in analysis, combinatorics, geometry, and number theory, reporting improvements over the best known constructions in 23 cases and matches in 36.[31][32][33][3]
  • July 2025 – Google DeepMind's Gemini Deep Think was officially assessed as solving five of the six IMO problems for a score of 35 out of 42, at the gold-medal threshold, within the competition's 4.5-hour sessions and using natural-language solutions. OpenAI reported the same score for an experimental reasoning model whose answers were graded by external experts. These were the first reported gold-medal-level performances by general-purpose AI systems at the IMO, but the problems had known answers and the results did not by themselves establish research-level mathematical discovery.[34][3]
  • October 2025 – Uijeong Jang and Ernest Ryu released an AI-assisted proof of point convergence for Nesterov's accelerated gradient method, resolving a question left open since the method was introduced in 1983. The authors said the discovery was heavily assisted by ChatGPT: they repeatedly examined incorrect model outputs, retained useful intermediate steps, and supplied the verification and mathematical synthesis. An independent paper by Radu Ioan Boţ, Jalal Fadili, and D.-K. Nguyen reached a contemporaneous resolution in a broader setting, so the AI-assisted paper was one of two independent solutions rather than the sole resolution.[35][3][36]
  • January 2026 – A preprint reported that OpenAI's GPT-5.2 Pro and Harmonic's Aristotle system produced a proof in Lean of Erdős problem 728, concerning factorial divisibility.[37]
  • April–May 2026 – Output from GPT-5.4 Pro suggested a new method for bounding Erdős sums of primitive sets, based on Markov chains with von Mangoldt weights. Mathematicians developed the method into proofs of two 1966 conjectures of Erdős, Sárközy, and Szemerédi—Erdős problems 1196 and 1217—and a revised form of the Banks–Martin conjecture.[38][39]
  • May 2026 – An internal OpenAI model produced a counterexample to Paul Erdős's conjectured near-linear upper growth for the planar unit distance problem. It constructed infinitely many sets of n planar points with at least n1+ε unit-distance pairs for some fixed ε>0, disproving the conjecture that the extremal number is n1+o(1). A group of mathematicians published a simplified, human-verified account. The result did not determine the exact asymptotic maximum, which remained open.[40][41]
  • July 2026 – Levent Alpöge reported a polynomial map from ℂ3 to itself, found with Anthropic's Claude Fable 5, whose Jacobian determinant is a nonzero constant but which is generically three-to-one. The counterexample disproved the Jacobian conjecture in dimension three and higher; the two-dimensional case remained open.[42][43]
  • July 2026 – OpenAI released a proof of the cycle double cover conjecture, which states that every bridgeless graph has a collection of cycles covering each edge exactly twice. Jim Geelen and Sang-il Oum subsequently published expositions of the argument.[44][45]

Verification

A proof accepted by a system such as Lean establishes that a formal statement follows from specified axioms and definitions according to a small checking kernel. It does not by itself establish that the formal statement accurately captures the intended informal problem or that the result is new. Those questions require mathematical and historical review.[46]

Different systems provide different forms of verification. FunSearch and AlphaTensor generate candidates that can be tested by deterministic evaluators, while formal provers generate objects that can be checked by a proof kernel. Natural-language model outputs may contain plausible but invalid arguments and require human checking.[3][30] Olympiad scores, formal benchmark pass rates, machine-verified proofs, and original research discoveries are therefore not directly comparable measures of mathematical capability.

See also

References

  1. ↑ Pantsar, Markus (2024). "Theorem proving in artificial neural networks: new frontiers in mathematical AI". European Journal for Philosophy of Science 14 (1): 4. doi:10.1007/s13194-024-00569-6. 
  2. ↑ 2.0 2.1 Li, Zhaoyu; Sun, Jialiang; Murphy, Logan; Su, Qidong; Li, Zenan; Zhang, Xian; Yang, Kaiyu; Si, Xujie (2024). "A Survey on Deep Learning for Theorem Proving". Conference on Language Modeling. https://openreview.net/forum?id=zlw6AHwukB. Retrieved 1 August 2026. 
  3. ↑ 3.0 3.1 3.2 3.3 3.4 3.5 Kakaes, Konstantin (13 April 2026). "The AI Revolution in Math Has Arrived". Quanta Magazine. https://www.quantamagazine.org/the-ai-revolution-in-math-has-arrived-20260413/. Retrieved 1 August 2026. 
  4. ↑ Hilbert, David; Ackermann, Wilhelm (1928) (in de). Grundzüge der theoretischen Logik. Berlin: Springer. 
  5. ↑ Turing, A. M. (1937). "On Computable Numbers, with an Application to the Entscheidungsproblem". Proceedings of the London Mathematical Society. 2 42 (1): 230–265. doi:10.1112/plms/s2-42.1.230. 
  6. ↑ Gugerty, Leo (2006). "Newell and Simon's Logic Theorist: Historical Background and Impact on Cognitive Modeling". 50. pp. 880–884. doi:10.1177/154193120605000904. 
  7. ↑ Gelernter, Herbert; Hansen, James R.; Loveland, Donald W. (1960). "Empirical explorations of the geometry theorem machine". Western Joint IRE-AIEE-ACM Computer Conference. pp. 143–149. doi:10.1145/1460361.1460381. 
  8. ↑ Robinson, J. A. (1965). "A Machine-Oriented Logic Based on the Resolution Principle". Journal of the ACM 12 (1): 23–41. doi:10.1145/321250.321253. 
  9. ↑ Geuvers, Herman; Nederpelt, Rob (2022). "Characteristics of de Bruijn's early proof checker Automath". Fundamenta Informaticae 185 (4): 313–336. doi:10.3233/FI-222112. 
  10. ↑ Moore, J Strother. "The Boyer-Moore Theorem Prover (NQTHM)". University of Texas at Austin. https://www.cs.utexas.edu/~moore/best-ideas/nqthm/index.html. 
  11. ↑ Gordon, Michael J. C. (2000). "From LCF to HOL: a short history". Proof, Language, and Interaction: Essays in Honour of Robin Milner. MIT Press. pp. 169–185. ISBN 978-0-262-16188-6. https://www.cl.cam.ac.uk/archive/mjcg/papers/HolHistory.pdf. Retrieved 1 August 2026. 
  12. ↑ Lenat, Douglas B. (1977). "Automated Theory Formation in Mathematics". Fifth International Joint Conference on Artificial Intelligence. pp. 833–842. https://www.ijcai.org/Proceedings/77-2/Papers/061.pdf. Retrieved 1 August 2026. 
  13. ↑ Fajtlowicz, Siemion (1988). "On Conjectures of Graffiti". Discrete Mathematics 72 (1–3): 113–118. doi:10.1016/0012-365X(88)90199-9. 
  14. ↑ DeLaViña, Ermelinda (January 2003). "Some History of the Development of Graffiti". University of Houston–Downtown. https://www.uhd.edu/documents/academics/sciences/history.pdf. 
  15. ↑ McCune, William (1997). "Solution of the Robbins Problem". Journal of Automated Reasoning 19 (3): 263–276. doi:10.1023/A:1005843212881. 
  16. ↑ Colton, Simon; Bundy, Alan; Walsh, Toby (1999). "Automatic Concept Formation in Pure Mathematics" (PDF). IJCAI-99. Stockholm, Sweden. pp. 786–791. https://www.ijcai.org/Proceedings/99-2/Papers/018.pdf. Retrieved 1 August 2026. 
  17. ↑ Paulson, Lawrence C.; Blanchette, Jasmin Christian (2012). "Three Years of Experience with Sledgehammer, a Practical Link between Automatic and Interactive Theorem Provers". International Workshop on the Implementation of Logics. 2. pp. 1–11. doi:10.29007/36dt. 
  18. ↑ "Introduction". The Lean Language Reference. Lean Focused Research Organization. https://lean-lang.org/doc/reference/latest/Introduction/. 
  19. ↑ The mathlib Community (2020). "The Lean Mathematical Library". Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs. pp. 367–381. doi:10.1145/3372885.3373824. 
  20. ↑ Alemi, Alexander A.; Chollet, François; Eén, Niklas; Irving, Geoffrey; Szegedy, Christian; Urban, Josef (2016). "DeepMath—Deep Sequence Models for Premise Selection". Advances in Neural Information Processing Systems 29. pp. 2235–2243. https://proceedings.neurips.cc/paper/2016/hash/f197002b9a0853eca5e046d9ca4663d5-Abstract.html. Retrieved 1 August 2026. 
  21. ↑ Bansal, Kshitij; Loos, Sarah M.; Rabe, Markus N.; Szegedy, Christian; Wilcox, Stewart (2019). "HOList: An Environment for Machine Learning of Higher-Order Logic Theorem Proving". Proceedings of the 36th International Conference on Machine Learning. 97. pp. 454–463. https://proceedings.mlr.press/v97/bansal19a.html. Retrieved 1 August 2026. 
  22. ↑ Polu, Stanislas; Sutskever, Ilya (2020). "Generative Language Modeling for Automated Theorem Proving". arXiv:2009.03393 [cs.LG].
  23. ↑ Raayoni, Gal et al. (2021). "Generating conjectures on fundamental constants with the Ramanujan Machine". Nature 590: 67–73. doi:10.1038/s41586-021-03229-4. 
  24. ↑ Davies, Alex et al. (2021). "Advancing mathematics by guiding human intuition with AI". Nature 600: 70–74. doi:10.1038/s41586-021-04086-x. PMID 34853458. 
  25. ↑ Polu, Stanislas; Han, Jesse Michael; Zheng, Kunhao; Baksys, Mantas; Babuschkin, Igor; Sutskever, Ilya (2023). "Formal Mathematics Statement Curriculum Learning". The Eleventh International Conference on Learning Representations. https://openreview.net/forum?id=-P7G-8dmSh4. Retrieved 1 August 2026. 
  26. ↑ Fawzi, Alhussein et al. (2022). "Discovering faster matrix multiplication algorithms with reinforcement learning". Nature 610: 47–53. doi:10.1038/s41586-022-05172-4. 
  27. ↑ Yang, Kaiyu; Swope, Aidan M.; Gu, Alex; Chalamala, Rahul; Song, Peiyang; Yu, Shixing; Godil, Saad; Prenger, Ryan et al. (2023). "LeanDojo: Theorem Proving with Retrieval-Augmented Language Models". Advances in Neural Information Processing Systems 36. https://proceedings.neurips.cc/paper_files/paper/2023/hash/4441469427094f8873d0fecb0c4e1cee-Abstract-Datasets_and_Benchmarks.html. Retrieved 1 August 2026. 
  28. ↑ Romera-Paredes, Bernardino et al. (2024). "Mathematical discoveries from program search with large language models". Nature 625: 468–475. doi:10.1038/s41586-023-06924-6. PMID 38096900. 
  29. ↑ Trinh, Trieu H.; Wu, Yuhuai; Le, Quoc V.; He, He; Luong, Thang (2024). "Solving olympiad geometry without human demonstrations". Nature 625: 476–482. doi:10.1038/s41586-023-06747-5. PMID 38233616. 
  30. ↑ 30.0 30.1 Hubert, Thomas et al. (2025). "Olympiad-level formal mathematical reasoning with reinforcement learning". Nature. doi:10.1038/s41586-025-09833-y. 
  31. ↑ Novikov, Alexander; Vũ, Ngân; Eisenberger, Marvin (2025). "AlphaEvolve: A coding agent for scientific and algorithmic discovery". arXiv:2506.13131 [cs.AI]. {{cite arXiv}}: Invalid |display-authors=0. (help)
  32. ↑ Dumas, Jean-Guillaume; Pernet, Clément; Sedoglavic, Alexandre (2025). "A non-commutative algorithm for multiplying 4×4 matrices using 48 non-complex multiplications". arXiv:2506.13242 [cs.SC].
  33. ↑ Georgiev, Bogdan; Gómez-Serrano, Javier; Tao, Terence; Wagner, Adam Zsolt (2025). "Mathematical exploration and discovery at scale". arXiv:2511.02864 [cs.NE].
  34. ↑ Cai, Kenrick; Singh, Jaspreet (22 July 2025). "Google clinches milestone gold at global math competition, while OpenAI also claims win". Reuters. https://www.reuters.com/world/asia-pacific/google-clinches-milestone-gold-global-math-competition-while-openai-also-claims-2025-07-22/. 
  35. ↑ Jang, Uijeong; Ryu, Ernest K. (2025). "Point Convergence of Nesterov's Accelerated Gradient Method: An AI-Assisted Proof". arXiv:2510.23513 [math.OC].
  36. ↑ Boţ, Radu Ioan; Fadili, Jalal; Nguyen, D.-K. (2025). "The Iterates of Nesterov's Accelerated Algorithm Converge in the Critical Regimes". arXiv:2510.22715 [math.OC].
  37. ↑ Sothanaphan, Nat (2026). "Resolution of Erdős Problem #728: a writeup of Aristotle's Lean proof". arXiv:2601.07421 [math.NT].
  38. ↑ Alexeev, Boris; Barreto, Kevin; Li, Yanyang; Lichtman, Jared Duker; Price, Liam; Shah, Jibran Iqbal; Tang, Quanyu; Tao, Terence (2026). "Primitive sets and von Mangoldt chains: Erdős Problem #1196 and beyond". arXiv:2605.00301 [math.NT].
  39. ↑ Howlett, Joseph (24 April 2026). "An amateur just solved a 60-year-old math problem—by asking AI". Scientific American. https://www.scientificamerican.com/article/amateur-armed-with-chatgpt-vibe-maths-a-60-year-old-problem/. Retrieved 1 August 2026. 
  40. ↑ Alon, Noga; Bloom, Thomas F.; Gowers, W. T.; Litt, Daniel; Sawin, Will; Shankar, Arul; Tsimerman, Jacob; Wang, Victor; Wood, Melanie Matchett (2026). "Remarks on the disproof of the unit distance conjecture". arXiv:2605.20695 [math.CO].
  41. ↑ "OpenAI makes breakthrough on 80-year-old maths problem". The Guardian. 21 May 2026. https://www.theguardian.com/technology/2026/may/21/openai-paul-erdos-maths-problem-breakthrough. 
  42. ↑ Stark-Elster, Eli (27 July 2026). "A.I. Disproves a Decades-Old Mathematical Idea, the 'Biggest Conjecture' That the Tech Has Played a Role in Yet". Smithsonian Magazine. https://www.smithsonianmag.com/smart-news/ai-disproves-a-decades-old-mathematical-idea-the-biggest-conjecture-that-the-tech-has-played-a-role-in-yet-180989189/. Retrieved 1 August 2026. 
  43. ↑ Shaska, T. (2026). "Graded Keller maps and the Jacobian Conjecture". arXiv:2607.20210 [math.AG].
  44. ↑ Geelen, Jim (2026). "OpenAI's proof of the Cycle Double Cover Theorem". arXiv:2607.15399 [math.CO].
  45. ↑ Oum, Sang-il (2026). "A proof of the cycle double cover conjecture by OpenAI: An exposition". arXiv:2607.16356 [math.CO].
  46. ↑ "From Trust to Verification: Lean's Impact on Mathematics". Simons Foundation. 23 June 2026. https://www.simonsfoundation.org/2026/06/23/from-trust-to-verification-leans-impact-on-mathematics/. 




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