Exceptions to the ABC conjecture in Lean

ac-library for lean4

The sublibrary of Mathlib dedicated to additive combinatorics

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

Ongoing human written formal proof of Ado's theorem

Verify Cairo contracts in Lean 4

Lean formalizations of the paper "We Can't Agree to Disagree, Formally: Aumann's Theorem and Assumption Accounting in Lean"

Disproof of the Aharoni–Korman conjecture

The open workbench for AI safety, made formal. Turn safety questions into machine-checked Lean proofs — a shared launchpad where researchers and AI agents build provable safety together.

Atlas of formalised number theory in Lean (Verso blueprint)

Algorithms and Complexity Library using the lightweight query combinator framework called "Prog"

This is the repository for algorithm design.

Verified efficient algorithms in Lean4.

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

A Lean companion to Analysis I

tool for turning Lean proofs into Blender animations

Formalisation of the Kelley-Meka bound on Roth numbers