Peer Proof Review¶
Review process — instantiates Contradiction-Closure Proof
A human referee scrutinizes a finished indirect proof for scope drift, hidden premises, and circularity, and records whether a direct or constructive proof would serve better.
Peer Proof Review is the human judgement applied to a proof someone else has already written. It does not derive, tabulate, or mechanize anything; a competent reviewer reads a completed contradiction-closure argument and asks the questions the author was too close to ask — does the conclusion match the scope of what was actually shown? Is the logic the proof assumes appropriate to the context that will consume it? Did a quantifier silently widen between the supposition and the closure? Is the argument secretly circular, leaning on the very claim it means to prove? Its distinctive contributions are two things no formal derivation supplies on its own: a judgement about fit — whether classical indirect closure is even the right currency here, or whether a reader who needed a construction has been short-changed — and a durable written verdict others can rely on. It is the mechanism of last resort against proofs that are locally valid but globally wrong for their purpose.
Example¶
A referee receives a submitted proof that a certain packing of spheres is the densest possible — established indirectly, by showing any denser packing forces an impossible local configuration. The reviewer does not re-derive the geometry line by line; instead she interrogates fit. Scope: does "densest" mean among all packings or only lattice packings? The proof quietly assumes the latter in one lemma but the theorem claims the former — a scope gap. Logic: the indirect step is classically fine, but a portion of the field wanted an explicit optimal packing, not a proof that no denser one can exist. Circularity: one inequality turns out to assume a bound that follows only from the theorem. She writes these up as a review, and adds a note that a constructive treatment of the flagged lemma would settle the doubt.
The review's product is not a new proof but a verdict with reasons — the scope gap named, the constructive alternative recommended, the concerns recorded so an editor and later readers inherit them rather than rediscovering them. The historical shadow behind such reviews is real: some famous indirect proofs have needed years of scrutiny before acceptance.[1]
How it works¶
- Read for fit, not steps. The reviewer checks the proof against its intended use — scope, logic, and whether the claim proved is the claim needed — rather than re-executing every inference.
- Hunt the classic indirect-proof failures. Scope drift, hidden premises, circular dependence on the target, and mis-matched logic are the specific defects the review targets.
- Judge the constructive question. Decide and record whether a direct or constructive proof would serve the audience better than the indirect one, even when the indirect proof is valid.
- Record a verdict. Produce a durable written review — concerns, scope caveats, recommendation — that later readers and gatekeepers inherit.
Tuning parameters¶
- Scrutiny depth — a fit-and-scope pass versus a full step-by-step re-derivation. Deeper review catches more but costs scarce expert time and may still miss what a machine would catch.
- Reviewer independence — one referee versus several blind to each other. More reviewers reduce shared blind spots but slow the verdict.
- Constructivity bar — how strongly the review pushes for a direct/constructive proof. A high bar suits contexts needing witnesses; a low bar accepts classical closure freely.
- Verdict granularity — a binary accept/reject versus a detailed conditions-for-acceptance record. Detail helps revision but takes longer to write.
When it helps, and when it misleads¶
Its strength is catching what formal rigor cannot see: a mechanically valid proof can still answer the wrong question or overreach its scope, and only a judgement about purpose flags that. It is also where the archetype's "would a direct or constructive proof be preferable?" caveat gets actually decided, and where the audit trail becomes a shared, durable record.
Its failure mode is that human review is fallible and social: a plausible, elegantly written indirect proof can pass reviewers who trusted its polish, and a subtle scope shift or a deep circular dependency can survive several careful readings — reviewer authority can even suppress a correct doubt. The guarding discipline is to pair human review with a mechanical check for anything load-bearing, to keep reviews independent, and to treat "the referees accepted it" as strong evidence, not proof.
How it implements the components¶
Peer Proof Review realizes the judgement-and-record side of the archetype:
scope_and_logic_boundary— the review's central check: does the conclusion stay within the scope shown, and is the assumed logic right for the consuming context?constructive_alternative_note— the reviewer records whether a direct or constructive proof would serve better than the indirect one.proof_audit_record— the written review is the durable verdict, with concerns and caveats, that later readers and gatekeepers inherit.
The review scrutinizes a finished proof but does not itself build the derivation or auto-mark where classical axioms were used (derivation_path, logic_exception_marker) — that is Proof Assistant Script; review supplies the human judgement the machine cannot.
Related¶
- Instantiates: Contradiction-Closure Proof — supplies the fit-and-scope judgement and durable verdict the archetype's tradeoffs demand.
- Consumes: Assumption Ledger — the dependency record the reviewer reads to check for hidden premises and circularity.
- Sibling mechanisms: Reductio Proof Template · Natural Deduction Proof Tree · Assumption Ledger · Contradiction Search Checklist · Minimal Unsat Core Analysis · Case-Split Elimination Table · Proof Assistant Script · Unsatisfiability Certificate
Editorial Notes¶
Form Classification¶
Form family: Assessment, Review & Assurance
Rationale: Peer Proof Review operates as a bounded evaluation of existing evidence or work that produces a finding or disposition because it a human referee scrutinizes a finished indirect proof for scope drift, hidden premises, and circularity, and records whether a direct or constructive proof would serve better.
Independent corroboration: The frozen evidence defines Peer Proof Review as 'A human referee scrutinizes a finished indirect proof for scope drift, hidden premises, and circularity, and records whether a direct or constructive proof would serve better', so its operative form is Assessment, Review & Assurance.
Review outcome: Independent reviewer agreement; high confidence.
Origin Attribution¶
Primary origin: Mathematics
Origin pattern: Cross-disciplinary synthesis
Present-day reach: Specialized
Rationale: Peer Proof Review is rooted in mathematics: Mathematical proof culture developed referee scrutiny of premises, scope, circularity, and constructive alternatives.
Related originating lineages:
- Computer Science & Software Engineering — Computer science and software engineering materially shaped Peer Proof Review through algorithms, software architecture, security, and distributed systems.
Review resolution: Both blind reviewers agree that mathematics is the primary origin. Reconciliation resolves alternate_origin_disagreement. Formative alternate lineages are retained as computer_science; later breadth of use is recorded separately as domain_reach=specialized, while origin_mode=cross_disciplinary_synthesis describes the relationship among origin lineages.
Encyclopedia synthesis: The exact catalogued form synthesizes established practice rather than reproducing a single standard historical label.
Review outcome: Reconciled after independent review; high confidence.
References¶
[1] Hales, T. C. "Formal Proof". Notices of the American Mathematical Society 55(11), 1370–1380 (2008). Documents that the computer-assisted Kepler proof remained under referee scrutiny for years before it was accepted for publication. registry ↩