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

Formally Verified Arguments of Knowledge in Lean

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

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

Repository hosting the resources for the Lean demo session of my talk presented at the weekly research seminar on CHallenges in ANalysis and GEometry (CHANGE) at the University of Trento on February 11, 2025.

Chess in Lean 4

Lean circuit DSL

Central limit theorem in Lean

Lean coding problem solving challenge website with proof verification