Detailed · 8 events
AI and Mathematics: A History
1970s
Smithsonian National Museum of American History (Wikimedia Commons) · Public domain · Commons ↗ The theorem that any map can be coloured with four colours so that no two neighbouring regions share a colour. The question Francis Guthrie noticed in 1852 was settled in 1976 by Kenneth Appel and Wolfgang Haken at the University of Illinois. MacTutor (University of St Andrews) records that on 21 June 1976 they announced a proof of the four colour conjecture with the aid of a computer. The proof built an unavoidable set of nearly 1,500 configurations and had a computer check that each was reducible; according to MacTutor the reductions used about 1,200 hours of computer time. Whether a proof that no human could check in full deserved the name became a debate, and in 1979 the philosopher Thomas Tymoczko framed it as a problem of surveyability. In 1997 Robertson, Sanders, Seymour and Thomas published a second proof using 633 configurations, and in 2005 Georges Gonthier and Benjamin Werner checked the whole proof mechanically in the Coq proof assistant.
2010s
Greg L (Wikimedia Commons) · CC BY-SA 3.0 · Commons ↗ Kepler wrote in 1611 that no packing of equal spheres in three-dimensional space can be denser than the face-centred cubic arrangement familiar from stacks of cannonballs. In August 1998 Thomas Hales and Samuel Ferguson announced a proof built on massive computer calculations. The twelve referees appointed by the Annals of Mathematics could not check all of it; according to George Szpiro they reported in July 2002 that they were 99 percent certain it was sound. The proof appeared in the Annals in 2005, but, as the Flyspeck paper puts it, without complete certification from the referees. In January 2003 Hales launched Flyspeck, a project to formalise the proof in proof assistants, and it was completed on 10 August 2014. It combined HOL Light and Isabelle, and checking more than 23,000 nonlinear inequalities took about 5,000 processor-hours on Microsoft Azure. The official account appeared in Forum of Mathematics, Pi on 29 May 2017.
2020s
MartinThoma (Wikimedia Commons) · CC0 · Commons ↗ A plane-geometry theorem prover from Google DeepMind and New York University researchers, published in Nature on 17 January 2024. On 30 geometry problems drawn from the International Mathematical Olympiad (IMO) between 2000 and 2022, it solved 25 within competition time limits, against 10 for the previous best method (Wu's method) and an average of 25.9 for IMO gold medallists (DeepMind's figure). It is a neuro-symbolic system: a neural language model proposes auxiliary points and lines while a symbolic deduction engine does the reasoning. It was trained without human solutions, purely on 100 million theorems and proofs synthesised from random diagrams. Its proofs are human-readable, and the code and model were released. An April 2024 study showed, however, that classic symbolic methods combined with Wu's method could reach 21 problems on the same test, resetting the baseline. The successor, AlphaGeometry2, reported in February 2025 that it solved 84% of IMO geometry problems from the previous 25 years.
International Mathematical Olympiad (Wikimedia Commons) · Public domain · Commons ↗ On 25 July 2024 Google DeepMind announced that a system combining AlphaProof, which uses reinforcement learning to search for formal proofs, with the geometry specialist AlphaGeometry 2 had solved four of the six problems at the 65th International Mathematical Olympiad (IMO) in Bath, England, scoring 28 out of 42. That year's gold threshold was 29, so 28 sat at the top of the silver range. The solutions were scored under IMO rules by the Fields medallist Timothy Gowers and Joseph Myers, chair of the IMO 2024 Problem Selection Committee. AlphaProof solved three problems, including the hardest of the contest, which only five of the 609 human contestants solved; AlphaGeometry 2 solved geometry Problem 4. But the problems were first translated by hand into the formal language of the Lean proof assistant, and while one was solved within minutes, others took up to three days, against two 4.5-hour sessions for humans. The methods paper appeared in Nature in November 2025.
