2021 - The Bottom Line
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.
This month in mathlib (Dec 2021)
December 2021 saw 565 commits to mathlib, which sets a new record. In this post we highlight some of these contributions.
Liquid Tensor Experiment: an update
In June 2021, we celebrated the first milestone of the Liquid Tensor Experiment. The achievement was covered in Nature and Quanta. Since then, we haven't been sitting still, and it's high time for a status update.
Update on mathport (Dec 2021)
mathport is the tool we're planning on using to help us port mathlib to Lean 4.
It has mostly been written by Mario Carneiro and Daniel Selsam,
and Gabriel Ebner and I have been making some fixes.
To provide some context, mathlib is the primary library for mathematics in Lean 3, containing over 700k lines of code and growing fast! Lean 4 now has a preliminary release, and we would really like to transition to building a mathematics library in Lean 4. While the type theory and kernel in Lean 4 are quite similar from a user point of view to Lean 3, it is certainly not the case that we can run Lean 3 code in Lean 4. Our aspiration is to achieve a "semi-automated" port.
Backstage with Yaël Dillies
We're introducing a new category of blog post: backstage interviews with mathlib's active contributors!
Today, Johan Commelin interviews Yaël Dillies.
Semilinear maps
Since linear maps appear everywhere in mathematics, it comes as no surprise that they have been part of mathlib for quite some time. However, as we were working on adding the basics of functional analysis to mathlib, a drawback quickly became apparent: conjugate-linear maps could not directly be expressed as linear maps. This meant that some constructions could not be formulated in their most natural way: for example, the map that takes an operator to its adjoint on a complex Hilbert space is a conjugate linear map, and so is the Riesz representation that maps a vector to its dual. This was also preventing us from developing the orthogonal group, the unitary group, etc, properly.
This month in mathlib (Nov 2021)
This post summarizes some of the activity that happened in mathlib in November.
Dedekind domains and class number in Lean
Pull request #9701 marks the completion of a string of additions to mathlib centered around formalizing Dedekind domains and class groups of global fields (those words will be explained below). Previous PRs had shown that nonzero ideals of a Dedekind domain factor uniquely into prime ideals, and had defined class groups in some generality. The main result in this PR is the finiteness of the class group of a global field (and in particular of the ring of integers of a number field). Formalizing these subjects has been one of my long-term goals for mathlib, and as far as we are aware, Lean is the first system in which this level of algebraic number theory is available. These formalizations have been joint work: most notable contributors on the Lean side were Ashvni Narayanan, Filippo Nuccio and myself, with Sander Dahmen developing a new finiteness proof of the class group specially for this project. Of course, we could not have done this without the assistance of the entire mathlib community. Sander, Ashvni, Filippo and I wrote a paper on the formalization project for the ITP 2021 conference; this blog post goes through the highlights of the paper.
Contributions to mathlib from LTE about normed groups
When the Liquid Tensor Experiment started, in December 2020, mathlib already had a decent theory of normed spaces. With this post I want to show how mathlib can benefit from projects like LTE, showing what we added to the theory of normed spaces in almost one year of work (this is only a small part of what has been added to mathlib from LTE, for a more complete list, see the history of for_mathlib folder).
This month in mathlib (Oct 2021)
This post summarizes some of the activity that happened in mathlib in October.