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

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