A Lean companion to Analysis I

Construction of a Brownian Motion in Lean

Lean formalization of the structure theorem for the single-qudit Clifford group

A cookbook for Metaprogramming in Lean4 containing code snippets to help you code!

The dependently-typed combinator calculus (DCC).

Verified computational algebra in Lean 4 — polynomial factoring, LLL, and friends

A formal verification project based on the work by Enric Cosme Llópez on "Higher-order categories".

The Lean Machine Learning Library

Interactive React-powered charting library for Lean 4 in VS Code's infoview

Formally verified mathematical finance in Lean 4. Black–Scholes/Greeks/PDE, Itô calculus, FTAP/Girsanov, CRR→BS convergence, Merton jump-diffusion.

Notes in PhysLean

numpy -> lean 4 through ai

PDE Lean formalization

Lean documentation authoring tool

The Lean reference manual

「The Lean Language Reference」の日本語訳（作業中）