Exceptions to the ABC conjecture in Lean

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

The proof that the adele ring of a number field is locally compact, formalised in Lean 4.

Verify Cairo contracts in Lean 4

Disproof of the Aharoni–Korman conjecture

Verified efficient algorithms in Lean4.

Lean formalization of aperiodic monotiles papers (staging repository for material not yet in mathlib)

tool for turning Lean proofs into Blender animations

Formal verification of apportionment theory.

Don't disturb my circle!

Formalization of Arithmetization of Mathematics/Metamathematics

Formally Verified Arguments of Knowledge in Lean

A formalized proof of Artin-Wedderburn theorem in Lean4

Automata theory in Lean

Binary Decision Diagrams in Lean 4

Project for "Machine-Checked Mathematics" at the Lorentz Center

A proof of Pointwise Birkhoff Ergodic Theorem in Lean

repository for the collaborative formalization seminar in Analysis in Bonn

Formalization project on analysis of Boolean functions in Lean 4, including a proof of Arrow's theorem via Fourier analysis.