Lean 3's obsolete mathematical components library: please use mathlib4

A Lean companion to Analysis I

Demo for high-performance type theory elaboration

The Lean Computer Science Library (CSLib)

Metamath Zero specification language

Simple verification of Rust programs via functional purification in Lean 2(!)

Perfectoid spaces in the Lean formal theorem prover.

The Hitchhiker's Guide to Logical Verification (2025 edition) and associated materials

A gamification of the theorems in MATH40002 Analysis 1

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

This may become a formalization of smooth manifolds in lean

Condensed mathematics in Lean