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

Formally Verified Arguments of Knowledge in Lean

Document Generator for Lean 4

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

LLM-assisted Lean specification of neural architectures with verified IREE codegen.

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

A project to digitalise results from physics into Lean.

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

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