Introducing Mathlib Changelog
Tldr; check out mathlib-changelog.org to explore the historical changes to mathlib, and find out what happened to that lemma you were using.
Completion of the Liquid Tensor Experiment
We are proud to announce that as of 15:46:13 (EST) on Thursday, July 14 2022 the Liquid Tensor Experiment has been completed. A year and a half after the challenge was posed by Peter Scholze we have finally formally verified the main theorem of liquid vector spaces using the Lean proof assistant. The blueprint for the project can be found here and the formalization itself is available on GitHub.
The first major milestone was announced in June last year. The achievement was described in Nature and Quanta.
For more information about Lean and formalization of mathematics, see the Lean community website.
The ring of integers of a cyclotomic field
In PR #13585 we compute the discriminant of cyclotomic fields. This is an important result, usually treated in a first year graduate course in number theory. In this post we would like to explain why it is an important result, and briefly explain how we proved it.
This month in mathlib (May 2022)
In May 2022 there were 606 PRs merged into mathlib. We list some of the highlights below.
This month in mathlib (Apr 2022)
In April 2022 there were 661 PRs merged into mathlib. We list some of the highlights below.
This month in mathlib (Mar 2022)
March 2022 saw a record number of new contributions to mathlib: 682 PRs were merged, obliterating the old record of 565 merged PRs.
This month in mathlib (Feb 2022)
February 2022 saw 501 commits to mathlib. In this post we highlight some of these contributions.
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.