Open Proof Network

Problems / euclid-primes / variant-2a7919a9--h2

A prime beyond the sum of a list

variant-2a7919a9--h2

proved

Hole euclid of variant-2a7919a9 (split by 20260919T185907Z-euclid-list-61d1ea-partial.lean).

$\displaystyle \forall\, l\in\operatorname{List}(\mathbb{N}):\quad \bigl(\forall x\in l,\ x\le \textstyle\sum l\bigr)\ \Rightarrow\ \exists p\in\mathbb{N},\ \textstyle\sum l<p\ \wedge\ p\ \text{prime}$

For every list of natural numbers, under the inherited hypothesis that each of its entries is at most its sum (the earlier hole's claim), there is a prime strictly greater than the sum of the list (List.sum). Prime is the problem's own Opn.IsPrime: $2\le p$ and every $d$ with $p=d\cdot c$ for some natural $c$ is $1$ or $p$.

unverified · history

Lean
theorem variant_2a7919a9__h2 : ∀ (l : List ℕ), (∀ x ∈ l, x ≤ l.sum) → ∃ p, l.sum < p ∧ Opn.IsPrime 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, 000122, records the gate’s run.

The proof step by step (outline)

Checked by the kernel — an outline of the attested proof below: attestations/000122.json, merge commit 8c31571316de.

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.

  1. f1 have (l.sum + (1 : ℕ)).factorial + (1 : ℕ) ≠ (1 : ℕ)

    Leaves ∃ (p : ℕ), l.sum < p ∧ Opn.IsPrime p, with f1 : (l.sum + (1 : ℕ)).factorial + (1 : ℕ) ≠ (1 : ℕ).

    Uses library Nat.factorial Nat.factorial n is the factorial of n. .

    Lean, lines 9–11
      have f1 : Nat.factorial (l.sum + 1) + 1 ≠ 1 := by
    have := Nat.factorial_pos (l.sum + 1)
    omega

    targets/euclid-primes/nodes/variant-2a7919a9--h2/Proof.lean, lines 9–11 at 8c31571316de ↗

    1. f1.this have (0 : ℕ) < (l.sum + (1 : ℕ)).factorial

      Leaves (l.sum + (1 : ℕ)).factorial + (1 : ℕ) ≠ (1 : ℕ), with this : (0 : ℕ) < (l.sum + (1 : ℕ)).factorial.

      Uses library Nat.factorial_pos.

      Lean, line 10
          have := Nat.factorial_pos (l.sum + 1)

      targets/euclid-primes/nodes/variant-2a7919a9--h2/Proof.lean, line 10 at 8c31571316de ↗

  2. pp have Nat.Prime ((l.sum + (1 : ℕ)).factorial + (1 : ℕ)).minFac

    Leaves ∃ (p : ℕ), l.sum < p ∧ Opn.IsPrime p, with pp : Nat.Prime ((l.sum + (1 : ℕ)).factorial + (1 : ℕ)).minFac.

    Uses library Nat.Prime Nat.Prime p means that p is a prime number, that is, a natural number at least 2 whose only divisors are p and 1. , Nat.minFac Returns the smallest prime factor of n ≠ 1. , Nat.factorial Nat.factorial n is the factorial of n. , Nat.minFac_prime.

    Lean, line 12
      have pp : Nat.Prime (Nat.minFac (Nat.factorial (l.sum + 1) + 1)) := Nat.minFac_prime f1

    targets/euclid-primes/nodes/variant-2a7919a9--h2/Proof.lean, line 12 at 8c31571316de ↗

  3. s3 case

    Leaves l.sum < ((l.sum + (1 : ℕ)).factorial + (1 : ℕ)).minFac.

    Lean, lines 14–19
      · by_contra h
    have h₁ : Nat.minFac (Nat.factorial (l.sum + 1) + 1) ∣ Nat.factorial (l.sum + 1) :=
      Nat.dvd_factorial (Nat.minFac_pos _) (by omega)
    have h₂ : Nat.minFac (Nat.factorial (l.sum + 1) + 1) ∣ 1 :=
      (Nat.dvd_add_iff_right h₁).2 (Nat.minFac_dvd _)
    exact pp.not_dvd_one h₂

    targets/euclid-primes/nodes/variant-2a7919a9--h2/Proof.lean, lines 14–19 at 8c31571316de ↗

    1. s3.h1 have ((l.sum + (1 : ℕ)).factorial + (1 : ℕ)).minFac ∣ (l.sum + (1 : ℕ)).factorial

      Leaves False, with h₁ : ((l.sum + (1 : ℕ)).factorial + (1 : ℕ)).minFac ∣ (l.sum + (1 : ℕ)).factorial.

      Uses library Nat.minFac Returns the smallest prime factor of n ≠ 1. , Nat.factorial Nat.factorial n is the factorial of n. , Nat.dvd_factorial, Nat.minFac_pos.

      Lean, lines 15–16
          have h₁ : Nat.minFac (Nat.factorial (l.sum + 1) + 1) ∣ Nat.factorial (l.sum + 1) :=
      Nat.dvd_factorial (Nat.minFac_pos _) (by omega)

      targets/euclid-primes/nodes/variant-2a7919a9--h2/Proof.lean, lines 15–16 at 8c31571316de ↗

    2. s3.h2 have ((l.sum + (1 : ℕ)).factorial + (1 : ℕ)).minFac ∣ (1 : ℕ)

      Leaves False, with h₂ : ((l.sum + (1 : ℕ)).factorial + (1 : ℕ)).minFac ∣ (1 : ℕ).

      Uses library Nat.minFac Returns the smallest prime factor of n ≠ 1. , Nat.factorial Nat.factorial n is the factorial of n. , Nat.dvd_add_iff_right, Nat.minFac_dvd.

      Lean, lines 17–18
          have h₂ : Nat.minFac (Nat.factorial (l.sum + 1) + 1) ∣ 1 :=
      (Nat.dvd_add_iff_right h₁).2 (Nat.minFac_dvd _)

      targets/euclid-primes/nodes/variant-2a7919a9--h2/Proof.lean, lines 17–18 at 8c31571316de ↗

  4. s4 case

    Leaves ∀ (d : ℕ), Opn.Divides d ((l.sum + (1 : ℕ)).factorial + (1 : ℕ)).minFac → d = (1 : ℕ) ∨ d = ((l.sum + (1 : ℕ)).factorial + (1 : ℕ)).minFac.

    Uses library Nat.dvd_prime, Exists.intro Existential introduction. .

    Lean, lines 20–22
      · intro d hd
    obtain ⟨c, hc⟩ := hd
    exact (Nat.dvd_prime pp).mp ⟨c, hc⟩

    targets/euclid-primes/nodes/variant-2a7919a9--h2/Proof.lean, lines 20–22 at 8c31571316de ↗

    1. s4.s1 obtain Opn.Divides d ((l.sum + (1 : ℕ)).factorial + (1 : ℕ)).minFac

      Leaves d = (1 : ℕ) ∨ d = ((l.sum + (1 : ℕ)).factorial + (1 : ℕ)).minFac, with c : ℕ, hc : ((l.sum + (1 : ℕ)).factorial + (1 : ℕ)).minFac = d * c.

      Lean, line 21
          obtain ⟨c, hc⟩ := hd

      targets/euclid-primes/nodes/variant-2a7919a9--h2/Proof.lean, line 21 at 8c31571316de ↗

The proof in Lean (Proof.lean)

Checked by the kernel — these bytes are the ones its attestation names: attestations/000122.json, merge commit 8c31571316de.

Proof.lean — its sha256 is the artifact_hash of the attestation below, so these are the bytes the gate checked. Rendered from targets/euclid-primes/nodes/variant-2a7919a9--h2/Proof.lean, sha256 881da5c60117.
import Defs.IsPrime
import Mathlib.Tactic

/-! Hole `euclid` 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__h2 : ∀ (l : List ℕ), (∀ x ∈ l, x ≤ l.sum) → ∃ p, l.sum < p ∧ Opn.IsPrime p := by
  intro l _
  have f1 : Nat.factorial (l.sum + 1) + 1 ≠ 1 := by
    have := Nat.factorial_pos (l.sum + 1)
    omega
  have pp : Nat.Prime (Nat.minFac (Nat.factorial (l.sum + 1) + 1)) := Nat.minFac_prime f1
  refine ⟨Nat.minFac (Nat.factorial (l.sum + 1) + 1), ?_, pp.two_le, ?_⟩
  · by_contra h
    have h₁ : Nat.minFac (Nat.factorial (l.sum + 1) + 1) ∣ Nat.factorial (l.sum + 1) :=
      Nat.dvd_factorial (Nat.minFac_pos _) (by omega)
    have h₂ : Nat.minFac (Nat.factorial (l.sum + 1) + 1) ∣ 1 :=
      (Nat.dvd_add_iff_right h₁).2 (Nat.minFac_dvd _)
    exact pp.not_dvd_one h₂
  · intro d hd
    obtain ⟨c, hc⟩ := hd
    exact (Nat.dvd_prime pp).mp ⟨c, hc⟩

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).

Write the explainer →

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 `euclid` 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__h2 : ∀ (l : List ℕ), (∀ x ∈ l, x ≤ l.sum) → ∃ p, l.sum < p ∧ Opn.IsPrime 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 →

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}):\quad \bigl(\forall x\in l,\ x\le \textstyle\sum l\bigr)\ \Rightarrow\ \exists p\in\mathbb{N},\ \textstyle\sum l<p\ \wedge\ p\ \text{prime}$

For every list of natural numbers, under the inherited hypothesis that each of its entries is at most its sum (the earlier hole's claim), there is a prime strictly greater than the sum of the list (List.sum). Prime is the problem's own Opn.IsPrime: $2\le p$ and every $d$ with $p=d\cdot c$ for some natural $c$ is $1$ or $p$.

Rendered from gloss/29263b509ece….md · Improve these words →

Rendered from targets/euclid-primes/nodes/variant-2a7919a9--h2/Statement.lean. Origin: skeleton-hole.

Attestation: pass, 7 of 7 checks

Checked by the kernel — the gate’s record of the run: attestations/000122.json, merge commit 8c31571316de.

Verdict pass, from attestations/000122.json.

Submitter
euclid-list-61d1ea
Toolchain
leanprover/lean4:v4.33.1 (hash f54d0bc916bf76a7fae460ce9d078ccd1f74aeb4fd12c4b6546bca28b6aa1c63)
Mathlib
0df444a360eaa60ab8c11dca51a86af692955474
Reviewer
thisisanameforsure
StepCheckResult
1toolchainpass
2pathspass
4kernel-replaypass
5axiomspass
6hazardspass
7witnesspass
8depspass
Witness

Checked by the kernel — step 7 passed in the run its attestation records: attestations/000122.json, merge commit 8c31571316de.

Witness.lean — checked at step 7 of the run recorded below: pass. Rendered from targets/euclid-primes/nodes/variant-2a7919a9--h2/Witness.lean, sha256 96b9f1f38834.
import Defs.IsPrime
import Mathlib.Tactic

theorem witness : ∃ (l : List ℕ), ∀ x ∈ l, x ≤ l.sum := ⟨[], 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 →

How to read this page

How to read a statement’s page →