Reservoir

Exceptions to the ABC conjecture in Lean

A Lean companion to Analysis I

Formally Verified Arguments of Knowledge in Lean

repository for the collaborative formalization seminar in Analysis in Bonn

Construction of a Brownian Motion in Lean

Construction of a Brownian Motion in Lean

A formalized proof of Carleson's theorem in Lean

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

Central limit theorem in Lean

Distributed Graph Algorithms in Lean

A project to map out the relations between different equational theories of Magmas.

Exponent pair database

A project to formalize Fisher-Tippett-Gnedenko theorem (default project of course MS-EV0029)

Ongoing Lean formalisation of the proof of Fermat's Last Theorem

Fermat's Last Theorem for regular primes

Proof of Kaplanski criterion for being a UFD in Lean4

Formalizing "Proofs from THE BOOK"

Formalization of Gröbner basis theory in Lean4 (WIP)