Problems / euclid-primes / variant-2a7919a9--h1
Each entry of a list is at most its sum
variant-2a7919a9--h1
proved
Hole bound of variant-2a7919a9 (split by 20260919T185907Z-euclid-list-61d1ea-partial.lean).
$\displaystyle \forall\, l\in\operatorname{List}(\mathbb{N}),\ \forall x\in l:\quad x\le \sum l$
Every element of a list of natural numbers is at most the sum of the list (List.sum, the empty list summing to $0$). There are no other hypotheses.
Lean
theorem variant_2a7919a9__h1 : ∀ (l : List ℕ), ∀ x ∈ l, x ≤ l.sum := 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, 000121, records the gate’s run.
The proof step by step (outline)
Checked by the kernel — an outline of the attested proof below: attestations/000121.json, merge commit c7d8b0b11c55.
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/000121.json, merge commit c7d8b0b11c55.
artifact_hash of the attestation below, so these are the bytes the gate checked. Rendered from targets/euclid-primes/nodes/variant-2a7919a9--h1/Proof.lean, sha256 14e19f969509.import Defs.IsPrime import Mathlib.Tactic /-! Hole `bound` of a merged partial proof, as a node (D-12 #5, D-29). Statement generated by the gate from the assembly; immutable (D-3). -/ theorem variant_2a7919a9__h1 : ∀ (l : List ℕ), ∀ x ∈ l, x ≤ l.sum := by intro l x hx exact List.single_le_sum (fun _ _ => Nat.zero_le _) x hx
What is known
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 its words (1 version)
Statement not audited — only a problem’s root statement is audited for fidelity (D-9); the kernel checks a proof against this Lean as written.
import Defs.IsPrime import Mathlib.Tactic /-! Hole `bound` of a merged partial proof, as a node (D-12 #5, D-29). Statement generated by the gate from the assembly; immutable (D-3). -/ theorem variant_2a7919a9__h1 : ∀ (l : List ℕ), ∀ x ∈ l, x ≤ l.sum := 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 →
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\, l\in\operatorname{List}(\mathbb{N}),\ \forall x\in l:\quad x\le \sum l$
Every element of a list of natural numbers is at most the sum of the list (List.sum, the empty list summing to $0$). There are no other hypotheses.
Rendered from gloss/bbe0a6087fbb….md · Improve these words →
Rendered from targets/euclid-primes/nodes/variant-2a7919a9--h1/Statement.lean. Origin: skeleton-hole.
Attestation: pass, 7 of 7 checks
Checked by the kernel — the gate’s record of the run: attestations/000121.json, merge commit c7d8b0b11c55.
Verdict pass, from attestations/000121.json.
- Submitter
euclid-list-61d1ea- Toolchain
- leanprover/lean4:v4.33.1 (hash
f54d0bc916bf76a7fae460ce9d078ccd1f74aeb4fd12c4b6546bca28b6aa1c63) - Mathlib
- 0df444a360eaa60ab8c11dca51a86af692955474
- Reviewer
- thisisanameforsure
| Step | Check | Result |
|---|---|---|
| 1 | toolchain | pass |
| 2 | paths | pass |
| 4 | kernel-replay | pass |
| 5 | axioms | pass |
| 6 | hazards | pass |
| 7 | witness | pass |
| 8 | deps | pass |
Witness
Checked by the kernel — step 7 passed in the run its attestation records: attestations/000121.json, merge commit c7d8b0b11c55.
014fbacc5707.import Defs.IsPrime import Mathlib.Tactic theorem witness : ∃ (l : List ℕ) (x : ℕ), x ∈ l := ⟨[0], 0, by simp⟩
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 →