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

Formalization of Arithmetization of Mathematics/Metamathematics

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

A control flow graph library for Lean