The open workbench for AI safety, made formal. Turn safety questions into machine-checked Lean proofs — a shared launchpad where researchers and AI agents build provable safety together.

Algorithms and Complexity Library using the lightweight query combinator framework called "Prog"

Formally Verified Arguments of Knowledge in Lean

An Universe for Mitar —— Classical Calculus

Document Generator for Lean 4

A project to formalize Fisher-Tippett-Gnedenko theorem (default project of course MS-EV0029)

Machine-checked statistical learning theory in Lean 4: empirical-Bernstein and time-uniform PAC-Bayes, Markov risk, Rademacher/VC, and Dudley chaining.

Formalization of Mathematical Logic

Formalization of Gröbner basis theory in Lean4 (WIP)

Haskell-inspired libraries for Lean 4 with maximalist typing

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

Proof of Kummer's criterion for regularity of a prime in Lean

✏️ | A cutting-edge, concurrent & performant Language Server Protocol (LSP) framework for Lean 4.

LeanEff is a small Lean 4 extensible-effects library

Lean specification of neural architectures with verified GPU codegen.

Link LMFDB and Lean