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

This is the repository for algorithm design.

AI-assisted Lean formalization for Economics and Computation research

Formally Verified Arguments of Knowledge in Lean

port of s2n-bignum to Lean

Legacy Complexitylib V1; development continues at cslib-community/complexitylib.

Lean cryptography library for prototyping/modeling protocols and proving protocol properties.

Distributed Graph Algorithms in Lean

A compositional toolkit for mechanised undecidability in Lean 4.

Functional Algorithms Design

Formally Verified Float Implementation with lean4

Esoteric Programming Languages, Formally

Lean 4 library for polynomial functors, interaction trees, and frameworks for modeling interactive and effectful protocols

Tensor-network theory, formalized in Lean 4: the fundamental theorem of matrix product states, canonical forms, parent Hamiltonians, matrix-product density operators, and projected entangled pair states, building on the QICLean quantum-information library

Machine-checked cryptographic proofs in Lean, built on Mathlib: oracle computations, probability semantics, program logic, and lattice- and hash-based schemes.