THE SITE DIAGNOSIS TABLE

the sites that did not come out, and what stopped each one

The Cleanable Table lists what came out. On its own that is a numerator with no denominator, and a numerator with no denominator is how a removal rate gets quoted as though it were a possibility rate. This is the rest.

Of 765 sites examined, 340 — 44.4% — were never testable. The occurrence is not in a position where an instance would be supplied, so there is no proposition to hand to synthesis and nothing to substitute. That is a fact about the shape of the proof term rather than about whether the mathematics needs choice.

Measured with gonzalgo · Lean 4.32.1 with Mathlib v4.32.1 · instance synthesis attempted per occurrence, inside the declaration's own context

Showing the first 120 of 765 rows. Grouped by verdict, so the head of the table is one category. The full set is in the JSON and the CSV.

proposition is the goal an instance would have had to be found for, where there was one. A not-a-goal row often shows Classical.propDecidable bare or partly applied, which is the case where there is nothing to decide.

Get the data

site-diagnosis.json · site-diagnosis.csv · CC-BY-4.0 · version 2026-08-12

One of the gonzalgo indexes — standing measurements of what formal libraries rest on, remeasured as the libraries move. Cite the series as 10.5281/zenodo.21900625, which resolves to the current deposit.

Reproduce it

lake env lean -D maxErrors=4000 lean/Substitute.lean

Method: 10.5281/zenodo.21769846.

What the four verdicts mean for a repair

no instance (395, 51.6%) is the honest negative: the proposition is there, synthesis was asked, and Lean has no constructive way to decide it. These are the sites where the classical dependence is doing real work.

not an instance position (340, 44.4%) is not a negative at all. Nothing was tested. Counting these as failures understates removability and counting them as successes overstates it, which is why they are their own category rather than folded into either.

needs choice anyway (18) is the sharpest case: an instance exists, and it depends on choice itself, so substituting it moves the dependence rather than removing it. Any measure that stops at whether an instance exists would score these as wins.

timed out (12) is unknown, not negative. It is small here, which is the improvement this run represents.

Why an earlier pass is not used

A previous run over the same question returned 404 synthesis timeouts against this run's 12, and had no not-a-goal category at all, so nearly every site it could not clean was recorded as a time limit being hit. It was measuring its own budget. Its numbers are not reproduced here.

Reading it with the Cleanable Table

Together the two tables give the shape of the problem rather than a single rate. Removal succeeded where a decidable proposition sat in an instance position and the constructive instance existed. Where any of those three fails it fails for a different reason, and only one of the three is about mathematics.