formalization

An introductory course to Homotopy Type Theory

A formalization of geometry in Coq based on Tarski's axiom system

LeanEuclid is a benchmark for autoformalization in the domain of Euclidean geometry, targeting the proof assistant Lean.

The Symbolic, Mechanized, Observable, Operational SHell: an executable formalization of the POSIX shell standard.

[ICML2026] The first, fully verified, sorry-free, large-scale Lean 4 library for statistical learning theory, covering infrastructures for mordern statistics and learning theory.

Formalising Type Theory in a modular way for translations between type theories

Formalization of the Millennium Problems in Lean 4

Formalization of the polymorphic lambda calculus and its parametricity theorem

Formalization of Gröbner basis theory in Lean4 (WIP)

Deciding Presburger arithmetic in agda

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

Two-Level Type Theory

🧊 An indexed construction of semi-simplicial and semi-cubical sets

Official repository of the Autosubst 2 project.

Formalization of "Analysis I" by Terence Tao

A curated list of awesome interactive theorem prover frameworks

Real analysis formalized in Lean 4 from nothing — the reals are constructed here. No mathlib, no external dependencies, no typeclasses.

Workspace-first orchestration for long-horizon Lean 4 formalization agents.

(Mirror) A Music formalization library and DSL in Lean 4