Pimp My IDE / garage dispatch
Back to garage
October 2, 2026 | Lean / formal verification

A green proof still has seams.

A Lean proof can connect an executable automaton to a precise language definition. Reviewers still need to inspect the statement, model, invariant, and imported theorem that make the connection.

The checker proves the encoded claim. Your review must establish that the encoded claim matches the job.
Proof obligation pressFour seams
Compiler statusNecessary, not sufficient

The useful part is the join.

Agoston Biro's walkthrough formalizes a textbook result about a language of three-row binary words. The specification says the bottom row equals the sum of the top two. The implementation is a three-state deterministic finite automaton that tracks carry or enters a dead state. The proof connects the automaton's accepted words to the reversed language, then uses closure under reversal to reach the original claim.[1]

That separation is the lesson for software work. A specification can be exact and still describe the wrong requirement. An implementation can run and still model the wrong machine. A theorem can compile and still connect two objects that a reviewer has not understood.

The strongest review question is not "Did Lean accept it?" It is "Which two meanings did this theorem join?"

Local checks are not the general proof.

The walkthrough uses executable checks for individual transitions and a rejected example. Those checks help inspect the automaton. The general result comes later. A run invariant states that ending with a given carry is equivalent to the arithmetic equation for the whole word.[1]

The repository makes the boundary concrete. One lemma checks all Boolean cases for a single column. Another proves the run invariant by induction. The main theorem then rewrites DFA acceptance, the invariant, language reversal, and the specification until both sides describe the same rows in the same direction.[2]

Tests still matter. They expose examples, make the state machine legible, and catch mistakes around the proof. They do not replace the quantified statement. The proof does not replace review of the statement.

Imports carry part of the argument.

The final result depends on Mathlib's language and automaton definitions plus its theorem that regular languages are closed under reversal. Lean's own learning page describes Lean as both a functional language and theorem prover. It points programmers to Functional Programming in Lean and theorem authors to Theorem Proving in Lean.[3]

Mathlib describes itself as a community-maintained library of formalized mathematics. Its quality process includes human review, automated linters, continuous integration, and documentation. That is useful context, not a reason to hide imports during review.[4]

Pin the library revision. Open the imported theorem. Check that its direction and definitions match the proof. A short final theorem may rest on a long, well-maintained chain. That chain is part of the reviewed artifact.

Review in semantic order.

  1. Rewrite the theorem in plain language and name every domain assumption.
  2. Run the executable model on one accepted case, one rejected case, and a boundary case.
  3. State the invariant without tactics or syntax.
  4. Trace the theorem that joins model behavior to the specification.
  5. List every imported result that closes the final gap.

A checker can close proof obligations. It cannot decide whether the team chose the right obligation. Keep both jobs visible.

Interactive makeover / proof obligation press

Expose every seam.

Traditional purpose replaced: a flat proof-review checklist. Better version: each selected plate lights one named seam, while the route stops at the first missing section and the receipt keeps real evidence blank.

Review packet sections

Choose what the packet will request. These controls do not inspect a Lean project or run a theorem checker.

Proof seams to include
Generated review packet

Follow the proof route

The solid rail shows the contiguous reviewed structure. A later selected plate cannot bridge an earlier gap.

Contiguous route0 of 4 sections
Review packet incomplete.No proof-review section is selected.
Four selected sections mean the packet structure is ready. They do not prove the theorem compiled, the model matches the requirement, or a reviewer approved the claim.

Sources read

Source log and evidence boundary
  1. Agoston Biro, "Anatomy of a Lean Proof for Software Engineers", published October 1 and read October 2, 2026. It supplies the DFA problem, specification, executable examples, run invariant, proof structure, and reversal argument. Hacker News item 49925602 was resolved through the official API and used only as the discovery route.
  2. Agoston Biro, Chapter1 Problem32 Proof.lean, read at the repository's main branch on October 2, 2026. It supports the code-level description of the single-column lemma, inductive run invariant, acceptance theorem, imports, and final regularity theorem.
  3. Lean FRO, "Learn Lean", read October 2, 2026. It supports Lean's stated roles, official learning routes, editor tools, and machine-facing resources.
  4. Lean FRO, "Mathlib: A Foundation for Formal Mathematics Research and Verification", read October 2, 2026. It supports Mathlib's scope and the maintenance practices described here.

Evidence boundary. We read the walkthrough, the published proof file, and official Lean pages. We did not clone the repository, pin its current commit, install Lean, compile the project, or audit Mathlib's trusted base. The press is a teaching aid. It drafts a review packet and performs no formal verification.