Does free proof checking actually reduce verification burden?

The source's central claim is that making proof checking free does not reduce the verification burden on mathematical knowledge. It moves that burden onto layers machines cannot perform, whose throughput is set by the number of qualified readers. The authors call the result "adjudication scarcity." The evidence is one corpus. OpenAI's 1 August 2026 release of ten results came with Lean 4 formalizations and no unproved steps. Across it, the kernel-checked proofs total 20.6 MB and the statements requiring human audit total 55.6 KB, a ratio of 379 to 1, and those statements introduce 218 bespoke definitions. Four weeks later, one result, a claimed counterexample to Connes's rigidity conjecture, remained in dispute.

The source's title marks the split it relies on: correct, in that a kernel verifies the derivation, but not understood, in that no one has established what the statement means. Three layers are distinguished. L1, derivational validity, is what a kernel checks; it is mechanizable and its cost is falling toward zero. L2, representational fidelity, asks whether the formal statement means the informal question; the source argues that no machine can settle this. L3, epistemic significance, is the referee's business and is not the paper's focus. The August corpus is verified at L1, but as far as the public record shows, no qualified specialist has read its 223-line statement and said what it means. The reason is a grounding regress inherited from Fetzer (1988). Checking a formal statement against its question requires a formal rendering of the question, and the same faithfulness problem reappears, so the regress ends in unaided human judgment. Mechanical checking also removes the incidental L2 check that line-by-line reading used to provide, so the L2 obligation is isolated rather than reduced.

The source extends the logic of What limits how much models can improve themselves? rather than contradicting it. That note treats verification as the resource limiting progress; this source says cheap verification moves the limit to a layer where verification stays expensive. Its warning about certificates also echoes Do reasoning traces actually cause correct answers?: a fluent artifact gets read as evidence of the function it appears to perform. Here a machine certificate risks being read as evidence of meaning when it only evidences derivation. The Connes episode shows the fallback the source expects, with some participants settling the question by asking language models.

The excerpt does not establish how general the pattern is. It rests on one laboratory's corpus and one dispute. The 379 to 1 ratio measures bytes, not audit hours. The claims that expert capacity is fixed and uncompensated, and that the per-claim audit cost does not fall, are argued rather than measured. The paper takes no position on whether the Connes construction is correct, and says its argument does not depend on the answer, which is the right scope. The excerpt also includes only the first category of the six-category mismatch taxonomy, and the paper's claims about software, cryptography and regulated systems are absent from it. The implication, at the strength the evidence allows, is a well-argued structural claim about where the bottleneck sits when derivation is cheap, illustrated by one case. It is not yet a measured law for other fields.