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)

Zero-sorry Lean 4 library of finite-sample statistical learning theory: PAC-Bayes (incl. a five-component test-time meta-bound), VC, Rademacher, sharp McDiarmid, and Dudley chaining. ICML 2026 AI4MATH

Formalization of Mathematical Logic

Haskell-inspired libraries for Lean 4 with maximalist typing

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 IREE codegen.

Link LMFDB and Lean

A Lean 4 library for formal linguistics: semantics, syntax, pragmatics, morphology, phonology, and processing — formalized across competing frameworks for high interconnection density.

simple web service in lean4

An introduction to numbers