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.

Advent of Code

Verify Cairo contracts in Lean 4

White-box automation for Lean 4

Disproof of the Aharoni–Korman conjecture

Algebra library for Lean 4

Verified efficient algorithms in Lean4.

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

Verified Optimizing Compiler for Cryptographic Primitives

tool for turning Lean proofs into Blender animations

Formalisation of the Kelley-Meka bound on Roth numbers

Formal verification of apportionment theory.

Don't disturb my circle!

Formalization of Arithmetization of Mathematics/Metamathematics

Formally Verified Arguments of Knowledge in Lean

Verified algorithms in Lean, implemented and proved by AIs

A formalized proof of Artin-Wedderburn theorem in Lean4

Automata theory in Lean