Proof 1 of 1
Proof 1 · root · submitter not recorded, merged in 6452ef80d4f1.
The statement
Statement not audited — fidelity mechanical-only; no statement-QA record for this problem.
theorem OpnProp.and_swap : ∀ p q : Prop, p ∧ q → q ∧ p := by sorry
A statement is written := by sorry: the sorry holds the place of a proof, because a statement file only says what is claimed. A proof the gate checked is its own file, Proof.lean. How to read a proof page →
No informal statement is recorded for this problem yet (D-6 intake, F11).
No gloss yet: no one has written in words what this statement says (D-3 v3.30); the Lean above is the statement. How to write one →
Fidelity: statement unchecked Nobody other than its author has yet judged whether the Lean says what the conjecture says. The kernel cannot decide this; a person must. protocol: fidelity: mechanical-only . Rendered from targets/tutorial/nodes/tutorial-and-swap/Statement.lean.
The proof, dependencies first
1 statement on this proof. Each statement comes before the statements whose proofs use it. A step’s outline is folded; open it for its goal, what it uses and its Lean lines. How to read a proof page →
tutorial-and-swap proved
Statement not audited — fidelity mechanical-only; no statement-QA record for this problem.
theorem OpnProp.and_swap : ∀ p q : Prop, p ∧ q → q ∧ p := by sorry
A statement is written
:= by sorry: thesorryholds the place of a proof, because a statement file only says what is claimed. A proof the gate checked is its own file,Proof.lean. How to read a proof page →No informal statement is recorded for this problem yet (D-6 intake, F11).
No gloss yet: no one has written in words what this statement says (D-3 v3.30); the Lean above is the statement. How to write one →
Checked by the kernel — an outline of the proof attested in attestations/000002.json, merge commit
6452ef80d4f1.Outline of
Proof.lean, extracted by the gate at82834c4684b8from the proof’s elaboration: each step is a claim the proof establishes and the goal it leaves. Open a step for what it uses and its Lean lines.Proof: targets/tutorial/nodes/tutorial-and-swap/Proof.lean, lines 1–5 at
6452ef80d4f1.No explainer yet. This proof written as a journal would print it, labelled unverified, is the next thing a writer could add, by pull request (D-3, D-36; the guide shows how).
Correspondence
Checked by the kernel — each row’s declaration, file, lines and attestation are the attested record; the explainer column says only whether unverified prose exists and who signed it.
| Statement | Declaration | Proof file and lines | Attestation | Explainer |
|---|---|---|---|---|
| tutorial-and-swap | OpnProp.and_swap | targets/tutorial/nodes/tutorial-and-swap/Proof.lean, lines 1–5 at 6452ef80d4f1 | attestations/000002.json | none yet |