A Lean companion to Analysis I

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

An introduction to theorem proving in Lean for the impatient.

Natural Number Game

Formalising Mathematics; a course for undergraduate mathematicians. Ran between January and March 2024.

Lean 4 kernel / 'external checker' written in Lean 4

Functional Programming in Lean

Companion files for Logical Verification 2020–2021 at VU Amsterdam

A small collection of formally verified junk theorems provable in Lean4 + Mathlib.

Formalizing "Proofs from THE BOOK"

Files associated with the course Interactive Theorem Proving at LMU SoSe 2024

My solutions to Tao's Analysis I, formalized in Lean

Lean Companion to the Category Theory in Context textbook by Emily Riehl

This is a repository on the formalization of Monsky's theorem by the UvA lean community.