The Lean research ecosystem, in one directory.

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.

An experimental framework for symbolic and numerical computing, automatic differentiation, differential equations, and optimization in Lean.

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

Typed tensors, neural-network graph semantics, finite-precision reasoning, runtime integration, and certificate checking.

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 implementation of a Lean kernel with formal metatheory. The project documents that it is not a fully independent kernel implementation.

Formal semantics and machine-checked results for the Cedar authorization language, with differential testing against the production implementation.

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

A completed formalization of the difficult part of the consistency proof for Quine's New Foundations set theory.

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

A formalization of Harder-Narasimhan filtrations and related results for vector bundles.

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

A Lean companion with definitions, examples, theorem statements, and exercises from Category Theory in Context.