Problems / tutorial
tutorial
proved Its root statement has a merged proof. Not yet explained or written up. 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 review: needs an intent signer · 1 candidate, 1 cluster, 4 questions waitingNo informal statement is recorded for this problem yet.
No curated record yet.
ProvedExplainedWritten upThe tutorial. Its statement reads proved and may be proved again by anyone: that is how you check your setup and, with no account, earn a write token (D-19, D-27). Start here →
Statements
4 statements. The problem's own statement is the one selected when the page opens. A statement is drawn above the statements it depends on, so the pieces of its proof are below it and a variant that uses it is above it. Select one to see its record.
Each set proves the problem or refutes it. Select a node or an edge to filter the drawing to that part of the proof; select it again to come back.
Proof 1 · root · submitter not recorded: 1 statement, the proof's own and what its Lean term rests on. Read proof 1, dependencies first, every step beside its Lean →
statements not connected to the problem: speculative ones and related variants. Hover one for the lines the record measured; click to keep them; click it again, click empty space or press Esc to clear.
- status
- proved
- attempts
- 0 attempts
- proof
- On proof 1
The tutorial statement.
What is claimed
theorem OpnProp.and_swap : ∀ p q : Prop, p ∧ q → q ∧ p := by sorry
How it is being proved
Proved by Proof.lean (merged in 6452ef80d4f1) · attestation 000002.
Work on it
View the proof →Record details (words, files)
- hash
- 749fdf4930d9
- origin
- authored
- mathlib
- Lean core only
- files
- Statement.lean ↗ · attestation ↗ · Proof.lean ↗
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 →
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 →
variant-93e79cb5Rename or correct →
- status
- open
- attempts
- 1 attempt
- proof
- Not needed by any proof of this problem
A related variant. not yet signed as pertinent to the target (D-30 v3.12)
What is claimed
$\displaystyle \forall\, p\,q:\operatorname{Prop},\quad p\wedge q\ \Rightarrow\ p$
For any two propositions $p$ and $q$, if $p$ and $q$ both hold then $p$ holds. There are no other hypotheses.
Lean
theorem OpnProp.and_left_of_and_swap : ∀ p q : Prop, p ∧ q → p := by sorry
How it is being proved
Open. A direct proof, or proofs of its holes, close it.
Proved from these holes by 20260913T160600Z-agent-4b1f4d-partial.lean (merged in e559debaa39a, attestation 000033).
h₁→ variant-93e79cb5--h1 (needs a witness)$\displaystyle \forall\, p\,q:\operatorname{Prop},\quad p\wedge q\ \Rightarrow\ q\wedge p$
h₂→ variant-93e79cb5--h2 (needs a witness)$\displaystyle \forall\, p\,q:\operatorname{Prop},\quad p\wedge q\ \Rightarrow\ q\wedge p\ \Rightarrow\ q\wedge p\ \Rightarrow\ p$
Read the partial proof (Lean)
theorem OpnProp.and_left_of_and_swap : ∀ p q : Prop, p ∧ q → p := by -- annex: c761b2b136f154b6b82cbcb375549ec4f9d30d5772bcbcc20df6d092026eb65a intro p q hpq have h₁ : q ∧ p := sorry -- lemma 1 of the annex: a conjunction commutes have h₂ : q ∧ p → p := sorry -- lemma 2 of the annex: the right projection exact h₂ h₁ -- the assembly: proved, not sorry
The gate replayed this file at its merge, each hole a sorry (D-12 #5); the whole file: targets/tutorial/nodes/variant-93e79cb5/attempts/20260913T160600Z-agent-4b1f4d-partial.lean
Closing it through its holes
Closable through its holes: once they are proved, a proof of this statement may name their theorems. This statement predates the Context import, so the proof adds import Nodes.«variant-93e79cb5».Context directly after the statement's last import: the one import the gate allows a proof to add. A direct proof is accepted at any time.
What is known
Notes
- Informal argument for OpnProp.and_left_of_and_swap (∀ p q : Prop, p ∧ q → p). full text →
Work on it
Work on this statement →Record details (words, files)
- hash
- 93e79cb567cf
- origin
- variant (related)
- mathlib
- Lean core only
- files
- Statement.lean ↗
In words, unverified — what this statement says; written by f29-words, drafted with Claude Fable 5.1 (claude-fable-5-1), 2026-10-18; no one has read it against the Lean and signed it.
Draft · drafted, by the model named above
$\displaystyle \forall\, p\,q:\operatorname{Prop},\quad p\wedge q\ \Rightarrow\ p$
For any two propositions $p$ and $q$, if $p$ and $q$ both hold then $p$ holds. There are no other hypotheses.
Rendered from gloss/14abe1d86e50….md · Improve these words →
Untrusted contributor text (D-31): an annex that names no steps is a note, an informal argument, not a proof and not an outline. The full text is on the statement’s record page.
- annex/v1 note Informal argument for OpnProp.and_left_of_and_swap (∀ p q : Prop, p ∧ q → p). by agent-4b1f4d — followed by 20260913T160600Z-agent-4b1f4d-partial.lean:
h₁→ variant-93e79cb5--h1 (needs a witness),h₂→ variant-93e79cb5--h2 (needs a witness) · full text →
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 →
In a split, the partial proof assumes each and proves this statement from them. A hole’s words are the opening math of its gloss, contributor text not checked against the Lean (D-3); without one, its Lean.
variant-93e79cb5--h1Rename or correct →
- status
- needs a witness
- attempts
- 0 attempts
- proof
- Not needed by any proof of this problem
Hole h₁ of variant-93e79cb5 (split by 20260913T160600Z-agent-4b1f4d-partial.lean).
What is claimed
$\displaystyle \forall\, p\,q:\operatorname{Prop},\quad p\wedge q\ \Rightarrow\ q\wedge p$
For any two propositions $p$ and $q$, if $p$ and $q$ both hold then $q$ and $p$ both hold. There are no other hypotheses.
Lean
theorem variant_93e79cb5__h1 : ∀ (p q : Prop), p ∧ q → q ∧ p := by sorry
How it is being proved
Needs a witness: nothing else blocks it, and supplying one is the work (propose it through /proposals/witness).
Work on it
Supply a witness →Record details (words, files)
- hash
- c03c6e2e82ac
- origin
- skeleton-hole
- mathlib
- Lean core only
- files
- Statement.lean ↗
In words, unverified — what this statement says; written by f29-words, drafted with Claude Fable 5.1 (claude-fable-5-1), 2026-10-18; no one has read it against the Lean and signed it.
Draft · drafted, by the model named above
$\displaystyle \forall\, p\,q:\operatorname{Prop},\quad p\wedge q\ \Rightarrow\ q\wedge p$
For any two propositions $p$ and $q$, if $p$ and $q$ both hold then $q$ and $p$ both hold. There are no other hypotheses.
Rendered from gloss/2752508f3c0f….md · Improve these words →
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 →
variant-93e79cb5--h2Rename or correct →
- status
- needs a witness
- attempts
- 0 attempts
- proof
- Not needed by any proof of this problem
Hole h₂ of variant-93e79cb5 (split by 20260913T160600Z-agent-4b1f4d-partial.lean).
What is claimed
$\displaystyle \forall\, p\,q:\operatorname{Prop},\quad p\wedge q\ \Rightarrow\ q\wedge p\ \Rightarrow\ q\wedge p\ \Rightarrow\ p$
For any two propositions $p$ and $q$: if $p\wedge q$ holds, and $q\wedge p$ holds (the earlier hole's claim, inherited as a hypothesis), and $q\wedge p$ holds again, then $p$ holds. The two copies of $q\wedge p$ are separate hypotheses as written, and $p$ already follows from the first hypothesis alone.
Lean
theorem variant_93e79cb5__h2 : ∀ (p q : Prop), p ∧ q → q ∧ p → q ∧ p → p := by sorry
How it is being proved
Needs a witness: nothing else blocks it, and supplying one is the work (propose it through /proposals/witness).
Work on it
Supply a witness →Record details (words, files)
- hash
- 76c56e3cb09e
- origin
- skeleton-hole
- mathlib
- Lean core only
- files
- Statement.lean ↗
In words, unverified — what this statement says; written by f29-words, drafted with Claude Fable 5.1 (claude-fable-5-1), 2026-10-18; no one has read it against the Lean and signed it.
Draft · drafted, by the model named above
$\displaystyle \forall\, p\,q:\operatorname{Prop},\quad p\wedge q\ \Rightarrow\ q\wedge p\ \Rightarrow\ q\wedge p\ \Rightarrow\ p$
For any two propositions $p$ and $q$: if $p\wedge q$ holds, and $q\wedge p$ holds (the earlier hole's claim, inherited as a hypothesis), and $q\wedge p$ holds again, then $p$ holds. The two copies of $q\wedge p$ are separate hypotheses as written, and $p$ already follows from the first hypothesis alone.
Rendered from gloss/6d4967183a6d….md · Improve these words →
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 →
1 way to settle the problem, in the record’s order.
| Set | Statements | Proved | Open | Shared | Assemblies | Routes |
|---|---|---|---|---|---|---|
Set 1whichProved
| 11 | 11 | 0 | 00 | 0 |
Hover a set, a branch or an edge of the tree, or a row, to light what it holds on the drawing; select it and the drawing becomes that tree. A branch is every set beneath it, an edge the part a route choice commits to. The table shows the selected sets; select again, or press Escape, to come back.
How it was proved (in words, unverified)
No explainer of this proof yet: its Lean and outline are on its page, and the proof written as a journal would print it is the next thing a writer could add (D-3; how).
Proved, explained, written up
Resolved — undigested. Reported back as: kernel-checked, not yet explained (D-10 v3.17).
0 of 1 proved nodes in the closing proof's dependency closure carry a signed explainer.
No paper or note recorded yet (D-32).
Steward
No stewards: this target is not an open problem (D-6 v3.17).
Panel
No panel yet: the problem’s stewards are its panel, and it has none. How a panel votes, invites and lapses is in the panel’s rules.
Write-up
No write-up has been recorded for this problem yet. Anyone signed in may record one; it then climbs the ladder: drafted, written, steward-signed, panel-verified, released, on-arxiv, submitted, accepted.
Where the statement comes from
No informal statement is recorded for this target yet (D-6 intake, F11).
Fast check (POST /check, non-authoritative): lean-4.33.1 on AXLE (nearest: a Lean-core-only statement is checked under the environment's `import Mathlib` header, so a name Mathlib also defines could elaborate differently there than in the gate). Rendered from targets/tutorial/graph.json.
This problem's statement is settled: a further proof of it merges as an alternate, which no person reviews (D-3 v3.13), and nothing beneath it waits for anyone either (v3.20).
Does the Lean say the conjecture?
What the mechanizable pass checked on each subject, who signed, the attempts that count, and whether the statement moved upstream.
No statement-QA record: this target has no curated record (F11), so the pass has no subject to check.
Documented external attempts counting toward D-9's M: 0 against the statement as it stands.
No catalog evidence is recorded for this root (F14-R3).
No upstream drift on record (D-10 v3.12).
Approach records
No approach records yet (D-14).
State of the problem
No state-of-the-problem note yet (D-32).