Skip to main content

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.

Read more…

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.

Read more…

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.

Read more…

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).

Read more…