The Lean research ecosystem, in one directory.

Verified quantum computing in Lean 4 with FFI bridge to Apple Silicon (Metal 3). Full NISQ stack, dependent types, formal circuit verification, and mathematical translators to Hamiltonians for autonomous AI.

A project to formalise Coxeter's frieze patterns

Advent of Code 2022 solutions: Lean4

port of s2n-bignum to Lean

State-of-the-art streams for Lean 4

Lean formalizations for the paper "Almost all primes are partially regular"

Port of the haskell time library to Lean 4 and verification of date calculations

A formalization of chip-firing games and the Riemann-Roch theorem for graphs using the Lean 4 theorem prover.

full featured async redis client for lean 4

Formalization of Game Theory in Lean4

Repository for the September 2023 Hausdorff School on Lean

A library to create and use Unicode tables based on the skip list data structure.

A library that shows how to use the Unicode skip list tables generation tool to create a table to test if a codepoint is numeric.

Low level utils (single precision float, byte spans, unboxed vector, finalization callbacks, fixnums, deque, slotmap etc; implemented via ffi)

Lean project on the Virasoro algebra (2-cohomology of the Witt algebra, definition of the Virasoro algebra, ...)

COMS 6998 (Fall 2025): Refinement-typed DSL for certified AIR constraints and lookups

Example specifications for the Lean Machines modelling framework

A Lean-based formalization of the Reactor model.