Reservoir

Exceptions to the ABC conjecture in Lean

Advent of Code

Verify Cairo contracts in Lean 4

White-box automation for Lean 4

Algebra library for Lean 4

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

Formalization of Arithmetization of Mathematics/Metamathematics

Formally Verified Arguments of Knowledge 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.

Construction of a Brownian Motion in Lean

A formalisation of the Bruhat-Tits tree in Lean4