I would like to ask about recent examples, mainly after 2015, where experimentation by computers or other use of computers has led to major mathematical advances.

There are several categories:

A) Mathematical conjectures or large body of work arrived at by examining experimental data

B) Computer-assisted proofs of mathematical theorems

C) Computer programs that interactively or automatically lead to mathematical conjectures.

D) Various computer programs which allow proving automatically theorems or generating automatically proofs in a specialized field.

E) Computer programs (both general purpose and special purpose) for verification of mathematical proofs.

F) Large databases and other tools

Of course more resources (like this Wikipedia page on experimental mathematics) are also useful.

• I would also like to know recent examples of results of the form "the probability that $X$ is true is at least $\alpha$" where $\alpha$ is very close to $1$ and where $X$ is a random variable that is evaluated experimentally with a computer. Jun 30 at 7:39
• To qualify as 'major mathematical advance', do you have specific criterias in mind? For example Beeson, Narboux and Wiedijk have formalized all of Euclid in HOL light and Coq link.springer.com/article/10.1007/s10472-018-9606-x It allowed them to fix various flaws in Euclid : does this qualify? Jun 30 at 11:04
• @Archie, In my judgement it does and maybe I should change "major" to "substantial" or "important". Jun 30 at 12:25
• @GilKalai The title of your question is a little misleading. In your list, B and E often involve no "experimental mathematics" as that term is usually understood. Maybe your question should be titled, "The use of computers leading to major advances." Jun 30 at 14:45
• Dear @TimothyChow, you are right. Thanks to you and to Matt F for the improvement. Jun 30 at 19:42

There is the recent computer-assisted verification of some key statements by Scholze and Clausen about "condensed mathematics". The task has been accomplished by Buzzard, Commelin, and others (see comments below) using Lean, and it led to major media coverage. For instance, here is a related article that appeared on Nature on June 18, 2021.

• Other people involved in this project: Adam Topaz, Riccardo Brasca, Patrick Massot, Scott Morrison, Bhavik Mehta, Filippo Nuccio, Heather Macbeth, Damiano Testa, Mario Carneiro and many other helpful contributions from people in the Lean community.
– jmc
Jul 1 at 4:45
• I concur with this -- in fact when it comes to actual lines of code written, several of the people in the above list wrote way more than me. Certainly I am a big proponent of formalising modern mathematics in a theorem prover, but most of the hard work here was done by others. Jul 1 at 6:56
• Ok, thank you for providing the names of further contributors. I edited the answer accordingly. Jul 1 at 7:33

Here is an example of type A: Stavros Garoufalidis and Don Zagier have extensive work on refinements of Kashaev's Volume Conjecture (which relates the order of growth of the values of Jones polynomials of hyperbolic knots to the volume of their knot complement). Analyzing not just the main order of growth, but the whole asymptotic expansion, they have uncovered a vast amount of hidden structure; the key word here is the Quantum Modularity Conjecture (see equation (36)) of Zagier, but recently even further refinements have been found. This is experimental mathematics par excellence: They compute certain numbers to 1000 decimal places, figure out some asymptotic expansion, subtract it off, find that the remainder still has 500 significant places and admits an asymptotic expansion itself, ... .

This led to some concrete purely number-theoretic discoveries, such as an explicit description of an etale regulator map by Calegari--Garoufalidis--Zagier, and analogues of the Habiro ring for general number fields. Zagier is currently teaching a course.

Here is an interesting one. Reinforcement learning to generate counter-examples to several open conjectures in combinatorics and graph theory.

https://arxiv.org/abs/2104.14516

• I rewrote the code a bit to make it easier to use. If you can use Python, you can just write a function which gives any graph a score, and it will find graphs with large score faster than brute force search. Jul 4 at 17:47

Duplicating my comment : in 2015 Beeson, Narboux and Wiedijk have formalized all of Euclid in HOL light and Coq https://doi.org/10.1007/s10472-018-9606-x It allowed them to fix various flaws in Euclid.

For experimental mathematics as that term is usually understood, I would commend to your attention the paper by Roger Behrend, Ilse Fischer and Matjaž Konvalinka, "Diagonally and antidiagonally symmetric alternating sign matrices of odd order," Advances in Mathematics 315 (2017), 324–365, which won the 2019 AMS David P. Robbins Prize. In this paper, the authors proved a formula for the number of odd-order diagonally and antidiagonally symmetric alternating sign matrices, thus settling the last remaining of David Robbins’s conjectures on alternating sign matrices, which had stood for over thirty years.

One of the criteria for the Robbins Prize is that the work should include a significant experimental component. In this case, the authors' computer experimentation helped them discover the form of a crucial partition function.

A fascinating recent example in category B is the progresses on Kazhdan's property (T) that were made after Ozawa's reformulation of property (T) in terms of semidefinite programming. This has lead in particular to the resolution (by the affirmative) of the long-standing open question whether automorphism groups of free groups of rank $$\geq 4$$ have property (T), by Kaluba-Nowak-Ozawa (rank $$5$$), Kaluba-Kielak-Nowak (rank $$>5$$) and Nitsche (rank $$4$$). This gives a rigourous explanation for the remarkable efficiency of the product replacement algorithm for the generation of random elements in a finite group.

This story has happened almost live on MO, see here for much more details.

Adding to Archie's answer, Marjin Heule and collaborators have proven two major questions in Ramsey theory on the integers using SAT solvers. The 2016 result resolving the boolean Pythagorean triples problem received a lot of media attention for the being the largest proof to date. The 2018 result determining the five color Schur number was much larger. For links, including the expository article "The Science of Brute Force," see his Carnegie Mellon webpage.

What about Giles Gardam's construction of non-trivial units in the mod-2 group algebra of a torsion-free group https://arxiv.org/abs/2102.11818, which solved an 80-year old conjecture, and Alan Murray's extension of Giles Gardam's work to the mod-$$p$$ group algebra of the same group for odd primes https://arxiv.org/abs/2106.02147? I'm not sure which category to put it in. There is an interview with Gardam in which he says that the computing he did only required his laptop, but that it was comforting to know that he could have done more with a bigger computer if necessary.

An example of type B (I think) is Marijn Heule's program to reduce the size of graphs satisfying a given property. As an application it allowed him to find 5-chromatic unit distance graphs smaller than Aubrey de Grey's original one, see https://arxiv.org/abs/1805.12181 and https://arxiv.org/abs/1907.00929

• I think de Grey’s proof was also originally computer-assisted. Jul 1 at 2:13
• Aubrey de Grey's paper won the 2020 MAA Robbins Prize. Jul 2 at 13:15