Problems / tutorial / tutorial-and-swap
tutorial-and-swap
proved
The tutorial statement.
The tutorial node: permanently open and off the ledger (D-27).
theorem OpnProp.and_swap : ∀ p q : Prop, p ∧ q → q ∧ p := by sorry
Why does it end in 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 →
How it was proved
Proved by Proof.lean, checked by the kernel. Its attestation, 000002, records the gate’s run.
The proof step by step (outline)
Checked by the kernel — an outline of the attested proof below: attestations/000002.json, merge commit 6452ef80d4f1.
Outline of Proof.lean, extracted by the gate at 82834c4684b8 from 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.
The proof in Lean (Proof.lean)
Checked by the kernel — these bytes are the ones its attestation names: attestations/000002.json, merge commit 6452ef80d4f1.
artifact_hash of the attestation below, so these are the bytes the gate checked. Rendered from targets/tutorial/nodes/tutorial-and-swap/Proof.lean, sha256 721b98ef9704./-! The tutorial node (D-27): permanently open, off-ledger. Lean core only. -/ theorem OpnProp.and_swap : ∀ p q : Prop, p ∧ q → q ∧ p := by intro p q h exact ⟨h.2, h.1⟩
Work on it
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).
How to contribute → · Pull requests in flight ↗ · See it in the problem’s graph →
Record
Statement: the Lean file and no words yet
Statement not audited — fidelity mechanical-only; no statement-QA record for this problem.
/-! The tutorial node (D-27): permanently open, off-ledger. Lean core only. -/ 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 →
Rendered from targets/tutorial/nodes/tutorial-and-swap/Statement.lean. Origin: authored.
Attestation: pass, 4 of 4 checks
Checked by the kernel — the gate’s record of the run: attestations/000002.json, merge commit 6452ef80d4f1.
Verdict pass, from attestations/000002.json.
- Submitter
- not recorded
- Toolchain
- leanprover/lean4:v4.33.1 (hash
f54d0bc916bf76a7fae460ce9d078ccd1f74aeb4fd12c4b6546bca28b6aa1c63) - Mathlib
- none (Lean core only)
- Reviewer
- none needed (tutorial)
| Step | Check | Result |
|---|---|---|
| 1 | toolchain | pass |
| 2 | paths | pass |
| 4 | kernel-replay | pass |
| 5 | axioms | pass |
Witness
Not checked — no run on this page records step 7 passing for it.
c63ac3e8af7d./-! Non-vacuity witness (D-4 step 7; F01-R3): the hypothesis `p ∧ q` is satisfiable. -/ theorem witness : ∃ p q : Prop, p ∧ q := ⟨True, True, trivial, trivial⟩
No gloss yet: no one has written in words what this witness says (D-3 v3.30); the Lean above is the witness. How to write one →