Mathlib Announcements

Stream: mathlib4

[Floris van Doorn]

Activity in Mathlib has grown significantly over the last years, and it's hard to keep up with all the exciting developments that are going on. Therefore, we're launching this thread to collect announcements about exciting developments in and around Mathlib.

Have you formalized an important new definition or theorem, and did it get merged into Mathlib? Did an exciting tactic you wrote get merged into Mathlib? Did you finish a giant refactor, or significantly sped up Mathlib? Please post an announcement here!

Please keep this thread relatively low-volume, so this is not the place to announce the average PR (this happens in #rss > Recent Commits to mathlib4:master), and this should not be used to announce PRs that are not yet merged (you could post in #PR reviews, if desired).

Similar to the #announce channel, discussions about announcements should be held in a separate thread.

[Floris van Doorn]

We can start by also announcing some recent additions to Mathlib (say, in June).

[Floris van Doorn]

About the recent additions, I'm most excited about the grw tactic that @Jovan Gerbscheid got over the finish line, but for which @Patrick Massot, @Sebastian Zimmer, @Heather Macbeth and @Mario Carneiro have written earlier versions. We can now prove write proofs like this:

example (h₁ : a < b) (h₂ : b ≤ c) : a + d ≤ c + d := by
  grw [h₁, h₂]

example (h : a ≡ b [ZMOD n]) : a ^ 2 ≡ b ^ 2 [ZMOD n] := by
  grw [h]

example : (h₁ : a ∣ b) (h₂ : p ∣ a * d) : p ∣ b * d := by
  grw [← h₁]
  exact h₂

Discussion thread: #mathlib4 > Announcement: New `grw` tactic

[Kevin Buzzard]

I was very pleased a few days ago to see mathlib get another homology theory, namely group homology, in #25868 . Homology and cohomology theories have been notoriously slow to appear in mathlib, with singular homology taking years and de Rham cohomology still not here. Group homology is essential for Tate cohomology which is an integral part of the modern treatment of class field theory, the simplest case of the Langlands philosophy.

[Sébastien Gouëzel]

Riemannian manifolds are finally available in mathlib, with #27250. In addition to the definitions (which are not easy to set up correctly as one should avoid diamonds), there is a first easy theorem there: the proof that the topology induced by the distance coming from a Riemannian metric coincides with the prior topology of the manifold. The main goal of including the proof of this theorem in the PR is to show that the design just works.

[Kevin Buzzard]

One of the fundamental constructions of p-adic Hodge theory, namely Fontaine's de Rham period ring, is in mathlib as of #26388. This is a nonarchimedean field of "$p$-adic periods" which plays the same role as the complex numbers does in the classical theory of periods (a period is what you get when you integrate a sensible function along a sensible path). Geometers will know that when one uses complex coefficients, singular and de Rham cohomology of a manifold are naturally isomorphic in favourable cases, via integration of differentials along paths. There is a similar but far more profound relationship between etale and de Rham cohomology of a $p$-adic variety, but here one needs to use coefficients in $B_{dR}$. I write more about the history of getting this construction into mathlib here #mathlib4 > Milestone: B_{dR} @ 💬 .

[Joscha Mennicken]

The old speedcenter for mathlib4 performance benchmarking has now been completely replaced by radar. Like the speedcenter, radar lets you view the results for individual commits, compare commits, and view graphs of how metrics evolve over time. Alongside the new benchmark results, radar also contains the historical speedcenter data.

Similar to the speedcenter, radar tries to detect whether commits contain significant (i.e. interesting) changes, and posts those changes to #rss > Significant commits to mathlib4. I'll continue to monitor and tweak the significance detection to try to reduce false positives.

Radar also responds to !bench commands in pull requests. If you want to defer the bench run until CI successfully passes, tag your PR with the awaiting-CI tag before issuing the !bench command and radar will wait until the tag is gone before initiating the benchmark. This replaces the old bench-after-CI workflow.

For more details and questions, see radar's About page or visit #mathlib4 > mathlib4 speedcenter @ 💬.

[Ching-Tsun Chou]

(deleted)