Exceptions to the ABC conjecture in Lean

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

Verify Cairo contracts in Lean 4

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

Formalization of Arithmetization of Mathematics/Metamathematics

Formally Verified Arguments of Knowledge in Lean

A formalized proof of Artin-Wedderburn theorem in Lean4

Binary Decision Diagrams in Lean 4

A proof of Pointwise Birkhoff Ergodic Theorem in Lean

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

Construction of a Brownian Motion in Lean

A formalisation of the Bruhat-Tits tree in Lean4

Proof exercises in Lean4 and Isabelle/HOL

Ejercicios de demostración con Lean4 e Isabelle/HOL.

A formalized proof of Carleson's theorem in Lean

A certified checker for Datalog entailments, written in Lean