Searching for Theorems in Mathlib
A post for beginners on the different ways to search for theorems in mathlib, inspired by this talk from Jireh Loreaux.
The correspondence between affine group schemes and Hopf algebras
This February saw the birth of the Toric project, whose aim is to build the theory of toric varieties following Toric Varieties by Cox, Little and Schenck.
We soon discovered that toric varieties contained tori, and that Mathlib didn't.
This blog post is a double announcement:
- The unexpected prerequisite of algebraic tori was recently cleared;
- We are looking for contributors to help with the second phase of the project, i.e. toric geometry and its relation to convex geometry.
Theorems about abelian categories
Two significant results about abelian categories have recently been added to mathlib. The first is that any Grothendieck abelian category has enough injectives, and it follows from a general construction known as the small object argument. The second is the Freyd-Mitchell theorem which states that any abelian category admits a fully faithful exact functor to a category of modules.
Simprocs for the Working Mathematician
Lean v4.6.0 (back in February 2024!) added support for custom simplification procedures, aka simprocs. This blog post is the first in a series of three aimed at explaining what a simproc is, what kind of problems can be solved with simprocs, and what tools we have to write them.
Durham Computational Algebraic Geometry Workshop
A group effort to formalise some algebraic geometry in Lean.
Basic probability in Mathlib
How do I define a probability space and two independent random variables in Lean? Should I use IsProbabilityMeasure or ProbabilityMeasure?
How do I condition on an event?
This post answers these and other simple questions about how to express probability concepts using Mathlib.
Announcing the ∞-Cosmos Project
Emily Riehl introduces the ∞-Cosmos Project.
This month in Mathlib (May 2024)
The last Month in Mathlib posts date from before the port started, in November 2022. We apologise for the momentary disappearance. We aim to keep it a monthly occurrence from now on.
There were 667 PRs merged in May 2024.
The Fermat's Last Theorem Project
Kevin Buzzard discusses the project to prove Fermat's Last Theorem in Lean.
The first official release of Lean 4
Lean 4 has just made its first official stable release, with the arrival of v4.0.0.
We're excited to transition from only providing nightly releases to having regular stable releases.