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.