Lean 4 Proof Corpus

Small, machine-checked abstractions for AI reliability claims: optimisation, dynamical systems, consensus, safety. Each repository names the abstraction, proves the boundary, and states its axioms and non-claims. Most are zero-sorry.

by velvetmonkey · ORCID · Claims need receipts.

One thesis: the results that make learning systems trustworthy, convergence, stability, consensus, generalisation, should be checkable down to their axioms. Each repository proves one such result and shows its footprint.

This is a research index, not a monolith. Each entry is a small, checkable piece of the mathematics under modern AI: a convergence rate, a stability basin, a consensus guarantee, proved in Lean 4 and published with its theorem statements, axiom footprint, and any remaining gaps visible in the source. The unit of work is one auditable claim, not one grand library.

The corpus is also a bet about method: that a narrow theorem driven honestly to zero sorry is worth more than a broad formalisation with hidden gaps. Start with a concrete theorem, keep the model narrow enough to audit, and publish what was proved, what was assumed, and what was left out. Some entries are mature proof bricks; others are active research notes. Where these convex and classical results bound the non-convex systems used in practice, that boundary is stated, not blurred.

The definition is the work. The proof is often just the receipt; the invention is finding the smaller shape a messy claim really has, and naming it. The method is one seam: a messy AI or systems claim, narrowed to the smallest faithful model, given a named abstraction, driven to a theorem boundary, with its non-claims stated, and connected back to a usable software or research story. Not a stack of isolated textbook lemmas. Architecture at the theorem boundary.

★ Featured demo  ·  Hebbian Kuramoto — Basin Boundary  interactive showcase → ★ Featured demo  ·  The Coordination Kernel — proof-linked consensus  interactive showcase →

Two load-bearing bricks anchor the corpus, each a field where a proven boundary is itself the product:

• AI expressivity — attention-lean: the Fixable abstraction gives exact per-function head counts for single-layer hard attention (parity on n bits needs n heads; strict majority on 5 bits needs exactly 4). A machine-checked lower bound on what the architecture can compute.
• Distributed coordination — crdt-lean: strong eventual consistency and conditional liveness, with fairness and quiescence stated, not blurred.

Lead repositories

• Research novelty
  attention-lean — Exact finite-model theory of single-layer hard attention (Mathlib): head output = Fixable = decision list, giving exact per-function head counts. Parity on n bits needs n heads; strict majority on 5 bits needs exactly 4. First witness-vs-certificate gap, k(maj5)=4, machine-checked to a three-axiom footprint, zero sorry. Paper (Zenodo, DOI 10.5281/zenodo.21188381).
• Assurance engineering · proof to system
  temporal-logic-lean — LTL + monitor soundness over the safety fragment. Enforcement proved as a theorem for traces generated by the verified monitor, not axiomatised. Zero sorry, axiom-clean.
• System-tied formalization
  kuramoto-lean — Finite-N Kuramoto synchronisation: 34 proved statements, zero sorry. Continuous convergence to synchrony for any symmetric coupling with a uniform positive off-diagonal floor (all-to-all as a corollary), from open-semicircle initial conditions; plus a discrete fleet-clock line proving coordinator-free convergence to zero phase skew. The dynamics spine under flywheel-universe.
• Distributed-systems proof library
  crdt-lean — State-based CRDT convergence (AP): Strong Eventual Consistency, conditional liveness (assuming fairness and quiescence, stated not blurred), concrete instances including OR-Set add-wins and RGA sequence convergence.

The rest is the supporting corpus: proof bricks for the mathematics the lead results rest on, grouped by area. Useful evidence of range; the identity above is the point.

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

• 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.

Distributed systems & consensus

• consensus-lean — Quorum-based consensus safety (CP): intersection implies agreement, at most one value chosen.

Neural & associative memory

• hopfield-lean — Hopfield network energy descent.
• modern-hopfield-lean — Modern Hopfield network energy descent.

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).