11. Formal proofs in Lean

Most of AI is empirical, and its evidence is experiments and published results (09, 10). A smaller part is mathematics: learning theory, the theory of dynamic programming and RL, logic and search, probability for inference, the properties of metrics and of fairness criteria. That part has theorems, and theorems can be proved in Lean. This document defines the AI Lean package, what it formalizes, how a Lean statement is checked against the page, how a page's proof is linked step by step to the Lean proof, and the formal ladder F0 to F3. It copies algorithm's 2150/07 where it can; it has no cost model and no refinement of implementations, because the subjects here are theorems about learning, not programs.

11.1 Goals and limits

The Lean part of a node proves what its page states as a theorem: a bound, a convergence result, an impossibility result, a soundness result, a property of a definition.

It does not prove that a trained model has a property, that an implementation is correct, or that an empirical finding is true. The site says this in plain words on each page with a Lean part: "The Lean proof is about the mathematical statement on this page. It says nothing about any trained model."

Formal statements of empirical claims (a scaling law, an emergent ability) are forbidden: they would only formalize a definition and could mislead (rule F09).

11.2 The `AI` package

lean/
  lakefile.toml              package AI; requires mathlib
  lean-toolchain             leanprover/lean4:v4.35.0
  lake-manifest.json         mathlib at the tag that matches v4.35.0
  AI.lean                    imports every module (generated by aik lean index)
  AI/
    Prelude/                 shared definitions: finite hypothesis classes, samples, losses, MDPs, propositional formulas
    LearningTheory/
      PAC.lean               the PAC framework: realizable and agnostic
      FiniteClass.lean       the sample complexity bound for finite classes
      VCDimension.lean       VC dimension, shattering, the Sauer-Shelah lemma
      Rademacher.lean
      NoFreeLunch.lean
    Classical/
      Perceptron.lean        Novikoff's convergence theorem
      SVM.lean               the hard-margin problem and its dual (statements first)
    ReinforcementLearning/
      MDP.lean
      Bellman.lean           the Bellman operators are contractions in the sup norm
      ValueIteration.lean
      PolicyImprovement.lean
      Bandits.lean           regret definitions; the UCB1 bound (later)
    Probabilistic/
      BayesNet.lean          the factorization of a Bayesian network; d-separation soundness
      EM.lean                the monotonicity of EM's likelihood
    Logic/
      Resolution.lean        soundness and refutation completeness of propositional resolution
      HornForwardChaining.lean
      STRIPS.lean            plan validity and the soundness of progression
    Search/                  statements about AI search that algorithm does not own (5.9)
    Games/
      Minimax.lean           von Neumann's minimax theorem for finite zero-sum games
    SocialChoice/
      Arrow.lean
    Fairness/
      Impossibility.lean     calibration and equal error rates cannot hold together except in degenerate cases
    Metrics/
      F1.lean                bounds and the relation to precision and recall
      CrossEntropy.lean      cross-entropy is at least the entropy (Gibbs), with equality iff equal
      Softmax.lean           shift invariance, the gradient of log-softmax
    Networks/
      UniversalApproximation.lean   the statement of the theorem for continuous activations (Leshno et al.)
      Attention.lean         permutation equivariance of attention with no positional information
  AITest/                    #guard and decide tests of definitions on small instances (rule F06)

Pins:

Lean v4.35.0 and Mathlib at the matching tag, the same pins as algorithm (Q-34). manifests/toolchains.yaml names them. The monthly bump (11.11) moves them together with algorithm's.
Mathlib provides measure-theoretic probability, the contraction mapping theorem, finite sums, real analysis and linear algebra. The learning-theory, MDP and logic definitions that Mathlib lacks are built in AI/Prelude and, when they are general, offered upstream (11.10).
No other dependency in v1. A dependency is a pull request with a reason and the build time it adds.

The module path mirrors the node's area in CamelCase, as in algorithm, with the exceptions of registers/lean-paths.yaml for modules shared by many nodes (rule F07).

11.3 What is formalized

lean: expected in a node's front matter marks a theorem that should be formalized; the target is F2 (04.10). The curate step sets it by these rules:

Area	Targets (first list)	Mathlib support
learning theory	the finite-class PAC bound (realizable and agnostic, with Hoeffding); the Sauer-Shelah lemma; the fundamental theorem of PAC learning for binary classification (statement first, proof by M5); a no-free-lunch theorem for finite domains; Rademacher bounds for finite classes (Massart's lemma)	probability, Hoeffding through concentration results where present; finite combinatorics
classical learning	Novikoff's perceptron convergence theorem; the representer theorem (statement); convexity of logistic loss; the bias-variance decomposition of squared error	inner product spaces; convexity
reinforcement learning	the Bellman expectation and optimality operators are gamma-contractions in the sup norm; value iteration converges to the unique fixed point; the policy improvement theorem; policy iteration terminates in a finite MDP; the existence of a deterministic optimal stationary policy for finite discounted MDPs	the contraction mapping theorem; finite types
probabilistic reasoning	the chain rule factorization of a Bayesian network; soundness of d-separation for conditional independence (statement first); EM never decreases the likelihood	measure-theoretic probability; finite distributions
logic and planning	soundness and refutation completeness of propositional resolution; forward chaining for Horn clauses is sound and complete; STRIPS progression is sound	propositional logic structures
games and social choice	the minimax theorem for finite two-player zero-sum games; Arrow's impossibility theorem; the Gibbard-Satterthwaite theorem (later)	convexity and linear programming duality; finite orders
fairness	the impossibility of calibration within groups together with balance for both classes, except with equal base rates or perfect prediction (Kleinberg, Mullainathan and Raghavan); the binary-case incompatibility of predictive parity and equal error rates with unequal base rates (Chouldechova)	elementary real arithmetic
metrics and losses	cross-entropy is at least entropy, with equality iff the distributions are equal; KL divergence is non-negative (a bridge to math2's proof where it exists); F1 is the harmonic mean of precision and recall and lies between their minimum and their maximum; softmax is invariant to adding a constant; the gradient of log-softmax with cross-entropy is `softmax - onehot`	finite sums; real analysis
networks	universal approximation: the statement for continuous non-polynomial activations on compact sets (Leshno, Lin, Pinkus and Schocken), with the proof as a long-term target; permutation equivariance of self-attention without positions; the parameter count of a Transformer block equals the formula of `shapes.yaml` (a check that ties 08.6 to Lean)	continuous functions; Stone-Weierstrass is in Mathlib; matrices

Not formalized: theorems that algorithm owns (the correctness of k-means' Lloyd iterations, alpha-beta, A* optimality), which are linked to algorithm's Lean proofs through bridge cards; and theorems of pure mathematics that math2 owns.

Scale (Estimate): about 600 theorems at M5 (02.4), of which about 150 core theorems at F2, and the rest statements at F1 or proofs of supporting lemmas.

11.4 The structure of a module

/-
  Part of https://ai.tamnd.com/perceptron-convergence-theorem/ (ai://9QW4TR).
  SPDX-License-Identifier: Apache-2.0
-/
import Mathlib.Analysis.InnerProductSpace.Basic
import AI.Prelude.Samples

namespace AI.Classical.Perceptron

/-- One perceptron update on a mistake: `w ← w + y • x`. -/
def update (w x : E) (y : ℤˣ) : E := w + (y : ℝ) • x

/-- **The perceptron convergence theorem** (Novikoff 1962).
If every sample has norm at most `R` and some unit vector `u` separates the data with margin `γ > 0`,
then the perceptron makes at most `(R / γ) ^ 2` mistakes on any order of the samples. -/
theorem mistakes_le (S : Sample E) (R γ : ℝ) (hγ : 0 < γ)
    (hR : ∀ p ∈ S, ‖p.x‖ ≤ R) (u : E) (hu : ‖u‖ = 1)
    (hsep : ∀ p ∈ S, γ ≤ (p.y : ℝ) * inner u p.x) (order : Stream' (Fin S.length)) :
    mistakeCount S order ≤ ⌊(R / γ) ^ 2⌋₊ := by
  -- step: inner-grows
  have h1 : ∀ k, (k : ℝ) * γ ≤ inner u (weightAfter S order k) := by …
  -- step: norm-bounded
  have h2 : ∀ k, ‖weightAfter S order k‖ ^ 2 ≤ k * R ^ 2 := by …
  -- step: combine
  …

end AI.Classical.Perceptron

The code illustrates the form; the module that merges is checked by the build, and its names and hypotheses may differ.

The front matter of the theorem node names the module and the declarations:

lean:
  module: AI.Classical.Perceptron
  statement: AI.Classical.Perceptron.mistakes_le
  expected: true
  steps: derivations/proof.md        # the page proof whose steps are linked (11.6)

11.5 The axiom policy

As in algorithm 07.5: a theorem that a node cites as proved may depend only on propext, Classical.choice and Quot.sound. No sorry, admit, native_decide (which adds Lean.ofReduceBool), implemented_by in a cited declaration, or axiom of our own (rule F03). aik lean axioms prints the axioms of each cited declaration from the build, and the page shows them under "Axioms used".

Statements may be committed with sorry proofs, at F1, in modules marked -- status: statement-only in their header. The build counts them and never shows them as proved (rule F04).

11.6 Linking the page proof and the Lean proof (F3)

F3 asks that the proof on the page and the proof in Lean follow the same steps, so that a reader can move from one to the other.

The page proof (derivations/proof.md, 06.5) gives each step an id: {#step-inner-grows}, {#step-norm-bounded}, {#step-combine}.
The Lean proof marks the block that proves each step with a comment -- step: <id> on the line before a have, a calc or a tactic block (as in 11.4).
aik lean steps extracts both lists and checks (rule F08):
1. every step id of the page appears in the Lean proof, in the same order (a Lean proof may have extra internal steps, unmarked);
2. every marked Lean step builds on its own: the statement of the have is elaborated and recorded in build/lean/steps.jsonl;
3. the back-translation check (11.7) of each marked have agrees with the page step's text, as an advisory check.
The page renders the proof with a "Lean" toggle on each step, which shows the Lean statement of that step and links the source line (16.4).

11.7 Fidelity

A proof is only as good as its statement. Fidelity is the check that the Lean statement says what the page says.

Machine checks (needed for F1).

Not vacuous. The hypotheses are satisfiable: the module has an example that builds an instance meeting all hypotheses (a separable sample for the perceptron theorem; a two-state MDP for the Bellman contraction). Rule F05 checks that such an example exists for each cited theorem.
Definitions agree with the page on small cases. AITest/ evaluates the definitions on small instances and compares with the page's worked example (06.6): the Bellman update of the page's gridworld gives the page's values; F1 of the page's confusion matrix gives the page's number (rule F06).
Back-translation. A model writes the Lean statement back into English without seeing the page, and a model of another family compares it with the page's statement. A disagreement opens an issue. This check advises; it never raises a level.

Human review (needed for F1 to count on core nodes). A reviewer who is not the author records reviews/<tag>/lean-statement.yaml:

reviewer: alice                    # in registers/reviewers.reg
date: 2027-03-02
page_statement: blake3:…           # the statement section of the page
lean_statement: blake3:…           # the elaborated type of the cited theorem, from the extractor
page_proof: blake3:…               # derivations/proof.md, when the review covers the steps
verdict:
  statement_matches_page: yes
  hypotheses_match: yes            # or "stronger in Lean", with a note
  steps_match: yes                 # needed for F3
notes: >-
  The page says "a unit vector u"; Lean has hu : ‖u‖ = 1. Same meaning.

The review counts only while all hashes are current; any change drops the node until a new review, as in algorithm and math2 (rule F02). A reviewer checks in particular: the domain (finite or general hypothesis classes; discounted or average reward), the quantifiers (for all distributions, for some sample size), constants (a bound with a log(1/δ) and the exact constant the page prints), and that the page does not claim more than Lean proves.

11.8 The formal ladder F0 to F3

The ladder of 04.10, with the exact checks:

Level	Needs	Rules
F0	no Lean part
F1	the statement is in Lean and builds; the definitions pass the small-case tests; the hypotheses are shown satisfiable; for the core, the statement review is current	F01, F02 (core), F05, F06
F2	F1, and the theorem is proved with the standard axioms only	F03, F04
F3	F2, and the page proof's steps are linked to the Lean proof's steps, and the review's `steps_match` is current	F08

For a concept or metric node with a Lean part (softmax, F1, cross-entropy), F2 means its listed properties are proved. For a theorem whose page has no proof of its own (a long proof only cited), F3 does not apply.

11.9 Who writes the proofs

The prover role (14.2) writes statements from the page, then proofs. AI provers and proof assistants of any origin may be used; the kernel checks every proof, so the source of a proof does not matter for its truth, as in algorithm. The statement is the part that matters, and it is reviewed by a person for the core. A model of another family audits statements against the page before review (15.4).

11.10 Upstreaming

General definitions and lemmas (MDPs and Bellman operators, shattering and the Sauer-Shelah lemma, finite PAC bounds, propositional resolution) are offered to Mathlib when they meet Mathlib's standards. When Mathlib accepts one, the AI module re-exports Mathlib's version, and the old name stays as a deprecated alias for one release.

11.11 The monthly bump

The pins move once a month, together with algorithm's (Q-34): aik lean bump updates lean-toolchain and the Mathlib tag, builds the package, and opens a pull request with the list of broken declarations. A bump merges only when every F2 theorem still builds; a node whose proof breaks drops to F1 until it is fixed, and the bump report lists it.

11.12 Rendering on the site

The statement section shows the theorem in math, then a "Lean" tab with the elaborated statement, the module, the axioms used and the build date.
The proof section shows the page proof with the step toggles of 11.6 at F3.
The facts box shows "Proved in Lean" at F2 and "Lean statement only" at F1. The evidence label of the theorem's claim is proved at F2, or when the page's own proof is complete and reviewed (07.4).

11.13 The rules of this document

The rules are listed in 15.3 with their severities. In short:

Rule	Checks
F01	each Lean name in the front matter exists in `build/lean/decls.jsonl` with the expected kind, and the module builds
F02	the statement review of a core node is current for all its hashes
F03	cited theorems use only `propext`, `Classical.choice` and `Quot.sound`; no `sorry`, `admit`, `native_decide`, `implemented_by` or package axioms
F04	statement-only modules are marked, counted, and never shown as proved
F05	each cited theorem has an `example` that satisfies all its hypotheses
F06	the definitions agree with the page's worked example on the small-case tests
F07	the module path mirrors the node path, or is listed in `registers/lean-paths.yaml`
F08	at F3, every step id of the page proof appears in the Lean proof in order, and each marked step builds
F09	no Lean formalization of an empirical claim (a finding, a scaling law, a benchmark result)
F10	each module builds in at most 120 seconds on the CI runner

Source of this page