The Lean research ecosystem, in one directory.

A Lean development of local and global class field theory and its algebraic foundations.

A formalization of toric geometry, including fans, cones, and the varieties they define.

A probability-theory development constructing and studying Brownian motion in Lean.

A formal library for higher category theory and infinity-cosmoi.

A broad formal library of results and exercises in modern combinatorics.

A reusable Lean library for automata, languages, and related computer-science proofs.

Shared APIs and formal foundations for computer science, software verification, and certified software in Lean.

A large source-linked collection of formal mathematical statements, including open questions and proved results. Statement review and mathematical status remain separate.

Community physics definitions, theorems, calculations, notation, tactics, and quantum-information developments.

Formal optimization models, verified reductions and relaxations, and proof-producing disciplined convex programming transformations.

A formal library for cryptographic games, probabilistic programs, relational reasoning, and quantitative Hoare logic.

A modular verification framework for interactive oracle reductions and modern zero-knowledge proof systems.

Reusable SSA semantics and MLIR integration for proving that compiler rewrites preserve meaning.

A Lean port of the Iris higher-order concurrent separation-logic framework.

A formal metatheory library covering axiomatic systems, syntax, semantics, proof theory, and incompleteness.

A multi-project workspace for Picard schemes, Quot schemes, Albanese constructions, line bundles, and Čech cohomology.

A Lean companion to Analysis I

Converts floating point numbers to decimal strings