Interactive theorem proving software can check, manipulate, and generate proofs of mathematical statements, just as computer algebra software can manipulate numbers, polynomials, and matrices. Over the last few years, these systems have become highly sophisticated, and have learnt a large amount of mathematics.

The "Lean for the Curious Mathematician 2022" workshop was held at ICERM in July 2022 and gathered mathematicians of all experience levels interested in formalization using the Lean interactive theorem prover. The workshop interspersed lectures on formalizing number theory, topology, geometry, analysis, and algebra with time for collaborative work on projects. 

One of the projects completed at the workshop was the Liquid Tensor Experiment. This project, led by Johan Commelin (University of Freiberg) and Adam Topaz (University of Alberta), had the goal of formalizing recent results by Dustin Clausen (University of Copenhagen) and Peter Scholze (University of Bonn) which are foundational to the development of condensed mathematics.  It began in December 2020 when Scholze proposed these results as a challenge to the formalization community. The results are very interesting targets as a challenge to current formalization capabilities because they are highly intricate, mathematically relatively self-contained, and central to an important current research program.

Over the course of 18 months, more than twenty people contributed to the formalization project.  The first major milestone was announced in June 2021. The achievement was described in Nature and Quanta.

During the ICERM workshop, several participants collaborated on the final effort that completed the project.  For more information about the Liquid Tensor Experiment, see the following blog post.

Another project was started at the workshop when Andrew Pollington (National Science Foundation), who specializes in metric number theory, started chatting with differential geometrist and formalization expert Oliver Nash (Imperial College London). It had been a week since James Maynard was awarded the Fields Medal for his work on prime number spacing. Pollington was particularly interested because Maynard's citation mentioned the Duffin-Schaeffer conjecture, which he himself had worked on in the past.

Nash decided to formalize one of the prerequisites for Koukoulopoulos and Maynard's proof: Gallagher's ergodic theorem. This is a theorem on Diophantine approximation. It states that the approximation of real numbers by rational numbers obeys a striking “all or nothing” behavior.

This formalization was completed in December 2022 and has been integrated into Lean’s core mathematical library, mathlib. For more information, see the preprint.