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.
For more information about Lean and formalization of mathematics, see the Lean community website.
In May 2022 there were 606 PRs merged into mathlib. We list some of the highlights below.
In April 2022 there were 661 PRs merged into mathlib. We list some of the highlights below.
March 2022 saw a record number of new contributions to mathlib: 682 PRs were merged, obliterating the old record of 565 merged PRs.
February 2022 saw 501 commits to mathlib. In this post we highlight some of these contributions.
January 2022 saw 533 commits to mathlib. In this post we highlight some of these contributions.
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.