The field surrounding a proof

Suppose a theorem has two proofs. One is short and efficient to verify. The other introduces a construction useful for a nearby problem. The first may be preferable for certification, while discarding the second may damage further inquiry. The two tasks value different information.

Proof-Path Theory makes this distinction explicit. A proof certificate is a selected derivation of a target from admitted premises. The surrounding proof field is a larger typed collection of claims, justifications, evidence, and alternatives. A recorded counterexample is not promoted into a proof step. A conjectured transition is not treated as certified because it appears beside a theorem. Status and scope belong to the record.[3]

The finite model uses justification hypergraphs because ordinary arrows can hide an important distinction. A step may require both \(A\) and \(B\) to obtain \(L\). Another conclusion may have two independent routes, either of which is sufficient. The former is a conjunction of premises. The latter is an alternative between justifications. A faithful record must preserve which kind of dependency is present.

For example, take certified steps \(\{A,B\}\Rightarrow L\) and \(L\Rightarrow T\). They form one certificate for the target \(T\). A second route might use \(A\Rightarrow M\) and \(\{M,B\}\Rightarrow T\). A candidate extension from \(M\) to a new target \(U\) can remain visible without becoming part of either certificate. It may be valuable precisely because it suggests what to investigate next, but its value does not make it valid.

Permalink · Source line 278

The final proof is a useful compression. It removes material unnecessary for establishing the endpoint. But sufficiency for endpoint verification does not imply sufficiency for teaching, semantic audit, or further discovery. This is the same factorization issue encountered earlier: a retained record may answer one family of questions while merging distinctions another family needs.[3]

A later task may require a discarded construction. Recovery may mean rereading a source, rerunning a computation, or repeating a search. When future tasks and their weights are specified, retention can be compared with this expected reconstruction cost. The comparison is relative to that model, not a universal measure of mathematical importance.

This suggests selective preservation rather than indiscriminate accumulation. Keep the example that explains a necessary hypothesis. Keep the obstruction that rules out a broad family of approaches. Keep a reusable comparison map and the test that caught an important translation error. A thousand nearly identical failed calculations may be less useful than one concise account of the reason they fail.

Revision also changes the record. Strengthening a lemma's hypothesis can affect every later argument that uses it. Those descendants need review, but are not automatically false. Some may already satisfy the stronger hypothesis. Others may have alternate proofs. A dependency record identifies where to look, allowing correction to propagate without treating the entire development as either untouched or destroyed.[3]

The proof field is a declared mathematical record, not a recovery of every thought that produced a theorem. Its selection and provenance should remain visible. Dependencies extracted from Lean describe the artifact, but cannot reconstruct unrecorded experiments or every choice preceding it.[3]

Review has a similar dependence problem. Two assessments can share the same mistaken definition or the same unexamined example. Agreement then provides less new information than agreement between genuinely different checks. Proof-Path Theory studies explicit models of such dependence. Their methodological lesson is to ask what a review adds, not to infer the motives or competence of particular reviewers from a model.[3]

A mathematical archive becomes powerful when it can answer both “why does this follow?” and “what can we do next?” The certificate addresses the first question. The richer field can help with the second. Preserving both is especially consequential when the next researcher is not the same person, or not the same kind of reasoner.

Permalink · Source line 294