The Machine That Checks: What Lean Is, How It Works, and What It Finds in a Tangential Action Space

September 17, 2026

marcel blattner | august 26

Introduction

In the previous post on this blog, Lean appeared once, in a subordinate clause, as the reason mathematics sits at the top of the verification gradient. That was too little room for the thing doing the work. This post gives Lean the space, and then turns it on material from my own paper on Tangential Action Spaces.

Three questions organise what follows. Why a proof assistant matters now. How Lean produces its guarantee. And what happens to a geometric claim when it is restated in a language that accepts nothing on authority. The third section contains a complete Lean file, checked under Lean 4.33.0, that proves a discrete form of the cost-memory law.

Why the Kernel Is the Interesting Part

Lean is an open-source programming language and proof assistant, started by Leonardo de Moura and now developed by the Lean Focused Research Organization. The two descriptions are one system: the language you write programs in is the language you write proofs in, and a definition can be executed and reasoned about without translation between tools.

The property that matters is architectural. Whatever writes a Lean proof, a person, a tactic, a search procedure, a language model, the output is a term in a small formal calculus, and that term is rechecked by a kernel of a few thousand lines. The tactics are not trusted. The elaborator is not trusted. The automation is not trusted. Only the kernel and your own definitions are. A proof assistant built this way satisfies what Barendregt and Geuvers call the de Bruijn criterion, and the practical consequence is that the checking can be replayed by an independent program. Lean ships one, `leanchecker`, alongside the compiler.

Set that against the certificate problem from the previous post. For most of history a finished artifact certified an invisible process, and the diagnosis was that this link has broken: models now produce work whose form no longer indicates the reasoning behind it. A proof assistant does not repair the link. It makes the link unnecessary. The artifact is checked directly, so the question of what produced it stops being load-bearing.

This is why the adoption pattern looks the way it does. Tao's formalization of the Polynomial Freiman-Ruzsa conjecture, launched in November 2023 with Yaël Dillies and Bhavik Mehta, reached its primary goal in twenty-three days by splitting the argument into tasks that contributors claimed without needing to hold the whole proof in their heads. The Equational Theories Project that followed in September 2024 went further: Tao reports that machine-generated contributions were numerically the largest source, and they could be accepted because acceptance never depended on trusting the contributor. Mathlib, the shared library those projects build on, now holds more than 1.9 million lines of formally verified mathematics from over 500 contributors.

Industry arrived at the same architecture from the other direction. Amazon verifies core components of Cedar, the authorization language behind Amazon Verified Permissions and AWS Verified Access, against a Lean formalization, and tests the production Rust implementation against it continuously. Google DeepMind built AlphaProof on Lean. In both cases the reason is the same one the mathematicians have: a system that generates candidate answers is useful exactly to the degree that something else can reject the wrong ones cheaply.

How Lean Works

Lean rests on a single identification: a proposition is a type, and a proof of it is a term of that type. Proving `P` means constructing an object of type `P`, and checking a proof means type-checking that object. Verification and compilation become the same operation.

Dependent types make this expressive enough for mathematics. A type may mention a value, so `Vector Int n` is a type that depends on the number `n`, and a function may return a type that depends on its argument. Statements with quantifiers become function types: "for every integer `a`, `0 ≤ a * a`" is the type of a function taking an integer `a` and returning a proof about it.

Writing those terms by hand is impractical, so Lean provides tactics, small programs that build the term for you. `simp` rewrites with a database of equations, `omega` decides linear arithmetic over integers and naturals, and `grind` combines case analysis, congruence closure, and linear arithmetic over ordered fields and rings. The tactic script is a recipe. The term it produces is the proof, and the kernel checks the term, not the recipe. A tactic can therefore be as clever, heuristic, or machine-learned as its author likes without enlarging what has to be correct.

What remains inside the trusted boundary is your definitions. The kernel certifies that your proof establishes the statement you wrote. Whether the statement you wrote is the one you meant is not a question it can answer. This is the gap I described in the previous post through the thought experiment about Fermat's last theorem and the natural numbers containing zero, and it is the gap the next section walks into deliberately.

A Tangential Action Space, Formally

Tangential Action Spaces model an embodied agent as a hierarchy of manifolds joined by projections, from physical states to cognitive representations and onward to intentions. Going down is a projection and loses information. Coming back up is a lift, and the lift is not unique: many physical motions project to the same cognitive motion. They differ in energy, and they differ in what they leave behind. The paper proves that the energy-minimising lift is the horizontal one, that any path-dependent memory costs strictly positive excess energy, and that for small loops the excess grows quadratically with the memory induced.

To put this in Lean without depending on Mathlib, I stripped the geometry to its smallest instance that still has a fibre. Physical velocities live in `Int × Int`, cognitive velocities in `Int`, and the projection keeps the first coordinate. The fibre over a cognitive velocity is then everything that agrees with it in the first component and is free in the second.

‍

```lean
/-- A physical velocity: a cognitive component and a fibre component. -/
structure Step where
  cog : Int
  vert : Int

/-- The projection from physical to cognitive velocities. -/
def proj (s : Step) : Int := s.cog

/-- Kinetic energy under the identity metric on the physical space. -/
def energy (s : Step) : Int := s.cog * s.cog + s.vert * s.vert

/-- The horizontal lift of a cognitive velocity: no motion in the fibre. -/
def horiz (u : Int) : Step := ⟨u, 0⟩

/-- Energy spent above the horizontal lift of the same cognitive velocity. -/
def excess (s : Step) : Int := energy s - energy (horiz (proj s))
```

Six lines, and the first result is already available. Among all lifts of a cognitive velocity the horizontal one costs least, and it is the only one that does.

```lean
theorem horiz_minimises (s : Step) : energy (horiz (proj s)) ≤ energy s := by
  have h := mul_self_nonneg s.vert
  simp [energy, horiz, proj]; omega

theorem horiz_unique (s : Step) (h : energy s = energy (horiz (proj s))) :
    s.vert = 0 := by
  simp [energy, horiz, proj] at h
  have h2 : s.vert * s.vert = 0 := by omega
  rcases Int.mul_eq_zero.mp h2 with h1 | h1 <;> exact h1
```

A path is a list of steps. Along it, three quantities accumulate: the number of steps, the total excess energy, and the memory, which is the net displacement in the fibre, the discrete holonomy of the path.

```lean
def steps : List Step → Int
  | [] => 0
  | _ :: rest => 1 + steps rest

def totalExcess : List Step → Int
  | [] => 0
  | s :: rest => excess s + totalExcess rest

def memory : List Step → Int
  | [] => 0
  | s :: rest => s.vert + memory rest
```

The cost-memory law is now a statement about these three. Since `totalExcess` sums the squares of the fibre components and `memory` sums the components themselves, the claim is that the square of the sum is bounded by the length times the sum of squares, which is Cauchy-Schwarz in the form the geometry asks for. Read as a lower bound on cost, it says the excess energy of a path is at least the square of the memory divided by the number of steps: quadratic growth of cost in memory, matching the continuous result for small loops.

```lean
theorem cost_memory (p : List Step) :
    memory p * memory p ≤ steps p * totalExcess p

theorem no_free_memory (p : List Step) (h : memory p ≠ 0) : 0 < totalExcess p
```

The proofs, in the full file linked below, run by induction on the path and depend on nothing but the three standard axioms of Lean's logic, which `#print axioms` reports as `propext`, `Classical.choice`, and `Quot.sound`. There is no `sorry` anywhere in the file.

Because Lean is also a programming language, the same definitions run. Take a cognitive loop that closes, two steps forward and two back, and lift it three ways. The tuples below are the evaluated output, not a transcription.

```lean
def loop   : List Step := [⟨1,1⟩, ⟨1,1⟩, ⟨-1,1⟩, ⟨-1,1⟩]
def flat   : List Step := [⟨1,0⟩, ⟨1,0⟩, ⟨-1,0⟩, ⟨-1,0⟩]
def uneven : List Step := [⟨1,4⟩, ⟨1,0⟩, ⟨-1,0⟩, ⟨-1,0⟩]

-- (cognitive net, memory, steps, total excess)
#eval (cogNet loop,   memory loop,   steps loop,   totalExcess loop)    -- (0, 4, 4, 4)
#eval (cogNet flat,   memory flat,   steps flat,   totalExcess flat)    -- (0, 0, 4, 0)
#eval (cogNet uneven, memory uneven, steps uneven, totalExcess uneven)  -- (0, 4, 4, 16)
```

All three close in the cognitive space, and the first coordinate confirms it. The horizontal lift closes in the physical space too, retains nothing, and pays nothing. The other two return the agent to a different physical state than it started from, and that displacement is the memory. Both carry memory 4 over 4 steps, so the theorem sets their floor at 4. The evenly spread loop sits exactly on it. Gathering the same memory into a single step costs 16, four times the minimum. The bound is tight, and it is tight precisely when the fibre motion is distributed evenly along the path.

What The Kernel Made Explicit

Two things surfaced during the formalization that the informal argument passes over.

The first is a degenerate case. The induction step divides through by the number of earlier steps to recover the arithmetic-geometric mean bound, which requires that number to be positive. When the path has no earlier steps, the division is unavailable and the argument has to reach the conclusion another way: the inductive hypothesis gives that the memory so far is at most zero, nonnegativity of squares gives that it is at least zero, and only then does the case close. On paper this is the kind of step that gets absorbed into "and the base case is trivial". The kernel required it to be written.

The second concerns automation. `grind` handles the ring normalization and the linear arithmetic in the induction step without help. It does not prove `0 ≤ a * a`. Asked to, it treats the product as an opaque atom and reports a satisfying assignment in which the square is negative. Core Lean has no lemma for it either, so the file opens with an eight-line proof by cases on the sign. Once that fact is supplied as a hypothesis, `grind` closes the surrounding nonlinear goals immediately. The boundary of the automation is not where a mathematician would guess: the hard-looking inequality is routine, and the fact that squares are nonnegative is where the human has to step in.

Neither observation changes the mathematics. Both change what I know about the mathematics, which is the return on the exercise.

Discussion

The Lean development above is a discrete, finite-dimensional instance rather than a formalization of the paper's theorems. It uses integer arithmetic in place of the reals, a one-dimensional fibre in place of a general fibration, a fixed identity metric in place of an arbitrary Riemannian metric, and finite sums in place of path integrals. Under those choices the horizontal lift is the trivial one, and the pseudoinverse characterisation of the minimising lift, which is the substance of the paper's second theorem, becomes invisible. Holonomy appears here only as net fibre displacement, without the curvature that generates it. Reaching the continuous statements means working over `Mathlib`'s real numbers, inner product spaces, and manifolds, which is a considerably larger undertaking and the natural next step.

What the exercise does establish is that the cost-memory relation survives translation into a setting where every step is checked, and that the shape of the inequality, quadratic cost in memory, is not an artifact of the continuous analysis. It comes from the same place Cauchy-Schwarz always comes from.

There is a broader point here, and it is the one the previous post ended on. A verifier certifies the statement you wrote, not the one you meant. Everything the theorem above says about embodied agents is carried by the definitions of `energy`, `proj`, and `memory`, and the kernel has no opinion on whether those are the right definitions. Formalization moves the entire burden of judgement into the modelling. That is a smaller burden than the one it replaces, and it is more visible, which is most of the value.