[Math] The use of computers leading to major mathematical advances II

big-listbig-pictureexamplesexperimental-mathematicsproof-assistants

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.

This is a continuation of a question that I asked 11 years ago.

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.

Best Answer

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.