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

Formally Verified Arguments of Knowledge in Lean

Document Generator for Lean 4

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

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

A project to digitalise results from physics into Lean.

⚠️ Experimental | Prototype

⚗️ | Soma is a general-purpose dependently-typed functional programming language powered by Interaction Nets with a minimal runtime.