6 The discipline of checking
On this page · Permalink · Source line 240
The phrase “the proof was checked” leaves an important question open. Was the argument reviewed, a calculation reproduced, a formal derivation accepted, or a software package tested? Each check has a particular scope. Their relationship needs to be established.
Lean gives a particularly strong form of deductive checking. Its kernel checks a proof of a formal statement relative to the definitions, theorems, and axioms in the environment. Lean's own validation guidance distinguishes this question from the meaning of the theorem statement, and describes additional checks for axiom dependencies and stored proof artifacts.[7]
The formal declaration is the proposition established, not a label attached to a prose claim. Its quantifiers, domains, coercions, and hypotheses must match the intended mathematics. A theorem about a fixed finite model does not cover every model. Assuming an extension exists does not construct it. These distinctions determine what the proof actually gives us.
Formalization makes these distinctions productive. Writing the statement can expose an ambiguity. Supplying an actual map can reveal where an argument relied on resemblance. A proof obligation that remains open can isolate the missing theorem more precisely than confident prose.
Acceptance is not the whole policy
On this page · Permalink · Source line 250
Axioms require a separate audit. Lean permits new axioms and records proof dependencies. Postulating \(\mathrm{False}\) allows any proposition to be derived. The derivation is valid relative to that assumption. A project that disallows the assumption must reject the dependency.[8]
A useful audit therefore follows dependencies transitively. Looking only for a placeholder in the final theorem can miss one in an imported lemma. The commonly admitted mathematical basis in Lean includes propext, Classical.choice, and Quot.sound. A result using only an allowed subset has passed an axiom-policy check, not an automatic test of every intended application.[8], [9]
Ordinary hypotheses are different from global axioms. The implication \(\mathrm{False}\Rightarrow P\) needs no newly postulated axiom, yet cannot establish \(P\) without the impossible premise. Less conspicuous hypotheses can conceal the same application gap. The review must therefore inspect the theorem's quantifiers and show that the required data are available where the result is used. A legitimate conditional theorem need not supply every application itself. Its conditional scope must remain visible.
The project record offers a concrete illustration. The verification section of Proof-Path Theory describes deliberately invalid equalities, witnesses, and conjunction models, as well as a proof placeholder. It also describes an explicit false axiom whose consequence Lean accepts, while a separate project policy rejects the dependency. The report distinguishes replay through Lean's own kernel from an independent implementation, and identifies the reused external dependency cache. These are scoped records, not a blanket claim that every page of the research program has received the same check.[3]
A negative control should fail for the intended reason. If a false equality is never checked because the file cannot import its dependencies, the test has not demonstrated mathematical rejection. A timeout is similarly inconclusive. This makes diagnostics part of the evidence. The useful record says which proposition or witness was rejected, by which check, and under what environment.
The principle extends beyond Lean. A certificate checker should reject corrupted witnesses. A manifest validator should detect altered files. A parser should reject malformed records rather than assign reassuring defaults. These tests address distinct ways a claim can become disconnected from its evidence.
Reproduction binds the claim to an artifact
On this page · Permalink · Source line 264
A proof lives in a source tree, a toolchain, and an imported environment. The Lean community's verification guidance therefore asks whether the project builds, whether the relevant theorem file is actually included, which axioms it uses, and whether its statement expresses the advertised claim. A source listing that looks plausible is not a completed verification record.[9]
Pinned dependencies, source digests, build commands, and preserved logs make this record recoverable. A digest identifies bytes. It does not prove that the bytes contain correct mathematics. A successful replay checks a particular artifact under a particular environment. Repeating the same kernel check can demonstrate reproducibility, but does not turn that kernel into an independent checker. An alternate proof or independently implemented validator may challenge a different class of failure.
Semantic review belongs alongside mechanical checks. Compare the formal theorem with the prose claim. Instantiate its hypotheses on meaningful examples. Map the manuscript result to the declarations establishing it, rather than relying on suggestive names. The aim is not paperwork, but an inspectable relationship between a claim and its evidence.
More tests help when they cover new failure modes. Repetition does not remove a shared mistaken definition. Conversely, a short proof checked under a clearly stated basis can deserve strong confidence. Precise qualification should sharpen that confidence, not turn established results into perpetual uncertainty.
Verification thus changes discovery by making statements precise and exposing missing interfaces. It tells the next inquiry what has survived. The certificate records that achievement, while the surrounding path may still carry useful mathematics.