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).

Development monorepo for Hex: verified computational algebra in Lean 4 (polynomial factoring, LLL, and friends). Released aggregate: https://github.com/leanprover/hex

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

Lean formalization and Blueprint for integral-representation neural networks and ridgelet transforms

The Lean Machine Learning Library

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

Development repo for translating Software Foundations to Lean

LEAN library supporting statistics formalization

Lean documentation authoring tool

The Lean reference manual