# This month in mathlib (Aug 2022)

In August 2022 there were 506 PRs merged into mathlib. We list some of the highlights below.

# This month in mathlib (Jul 2022)

In July 2022 there were 611 PRs merged into mathlib. We list some of the highlights below.

# This month in mathlib (Jun 2022)

We apologize for the delay in posting this overview. In June 2022 there were 460 PRs merged into mathlib. We list some of the highlights below.

# Classification of one-dimensional isocrystals

Last year, there was a big mathlib refactor to replace linear maps throughout the library with semilinear maps, a more abstract concept which, importantly, unifies linear and conjugate-linear maps.

But this is not the full extent of the generalization! Our number theorist friends here in mathlib told us that we should make sure we chose this full generality of semilinear maps, maps $f:M \to N$ such that $f(ax)=\sigma(a)f(x)$ for some ring homomorphism $\sigma$ between the scalar rings of the modules $M$ and $N$. So we and our coauthor Frédéric Dupuis implemented this full generality, and then asked them for an example to illustrate their need for this more abstract definition. This blog post tells the story of our little adventure in number theory.

It turns out that the standard use of semilinear maps in number theory is for Frobenius-semilinearity, semilinearity with respect to the ring homomorphism of the fraction field of the $p$-typical Witt vectors over a perfect characteristic-$p$ integral domain which is induced by the Frobenius automorphism of that domain. Let's backtrack to catch everyone up...

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

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