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. Here is the second blog post.
A group effort to formalise some algebraic geometry in Lean.
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.
Emily Riehl introduces the ∞-Cosmos Project.
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.
Kevin Buzzard discusses the project to prove Fermat's Last Theorem in Lean.
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.