The Fermat's Last Theorem Project
Kevin Buzzard discusses the project to prove Fermat's Last Theorem in Lean.
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.
Hello, everyone! My name is Jana Göken, a master's student in mathematics from Bremen. Today, I want to share with you my experiences at the Machine-Checked Mathematics workshop that introduced me to the world of proof assistants, specifically Lean. The workshop took place in Leiden from July 10th to July 14th 2023, and it was an amazing and educational journey.
Kevin Buzzard rounds up the BIRS conference on formalising cohomology theories.
In PR# 13250 we define modular forms and cusp forms, and prove that they form complex vector spaces. These are analytic functions of number theoretic interest with strong links to geometry, representation theory and analysis. Most famously they are a key ingredient in the proof of Fermat's Last Theorem. In this post we discuss the formalization process, motivate some design choices and map out some future work.
In October and November 2022 there were 512 and 453 PRs merged into mathlib. We list some of the highlights below.
Measure theory.
Algebra.
Analysis
Number theory.
Representation theory.
Topology.
Probability theory.
Algebraic and differential geometry.
Linear algebra.
Category theory.
Combinatorics
Tactics
During these two months, we got two new versions of Lean. We also started to systematically port mathlib to Lean4, see the wiki.
A few weeks ago, we announced the completion of the liquid tensor experiment (LTE for short). What this means is that we stated and (completely) proved the following result in Lean:
variables (p' p : ℝ≥0) [fact (0 < p')] [fact (p' < p)] [fact (p ≤ 1)] theorem liquid_tensor_experiment (S : Profinite) (V : pBanach p) : ∀ i > 0, Ext i (ℳ_{p'} S) V ≅ 0 := -- the proof ...
The code block above, which is taken directly from the file challenge.lean
in the main LTE repository, uses some custom notation to make the statement appear as close as possible to the main theorem mentioned in
Scholze's original challenge.
Fortunately, it's relatively straightforward to unravel the notation to see the underlying definitions themselves.
But there is a bigger issue: How can we convince ourselves (and others) that the definitions we introduced in LTE are actually correct?
For instance, we could have defined Ext
to be $0$ (spoiler: we didn't).
Or, we could have made some subtle innocent mistake in setting up the definitions that somehow implies that Ext
is always $0$, or that all condensed abelian groups are trivial, or one of several other pitfalls that renders the statement above meaningless.
To answer this question, we built a new examples
folder in the repository which contains several files corresponding to the main players in the statement above.
These examples can be considered as centralized "sanity checks" that the definitions we wrote using Lean actually behave as expected.
We tried to write the files in this folder in a way which should be (approximately) readable by mathematicians who have minimal experience with Lean.
The goal is to make it easy for non-experts to look through the examples folder, then look through the concise final statement in challenge.lean
, and be reasonably confident that the challenge was accomplished.
This blog post gives a detailed overview of this folder and its contents, and how it relates to the definitions used in the main statement of the liquid tensor experiment. It is meant to be read alongside the actual files from the examples folder.
In September 2022 there were 361 PRs merged into mathlib. We list some of the highlights below.
In August 2022 there were 506 PRs merged into mathlib. We list some of the highlights below.
In July 2022 there were 611 PRs merged into mathlib. We list some of the highlights below.