Since the mathlib repository was created in summer 2017, each year has been bigger than the last. As an end-of-year retrospective, we look at how the mathlib library and community have developed in 2021.

Statistics

Since early 2019, mathlib has followed a "squash and merge" strategy for pull requests. One commit to the main branch corresponds to one merged pull request.

For more information, see the page on mathlib statistics.

Records

December 2021 set a record as the month with the highest number of commits, at 565. Four of the five most active months happened in 2021; December, October, and September were mathlib's first, second, and third most active months, respectively.

Yury Kudryashov was the year's most prolific contributor, with 662 commits, surpassing his previous year's record of 624. Yaël Dillies deserves a special shoutout: in their first year of contributing, they became the year's fourth most prolific contributor, with 301 commits.

New contributors to mathlib

77 people contributed to mathlib for the first time in 2021. In total, 864 commits were from new contributors. Many thanks to:

Mohamed Al-Fahim, David Kurniadi Angdinata, Noam Atar, Mantas Baksys, Itai Bar-Natan, Chris Birkbeck, Manuel Candales, Carlos Caralps, Robin Carlier, Antoine Chambert-Loir, Tian Chen, Joanna Choules, Iván Sadofschi Costa, Sara Díaz Real, Yaël Dillies, Ender Doe, Moritz Doll, Jon Eugster, Moritz Firsching, Mark Gerads, Vladimir Goryachev, Winston Gu, Mathieu Guay-Paquet, Violeta Hernández, Christopher Hoskin, Joseph Hua, María Inés de Frutos-Fernández, Ashwin Iyengar, Matt Kempster, Luke Kershaw, Huỳnh Trần Khanh, Praneeth Kolichala, Alex Kontorovich, Kalle Kytölä, Julian Külshammer, Antoine Labelle, Ryan Lahfa, Paul Lezeau, Jireh Loreaux, Bernd Losert, Giacomo Maletto, Julien Marquet, Marc Masdeu, Chase Meadors, Yuma Mizuno, Gabriel Moise, Sebastian Monnet, Hunter Monroe, Apurva Nakade, Anupam Nayak, Peter Nelson, Luke Nelson, Arthur Paulino, Sorawee Porncharoenwase, Stuart Presnell, Greg Price, Ethan Pronovost, Jakob von Raumer, David Renshaw, Joël Riou, Eric Rodriguez, Shadman Sakib, Jakob Scholbach, Andrew Souther, Justus Springer, François Sunatori, Henry Swanson, Ben Toner, Alain Verberkmoes, Way Yan Win, Ines Wright, Andrew Yang, Yourong Zang, Alex Zhang, Hanting Zhang, Alex Zhao, hallow-world

New mathlib maintainers

The group of mathlib maintainers has also grown! In 2021, Rémy Degenne, Markus Himmel, Bhavik Mehta, Oliver Nash, Adam Topaz, and Eric Wieser joined the team, which now numbers 23. (With the latter three, the team finally includes surnames from the second half of the alphabet.)

New field in mathlib: probability theory

The measure theory and analysis libraries have been developed enough to allow the definition of some probability theory concepts. mathlib now contains definitions of independence, probability density functions, conditional expectations, martingales and stopping times. We don't have many theorems about them yet and many other basic definitions are still missing, but the foundations are in place and 2022 should see a large development of probability theory in mathlib.

New Lean 3 community releases

The community has continued to maintain its version of Lean 3. Lean 3.24.0c was released Jan 4, 2021; as of Dec 31, the current version was 3.35.1c. Changes include:

• Parts of the core library were transitioned to mathlib to ease maintenance.
• Features were changed to support the transition to Lean 4, including coercion handling, ite/dite, and export formats.
• Many bugs were squashed, much documentation was added.

The Lean 3 repository includes a full change log.

Hoskinson Center for Formal Mathematics

In September, Carnegie Mellon University announced that a $20 million gift from blockchain entrepreneur Charles C. Hoskinson will be used to establish the Hoskinson Center for Formal Mathematics, housed in the Department of Philosophy. The center supports work making formal mathematics accessible and enjoyable to as wide an audience as possible.

Lean Together 2021

Way back in January, we hosted Lean Together 2021, an online meeting for Lean users and people from other formalization communities. The meeting included a number of talks, all recorded and posted on YouTube, as well as informal discussions and social time. Some highlights: Leonardo de Moura and Sebastian Ullrich officially introduced Lean 4, and a number of panelists discussed using proof assistants in the classroom.

Big projects

Liquid Tensor Experiment

One of the spectacular highlights in 2021 was the formalization of Theorem 9.4 of Scholze's Lectures on Analytic Geometry. This is the main technical ingredient in the proof of the main theorem of liquid vector spaces, a recent result of Clausen and Scholze. We embarked on this project after Scholze posted a challenge to the formalization communities.

We reached the milestone within half a year, faster than anyone had expected, surprising ourselves and others. The accomplishment was covered by Nature and Quanta.

The full challenge is not yet completed, and is actively worked on right now. See one of our recent blogposts for a progress report.

Sphere eversion

The sphere eversion project aims to formalize flexibility results in differential topology, including the celebrated existence of sphere eversions in $ℝ^3$. Development really took off in September 2021 with Floris van Doorn and Oliver Nash joining Patrick Massot in the project, with some extra help from Anatone Dedecker.

All the affine geometry of the project is now done, thanks to the work of Oliver, which was mostly contributed directly to mathlib. Most of general topology entering the project has been done, with Floris proving some delicate continuous function gluing results, and currently finishing some covering lemmas. The calculus backbone has been worked out by Patrick who proved many results about continuity and differentiability of integrals depending on parameters (still to be fully brought to mathlib) with help from Floris. Using this, the fundamental corrugation estimates have been proved. The project is now ready to merge those three aspects (affine geometry, topology and calculus) to prove all local results. Then the final part will be to handle the global theory using the differentiable manifolds theory in mathlib.

Fermat's Last Theorem for regular primes

The aim of the flt-regular project is to prove Fermat's Last Theorem for regular primes, an important result proved in 1850. This project continues the development of algebraic number theory in mathlib. You can have a look at the blueprint to check the mathematical details. After having developed the basic properties of cyclotomic extensions and of the discriminant, we are now computing the ring of integers of a cyclotomic extension. We can then work in $\mathbb{Z}[\zeta_p]$: doing arithmetic in $\mathbb{Z}[\zeta_p]$ is more complicated than in $\mathbb{Z}$, but the regularity assumption allows to prove the results we need.

Lean 4 porting effort

An early version of Lean 4 was released on Jan 4, 2021. Since then, effort has been going into tooling to help port mathlib from Lean 3. The mathlib4 library stub and mathport tool are both ongoing projects.

A recent blog post describes the current state of the effort.

Monthly recaps

Since the creation of this blog in summer 2021 we have recapped the project activity each month.

• August
• September
• Octover
• November
• December

Looking forward

A lot has changed in 2021. What's to come in 2022? Nobody knows for sure, but there's plenty to look forward to! Come join the crowd and help make this year an even bigger one than the last.