Lean 4 Proof Corpus

A machine-checked library of mathematics across the spine of modern AI: optimisation, dynamical systems, learning theory. Each repository states its axioms and any documented gaps. Most are zero-sorry.

by velvetmonkey · ORCID · Claims need receipts.

★ Featured demo  ·  Hebbian Kuramoto — Basin Boundary  interactive showcase →

Convex optimisation & gradient methods

• gradient-descent-lean — GD convergence for smooth convex optimisation. 17 theorems, zero sorry.
• nesterov-lean — Nesterov accelerated gradient descent.
• heavy-ball-lean — Polyak heavy-ball convergence.
• proximal-gd-lean — Proximal gradient descent for composite objectives.
• projected-gd-lean — Projected gradient descent convergence.
• subgradient-lean — Subgradient method for nonsmooth convex objectives.
• mirror-descent-lean — Mirror descent with Bregman divergence.
• frank-wolfe-lean — Frank-Wolfe (conditional gradient).
• coordinate-descent-lean — Cyclic coordinate descent convergence.
• admm-lean — ADMM convergence, primal/dual residuals.
• newton-lean — Newton's method quadratic convergence.
• sgd-lean — Stochastic gradient descent convergence.

Learning theory & online learning

• pac-learning-lean — PAC learning bounds, Hoeffding inequality.
• online-learning-lean — FTRL regret bounds for online convex optimisation.
• replicator-lean — Replicator dynamics on the standard simplex.

Dynamical systems & stability

• kuramoto-lean — Finite-N Kuramoto synchronisation.
• lyapunov-odes-lean — Lyapunov stability for autonomous ODEs.
• lasalle-lean — LaSalle's invariance principle.
• barbalat-lean — Barbalat's lemma and the Lyapunov-Barbalat route.
• contraction-lean — Contraction theory, Banach fixed point.
• lotka-volterra-lean — Lotka-Volterra predator-prey dynamics.
• langevin-lean — Bounded-noise Langevin dynamics.

Neural & associative memory

• hopfield-lean — Hopfield network energy descent.
• modern-hopfield-lean — Modern Hopfield network energy descent.
• attention-lean — Hard-attention expressivity (Mathlib).

Linear algebra & logic

• schur-complement-lean — Schur complement nonsingular-inverse API and block matrices.
• trace-logic-lean — Hoffman trace logic formalisation.

Physics

• hamiltonian-lean — Hamiltonian mechanics and Liouville's theorem.
• observer-patch-holography — OPH: finite observer-patch reconstruction (active research).