Adventure 10000
About a month ago, the Cauchy integral theorem for some simple domains landed in mathlib. PR number 10000 was specially allocated for this occasion in advance. In this post I will recollect the events that led to this formalization.
This month in mathlib (Jan 2022)
January 2022 saw 533 commits to mathlib. In this post we highlight some of these contributions.
Backstage with Yakov Pechersky
The next installment in the series of backstage interviews with mathlib's active contributors!
Today, Johan Commelin interviews Yakov Pechersky. The first half of the interview's video was lost, so it was "recovered" via written communication.
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.