Reservoir

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

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

repository for the collaborative formalization seminar in Analysis in Bonn

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

Formalisation in the Lean theorem prover of the relation between corner-free sets and communication complexity

Chromatic polynomial in Lean4

Central limit theorem in Lean

Formalization of communication complexity in Lean

Catalog Of Math Problems Formalized In Lean

A formal consistency proof of Quine's set theory New Foundations

Distributed Graph Algorithms in Lean

Duality theory in linear optimization and its extensions