Fermat's Last Theorem

Ongoing Lean formalisation of the proof of Fermat's Last Theorem

Prime Number Theorem and ...

blueprint for prime number theorem and more

The Polynomial Freiman-Ruzsa Conjecture

Repository for formalization of the Polynomial Freiman Ruzsa conjecture (and related results)

∞-Cosmos

A blueprint for a formalization of infinity-cosmos theory in Lean.

Carleson operators on doubling metric measure spaces

A formalized proof of Carleson's theorem in Lean

Fermat's Last Theorem for regular primes

Fermat's Last Theorem for regular primes

Cambridge Combinatorics in Lean

Formalisation of the Cambridge Part II and Part III courses Graph Theory, Combinatorics, Extremal and Probabilistic Combinatorics in Lean

Combinatorial Games in Lean

Combinatorial game library in Lean 4

The sphere eversion project

Formalization of the existence of sphere eversions

Brownian motion project

Construction of a Brownian Motion in Lean

Arithmetic Progressions - Almost Periodicity

Formalisation of the Kelley-Meka bound on Roth numbers

Class Field Theory

Github repository for the 2025 Clay Summer School on Formalizing Class Field Theory

Toric varieties

Formalisation of toric varieties in Lean 4

add-combi

The (currently unofficial) sublibrary of Mathlib dedicated to additive combinatorics

Gibbs Measures

ASCI Summer Research Lean

Brauer Group

None

Decomposition of Persistence Modules

Formalizing the Structure Theorem for Persistence Modules

Chandra-Furst-Lipton

Formalisation in the Lean theorem prover of the relation between corner-free sets and communication complexity

Miscellaneous results by Yaël Dillies

Miscellaneous projects I am working on in Lean

Forbidden Matrix Theory

Formalisation of forbidden matrix theory

lean-liquid

maintained by @jcommelin

Liquid Tensor Experiment is a challenge by Peter Scholze to formalize parts of condensed mathematics, culminating in the main theorem of liquid modules.

flypitch

maintained by @jesse-michael-han @fpvandoorn

The Flypitch project gives a formal proof of the independence of the continuum hypothesis from ZFC. The continuum hypothesis states that there is no cardinality between the smallest infinite cardinal and the cardinality of the continuum. This project also develops a library of first-order logic, set theory and forcing.

lean-gptf

maintained by @jesse-michael-han @jasonrute @tonywu95 @edayers @spolu

Provides an interactive frontend to Lean GPT-f, a neural theorem prover which relies on a large Transformer language model to suggest tactics. It can prove nearly 50% of the remaining theorems in a held-out test set. See Jason Rute's talk at Lean Together 2021.

lean-perfectoid-spaces

maintained by @kbuzzard @jcommelin @PatrickMassot

Perfectoid spaces are sophisticated objects in arithmetic geometry introduced by Peter Scholze in 2012. We formalised enough definitions and theorems in topology, algebra and geometry to define perfectoid spaces in Lean. See also our project webpage and paper.

lean-matrix-cookbook

maintained by @eric-wieser

This project aims to provide the lemmas in The Matrix Cookbook as proofs in the Lean theorem prover. Ideally, every proof in this repository should be a reference to a single lemma in Mathlib; this can be used as an index against (and progress report for) mathlib for standard matrix results.

sudoku

maintained by @TwoFx

This is an implementation of sudoku, written in Lean. When you open a level in VS Code, a sudoku board is displayed in the goal view. You can put numbers (and also pencil marks) on the board by adding hypotheses, but you have to prove that the placement of the number follows logically from what is already on the board! There are some tactics to help you with this, and you can also prove theorems to build up your personal library of sudoku theory.

con-nf

maintained by @YaelDillies @zeramorphic

A formalisation of the consistency of Quine's New Foundations axiom system, following Randall Holmes' proof. This is arguably the longest standing open question in set theory.

lftcm2020

maintained by @jcommelin @PatrickMassot

This repository contains tutorials about Lean and mathlib that were developed for the workshop Lean for the Curious Mathematician, held in July 2020. The tutorials range from introductory lessons on numbers, logic, and sets to advanced lessons on category theory and manifolds. In addition to the materials found in this repository, we recommend watching the videos of the tutorials and lectures from the workshop.

topos

maintained by @b-mehta

This repository contains formal verifications of results in Topos Theory, drawing from "Sheaves in Geometry and Logic" and "Sketches of an Elephant". It currently includes a range of constructions and theorems about both Grothendieck topoi and elementary toposes.

flt-regular

maintained by @alexjbest @riccardobrasca @ericrbg @CBirkbeck

The goal of this project is to formalize Kummer's proof of Fermat's Last Theorem for regular prime exponents. This was a landmark 19th century result in algebraic number theory, proving the theorem in many new cases at the time, but is quite different to the final proof of the full theorem, due to Wiles-Taylor. This project hopes to add more material on algebraic number theory and related topics to mathlib in addition to formalizing a version of Kummer's proof.

lean-ga

maintained by @eric-wieser @utensil

A formalization of parts of Geometric Algebra, and the source from which most of the clifford_algebra library graduated to mathlib.

sphere-eversion

maintained by @PatrickMassot @fpvandoorn @ocfnash

In this project we formalize the proof of existence of sphere eversions in Lean. More precisely, we aim to formalize the full h-principle for open and ample first order differential relations, and deduce existence of sphere eversions as a corollary.

mathematica

maintained by @robertylewis @minchaowu

Connects Lean to the computer algebra system Mathematica. This project offers a bi-directional translation between the two systems. From within Lean, you can evaluate Mathematica commands, possibly including translated Lean expressions, and process the results. From Mathematica, you can access a Lean environment.

Examples of calling Mathematica from Lean can be found at robertylewis/mathematica_examples, and examples in the other direction at minchaowu/mm-lean. These repositories are not in the contrib list because they depend on Mathematica, which is proprietary software. See also our project webpage with a link to our paper about this project.

rubiks-cube-group

maintained by @kendfrey

This project formalizes the Rubik's cube group as a product of corner orientation, corner permutation, edge orientation, and edge permutation.

The solvable subgroup is defined as the the set of positions where both orientations sum to 0 and the permutations have the same sign.

This project includes a widget to visualize elements of the group as physical puzzle states.

lean-social-choice

maintained by @asouther4 @benjamindavidson

Social Choice Theory is a theoretical framework at the intersection of philosophy, political science, and welfare economics. It studies methods for aggregating individual preferences into collective social welfare functions.

This is a library of noteworthy proofs from Social Choice Theory formalized in Lean.

super

maintained by @gebner

Version one of a small superposition prover written in Lean. This repository introduces a tactic super which attempts to solve problems in first order logic, possibly given a list of extra hypotheses.

This version is not compatible with community releases of Lean.

unit-fractions

maintained by @b-mehta @TFBloom

This project formalizes the main results of the preprint On a density conjecture about unit fractions in Lean. One of these results says that any dense set of naturals contains distinct naturals whose reciprocals sum to 1.

grammars

maintained by @madvorak

The aim of the project is to formalize the Chomsky hierarchy. So far, the main focus has been to prove closure properties of general (type 0) grammars. We also have some results about context-free (type 2) grammars.

lean-acl-pairs

maintained by @adamtopaz

This project contains formalization of the relationship between so-called acl-pairs and valuation rings. If K and F are two fields, a pair of (group) morphisms f g : Kˣ → F is called an acl-pair provided that f u * g v = f v * g u whenever u + v = 1 in K. The main result regarding such pairs shows that they essentially always arise from valuation theory, at least when F is a prime field (such as ℚ or zmod p where p is prime). The proofs formalized in this repository are based on ideas of Bogomolov-Tschinkel, Efrat, Koenigsmann, and the author. This repository also formalizes some results about rigid elements and valuation which are due to Arason-Elman-Jacob.

super2

maintained by @gebner

Version two of a small superposition prover written in Lean. This repository introduces a tactic super which attempts to solve problems in first order logic, possibly given a list of extra hypotheses.