We had a Lean file that was sorry-free. Every theorem in it was true. Nothing in it was wrong. And a false claim sat next to it for months, in a LaTeX document, saying something the Lean file could have refuted instantly — if anyone had thought to ask it.
This entry is about why that happened, and the cheap change that catches it.
The file is DarkTower/Patterns/Propagator.lean. It reasons about
a family of eight-position propagators, and it states its theorems over
Equiv.Perm — Lean's type of bijections. That is a
reasonable choice: the objects we cared about are permutations of eight
positions, and there are 8! = 40,320 of them.
Elsewhere, in prose, we wrote a claim of the form: a 2015 paper's mechanism is a member of this family.
The mechanism in question is the map
k ↦ max(k-1, 0)on positions 0–7. Write it out:
| input k | 0 | 1 | 2 | 3 | 4 | 5 | 6 | 7 |
|---|---|---|---|---|---|---|---|---|
| output | 0 | 0 | 1 | 2 | 3 | 4 | 5 | 6 |
Position 0 is written twice. Position 7 is written
never. So this map is not a bijection — it has no inverse, and
it cannot be constructed as an Equiv.Perm at all.
Here is the part worth sitting with. In Lean, our claim was not false. It was inexpressible. You cannot even write down the sentence "this map is in the family", because you cannot produce the term the sentence needs. The type system contained the refutation, as a typing obstruction, and never surfaced it — because a typing obstruction only speaks when someone tries to type the thing.
A proof assistant checks theorems. It does not check the relevance of theorems.
The load-bearing claim — "…and this is what our system is" — lived outside the formalism by construction. Being sorry-free was a fact about the file's types, not about the world.
The thing that finally caught it is a unit test, in
futon5/test/futon5/exotype/invariants_test.clj. It does not prove a
theorem. It constructs the actual map and counts:
(let [bug (mapv #(max (dec %) 0) (range 8))
counts (frequencies bug)]
(is (= 2 (get counts 0)) "position 0 is written twice")
(is (nil? (get counts 7)) "position 7 is never written")
(is (not= (into {} (map #(vector % 1) (range 8))) counts)
"the bug is therefore not a permutation, and not in the 8! family"))Alongside it, the companion assertion over the real propagators: every permutation in the family writes each of the eight positions exactly once — 12.5% each. The disputed mechanism produces roughly 25% at position 0 and 0.000% at position 7. Those histograms cannot be the same shape, which is the whole argument, executable in about a second.
The Clojure test is in every way the weaker artifact. It proves nothing universally; it checks one case by enumeration. And it is the one that found the error, because it could state the claim that mattered.
| kind | what it establishes | who is good at it |
|---|---|---|
| model-internal proof | properties of an idealisation | Lean, extremely |
| model–artifact bridge | whether the running thing satisfies what the model says about it | almost nothing, so far |
Reviewing our own failures of the last months, every one is the second kind. A function claimed to be stochastic per cell and was not. A configuration claimed to describe a component and did not. A paper's mechanism was claimed to be in a family and was not. In each case the model was fine and the sentence about the model was wrong.
Lean sits entirely on the model side. That is not a criticism of Lean — it is a statement of what a proof assistant is for. The consequence is an ordering:
Bounds live in tests, not docstrings. One of our defects was
a rate that violated a bound stated in a docstring. Nothing reads a docstring. A
test that asserts fix(σ)/8 ≤ rate ≤ 1 across every named propagator
and 500 random permutations reads it every build.
A hole gets a test, not a comment. Where something is
genuinely unverified, we now write a test named hole-… that pins
the current unsatisfactory state — with the numbers, and a dated note
of how they have moved. A comment saying "unverified" ages silently. A test
saying "exactly 4 of 12 candidates are distinct here, and last month it was 2"
cannot: any change to that number fails the build and demands an explanation.
Mutate the test to prove it can fail. Each new check was verified by reintroducing the real defect it was written for and confirming the check dies. This matters more than it sounds:
A test that cannot fail is worth nothing.
The same applies to the scan that enforces the first practice: it asserts that it still finds instances of each class it classifies, so it cannot quietly degrade into a vacuous pass when files move. A check that passes because it is looking at nothing is worse than no check, because it also produces confidence.
The honest accounting: the refutation was available the whole time, in a file we had written ourselves, and the reason nobody retrieved it is that nobody knew to pose the question in a form the file could answer. That is the same shape as a library whose contents are technically present but unreachable by the vocabulary a reader would actually use.
What we do not yet have is a general way to know which claims are load-bearing enough to deserve a bridge. Our current rule is blunt: if a claim would embarrass us in a paper, it needs an executable check or an explicitly declared hole — and silence is the only forbidden option. That rule is a stopgap, and improving it is open.
The generalisation that would have prevented this one is stated and not yet done: state the theorems over general endomaps rather than permutations. Then "is this mechanism in the family?" stops being prose and becomes a typing question — which moves the load-bearing claim inside the formalism, the only place a formalism can help.