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