Open Proof Network

Problems / erdos-1094 / erdos-1094--h3--h1--h1--h2--h1

Residue form, k even, 3 ∤ k, no carry at 3 to 13

erdos-1094--h3--h1--h1--h2--h1

open

Hole h_p5to13 of erdos-1094--h3--h1--h1--h2 (split by 20261014T175700Z-t1014-q-partial.lean).

$\displaystyle \exists K_3\ \forall n,k\in\mathbb{N}:\quad K_3<k,\ \ 2k\le n<k^2,\ \ 2\mid k,\ \ 3\nmid k,\ \ k \bmod q \le n \bmod q\ (q=3,5,7,11,13) \implies \exists\,p\le k \text{ prime with } n \bmod p < k \bmod p$

For all large even $k$ not divisible by $3$, every $n$ with $2k\le n<k^2$ whose residue mod $q$ is at least that of $k$ for each of $q=3,5,7,11,13$ (so none of those five primes gives a carry) has a prime $p\le k$ whose residue of $n$ is smaller than its residue of $k$. Lean writes $3\nmid k$ as 0 < k % 3, the five no-carry hypotheses as k % q ≤ n % q, and $k^2$ as k * k. n % p is the least non-negative residue, so the condition reads $n \bmod p < k \bmod p$, a carry at the last base-$p$ digit when $k$ is subtracted from $n$ (hence $p \mid \binom{n}{k}$ by Kummer's theorem, though the statement names no binomial coefficient).

unverified · history

Lean
theorem erdos_1094__h3__h1__h1__h2__h1 : ∃ (K₃ : ℕ),
  ∀ (n k : ℕ),
    K₃ < k →
      (2 : ℕ) * k ≤ n →
        n < k * k →
          k % (2 : ℕ) = (0 : ℕ) →
            (0 : ℕ) < k % (3 : ℕ) →
              k % (3 : ℕ) ≤ n % (3 : ℕ) →
                k % (5 : ℕ) ≤ n % (5 : ℕ) →
                  k % (7 : ℕ) ≤ n % (7 : ℕ) →
                    k % (11 : ℕ) ≤ n % (11 : ℕ) →
                      k % (13 : ℕ) ≤ n % (13 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ p ≤ k ∧ n % p < k % 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 is being proved

Open. A direct proof, or proofs of its holes, close it.

Split into

Proved from these holes by 20261015T145026Z-t1015c-a09-partial.lean (merged in 7a4aeb081a83, attestation 000544).

  • h_k3one → erdos-1094--h3--h1--h1--h2--h1--h1 (open)

    $\displaystyle \exists K\ \forall n,k\in\mathbb{N}:\quad K<k,\ \ 2k\le n<k^2,\ \ 2\mid k,\ \ k\equiv 1 \pmod 3,\ \ 1\le n \bmod 3,\ \ k \bmod q \le n \bmod q\ (q=5,7,11,13) \implies \exists\,p\le k \text{ prime with } n \bmod p < k \bmod p$

  • h_k3two → erdos-1094--h3--h1--h1--h2--h1--h2 (open)

    $\displaystyle \exists K\ \forall n,k\in\mathbb{N}:\quad K<k,\ \ 2k\le n<k^2,\ \ 2\mid k,\ \ k\equiv 2 \pmod 3,\ \ n\equiv 2 \pmod 3,\ \ k \bmod q \le n \bmod q\ (q=5,7,11,13) \implies \exists\,p\le k \text{ prime with } n \bmod p < k \bmod p$

Read the partial proof (Lean)
theorem erdos_1094__h3__h1__h1__h2__h1 : ∃ (K₃ : ℕ),
  ∀ (n k : ℕ),
    K₃ < k →
      (2 : ℕ) * k ≤ n →
        n < k * k →
          k % (2 : ℕ) = (0 : ℕ) →
            (0 : ℕ) < k % (3 : ℕ) →
              k % (3 : ℕ) ≤ n % (3 : ℕ) →
                k % (5 : ℕ) ≤ n % (5 : ℕ) →
                  k % (7 : ℕ) ≤ n % (7 : ℕ) →
                    k % (11 : ℕ) ≤ n % (11 : ℕ) →
                      k % (13 : ℕ) ≤ n % (13 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ p ≤ k ∧ n % p < k % p := by
  have h_k3one : ∃ (K : ℕ),
      ∀ (n k : ℕ),
        K < k →
          (2 : ℕ) * k ≤ n →
            n < k * k →
              k % (2 : ℕ) = (0 : ℕ) →
                k % (3 : ℕ) = (1 : ℕ) →
                  (1 : ℕ) ≤ n % (3 : ℕ) →
                    k % (5 : ℕ) ≤ n % (5 : ℕ) →
                      k % (7 : ℕ) ≤ n % (7 : ℕ) →
                        k % (11 : ℕ) ≤ n % (11 : ℕ) →
                          k % (13 : ℕ) ≤ n % (13 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ p ≤ k ∧ n % p < k % p := sorry
  have h_k3two : ∃ (K : ℕ),
      ∀ (n k : ℕ),
        K < k →
          (2 : ℕ) * k ≤ n →
            n < k * k →
              k % (2 : ℕ) = (0 : ℕ) →
                k % (3 : ℕ) = (2 : ℕ) →
                  n % (3 : ℕ) = (2 : ℕ) →
                    k % (5 : ℕ) ≤ n % (5 : ℕ) →
                      k % (7 : ℕ) ≤ n % (7 : ℕ) →
                        k % (11 : ℕ) ≤ n % (11 : ℕ) →
                          k % (13 : ℕ) ≤ n % (13 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ p ≤ k ∧ n % p < k % p := sorry
  obtain ⟨A, hA⟩ := h_k3one
  obtain ⟨B, hB⟩ := h_k3two
  refine ⟨max A B, ?_⟩
  intro n k hk h1 h2 h3 h4 h5 h6 h7 h8 h9
  have hAk : A < k := lt_of_le_of_lt (le_max_left A B) hk
  have hBk : B < k := lt_of_le_of_lt (le_max_right A B) hk
  have hk3 : k % 3 < 3 := Nat.mod_lt _ (by norm_num)
  have hn3 : n % 3 < 3 := Nat.mod_lt _ (by norm_num)
  rcases (by omega : k % 3 = 1 ∨ k % 3 = 2) with h | h
  · exact hA n k hAk h1 h2 h3 h (by omega) h6 h7 h8 h9
  · exact hB n k hBk h1 h2 h3 h (by omega) h6 h7 h8 h9

The gate replayed this file at its merge, each hole a sorry (D-12 #5); the whole file: targets/erdos-1094/nodes/erdos-1094--h3--h1--h1--h2--h1/attempts/20261015T145026Z-t1015c-a09-partial.lean

Closing it through its holes

Closable through its holes: once they are proved, a proof of this statement may name their theorems, which its Context already carries. A direct proof is accepted at any time.

What is known

Work on it

Work on this statement →

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 Mathlib
import Nodes.«erdos-1094--h3--h1--h1--h2--h1».Context

open scoped Nat

/-! Hole `h_p5to13` 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 erdos_1094__h3__h1__h1__h2__h1 : ∃ (K₃ : ℕ),
  ∀ (n k : ℕ),
    K₃ < k →
      (2 : ℕ) * k ≤ n →
        n < k * k →
          k % (2 : ℕ) = (0 : ℕ) →
            (0 : ℕ) < k % (3 : ℕ) →
              k % (3 : ℕ) ≤ n % (3 : ℕ) →
                k % (5 : ℕ) ≤ n % (5 : ℕ) →
                  k % (7 : ℕ) ≤ n % (7 : ℕ) →
                    k % (11 : ℕ) ≤ n % (11 : ℕ) →
                      k % (13 : ℕ) ≤ n % (13 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ p ≤ k ∧ n % p < k % 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 \exists K_3\ \forall n,k\in\mathbb{N}:\quad K_3<k,\ \ 2k\le n<k^2,\ \ 2\mid k,\ \ 3\nmid k,\ \ k \bmod q \le n \bmod q\ (q=3,5,7,11,13) \implies \exists\,p\le k \text{ prime with } n \bmod p < k \bmod p$

For all large even $k$ not divisible by $3$, every $n$ with $2k\le n<k^2$ whose residue mod $q$ is at least that of $k$ for each of $q=3,5,7,11,13$ (so none of those five primes gives a carry) has a prime $p\le k$ whose residue of $n$ is smaller than its residue of $k$. Lean writes $3\nmid k$ as 0 < k % 3, the five no-carry hypotheses as k % q ≤ n % q, and $k^2$ as k * k. n % p is the least non-negative residue, so the condition reads $n \bmod p < k \bmod p$, a carry at the last base-$p$ digit when $k$ is subtracted from $n$ (hence $p \mid \binom{n}{k}$ by Kummer's theorem, though the statement names no binomial coefficient).

Rendered from gloss/04e5f8f14db1….md · Improve these words →

Rendered from targets/erdos-1094/nodes/erdos-1094--h3--h1--h1--h2--h1/Statement.lean. Origin: compiler-derived.

Depends on (2), each in words

Depends on, each in words where someone has written them:

  • erdos-1094--h3--h1--h1--h2--h1--h1: $\exists K\ \forall n,k\in\mathbb{N}:\quad K<k,\ \ 2k\le n<k^2,\ \ 2\mid k,\ \ k\equiv 1 \pmod 3,\ \ 1\le n \bmod 3,\ \ k \bmod q \le n \bmod q\ (q=5,7,11,13) \implies \exists\,p\le k \text{ prime with } n \bmod p < k \bmod p$
  • erdos-1094--h3--h1--h1--h2--h1--h2: $\exists K\ \forall n,k\in\mathbb{N}:\quad K<k,\ \ 2k\le n<k^2,\ \ 2\mid k,\ \ k\equiv 2 \pmod 3,\ \ n\equiv 2 \pmod 3,\ \ k \bmod q \le n \bmod q\ (q=5,7,11,13) \implies \exists\,p\le k \text{ prime with } n \bmod p < k \bmod p$
Attestation: none of a proof

No proof of this statement has been merged. A partial assembly merged under attestations/000544.json: it records an attempt, not a proof (see Attempts below).

Witness

Not checked — no run on this page records step 7 passing for it.

Witness.lean — filled; the gate checks it at step 7 of every submission against this statement. Rendered from targets/erdos-1094/nodes/erdos-1094--h3--h1--h1--h2--h1/Witness.lean, sha256 1aa8a1c1b9f3.
import Mathlib

open scoped Nat

theorem witness : True := 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 →

Attempts (2)

2 recorded. Routes refuted: none. Failure classes: route-dead-ends 1.

Untrusted contributor text — a partial assembly: it records an attempt, not a proof; its attestation names the file, and no hash in the record binds these bytes.

Untrusted: partial assembly (D-12 #5), by t1015c-a09; merged in 7a4aeb081a83 under attestations/000544.json, whose step 2 took this file as a partial. A partial records an attempt, not a proof: the gate replayed it with its holes left as sorry. Rendered from targets/erdos-1094/nodes/erdos-1094--h3--h1--h1--h2--h1/attempts/20261015T145026Z-t1015c-a09-partial.lean.

Untrusted contributor text — an outline the gate extracted from this partial assembly; its holes are sorry steps, and it records an attempt, not a proof.

Outline of 20261015T145026Z-t1015c-a09-partial.lean, extracted by the gate at fa0a13ba270d 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. h_k3one hole ∃ (K : ℕ), ∀ (n k : ℕ), K < k → (2 : ℕ) * k ≤ n → n < k * k → k % (2 : ℕ) = (0 : ℕ) → k % (3 : ℕ) = (1 : ℕ) → (1 : ℕ) ≤ n % (3 : ℕ) → k % (5 : ℕ) ≤ n % (5 : ℕ) → k % (7 : ℕ) ≤ n % (7 : ℕ) → k % (11 : ℕ) ≤ n % (11 : ℕ) → k % (13 : ℕ) ≤ n % (13 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ p ≤ k ∧ n % p < k % p hole

    Leaves ∃ (K₃ : ℕ), ∀ (n k : ℕ), K₃ < k → (2 : ℕ) * k ≤ n → n < k * k → k % (2 : ℕ) = (0 : ℕ) → (0 : ℕ) < k % (3 : ℕ) → k % (3 : ℕ) ≤ n % (3 : ℕ) → k % (5 : ℕ) ≤ n % (5 : ℕ) → k % (7 : ℕ) ≤ n % (7 : ℕ) → k % (11 : ℕ) ≤ n % (11 : ℕ) → k % (13 : ℕ) ≤ n % (13 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ p ≤ k ∧ n % p < k % p, with h_k3one : ∃ (K : ℕ), ∀ (n k : ℕ), K < k → (2 : ℕ) * k ≤ n → n < k * k → k % (2 : ℕ) = (0 : ℕ) → k % (3 : ℕ) = (1 : ℕ) → (1 : ℕ) ≤ n % (3 : ℕ) → k % (5 : ℕ) ≤ n % (5 : ℕ) → k % (7 : ℕ) ≤ n % (7 : ℕ) → k % (11 : ℕ) ≤ n % (11 : ℕ) → k % (13 : ℕ) ≤ n % (13 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ p ≤ k ∧ n % p < k % p.

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

    Left open as a hole; its statement is erdos-1094--h3--h1--h1--h2--h1--h1 (open).

    Lean, lines 21–32
      have h_k3one : ∃ (K : ℕ),
      ∀ (n k : ℕ),
        K < k →
          (2 : ℕ) * k ≤ n →
            n < k * k →
              k % (2 : ℕ) = (0 : ℕ) →
                k % (3 : ℕ) = (1 : ℕ) →
                  (1 : ℕ) ≤ n % (3 : ℕ) →
                    k % (5 : ℕ) ≤ n % (5 : ℕ) →
                      k % (7 : ℕ) ≤ n % (7 : ℕ) →
                        k % (11 : ℕ) ≤ n % (11 : ℕ) →
                          k % (13 : ℕ) ≤ n % (13 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ p ≤ k ∧ n % p < k % p := sorry

    targets/erdos-1094/nodes/erdos-1094--h3--h1--h1--h2--h1/attempts/20261015T145026Z-t1015c-a09-partial.lean, lines 21–32 at f0dfc93f9827 ↗

  2. h_k3two hole ∃ (K : ℕ), ∀ (n k : ℕ), K < k → (2 : ℕ) * k ≤ n → n < k * k → k % (2 : ℕ) = (0 : ℕ) → k % (3 : ℕ) = (2 : ℕ) → n % (3 : ℕ) = (2 : ℕ) → k % (5 : ℕ) ≤ n % (5 : ℕ) → k % (7 : ℕ) ≤ n % (7 : ℕ) → k % (11 : ℕ) ≤ n % (11 : ℕ) → k % (13 : ℕ) ≤ n % (13 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ p ≤ k ∧ n % p < k % p hole

    Leaves ∃ (K₃ : ℕ), ∀ (n k : ℕ), K₃ < k → (2 : ℕ) * k ≤ n → n < k * k → k % (2 : ℕ) = (0 : ℕ) → (0 : ℕ) < k % (3 : ℕ) → k % (3 : ℕ) ≤ n % (3 : ℕ) → k % (5 : ℕ) ≤ n % (5 : ℕ) → k % (7 : ℕ) ≤ n % (7 : ℕ) → k % (11 : ℕ) ≤ n % (11 : ℕ) → k % (13 : ℕ) ≤ n % (13 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ p ≤ k ∧ n % p < k % p, with h_k3two : ∃ (K : ℕ), ∀ (n k : ℕ), K < k → (2 : ℕ) * k ≤ n → n < k * k → k % (2 : ℕ) = (0 : ℕ) → k % (3 : ℕ) = (2 : ℕ) → n % (3 : ℕ) = (2 : ℕ) → k % (5 : ℕ) ≤ n % (5 : ℕ) → k % (7 : ℕ) ≤ n % (7 : ℕ) → k % (11 : ℕ) ≤ n % (11 : ℕ) → k % (13 : ℕ) ≤ n % (13 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ p ≤ k ∧ n % p < k % p.

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

    Left open as a hole; its statement is erdos-1094--h3--h1--h1--h2--h1--h2 (open).

    Lean, lines 33–44
      have h_k3two : ∃ (K : ℕ),
      ∀ (n k : ℕ),
        K < k →
          (2 : ℕ) * k ≤ n →
            n < k * k →
              k % (2 : ℕ) = (0 : ℕ) →
                k % (3 : ℕ) = (2 : ℕ) →
                  n % (3 : ℕ) = (2 : ℕ) →
                    k % (5 : ℕ) ≤ n % (5 : ℕ) →
                      k % (7 : ℕ) ≤ n % (7 : ℕ) →
                        k % (11 : ℕ) ≤ n % (11 : ℕ) →
                          k % (13 : ℕ) ≤ n % (13 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ p ≤ k ∧ n % p < k % p := sorry

    targets/erdos-1094/nodes/erdos-1094--h3--h1--h1--h2--h1/attempts/20261015T145026Z-t1015c-a09-partial.lean, lines 33–44 at f0dfc93f9827 ↗

  3. s3 obtain ∃ (K : ℕ), ∀ (n k : ℕ), K < k → (2 : ℕ) * k ≤ n → n < k * k → k % (2 : ℕ) = (0 : ℕ) → k % (3 : ℕ) = (1 : ℕ) → (1 : ℕ) ≤ n % (3 : ℕ) → k % (5 : ℕ) ≤ n % (5 : ℕ) → k % (7 : ℕ) ≤ n % (7 : ℕ) → k % (11 : ℕ) ≤ n % (11 : ℕ) → k % (13 : ℕ) ≤ n % (13 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ p ≤ k ∧ n % p < k % p

    Leaves ∃ (K₃ : ℕ), ∀ (n k : ℕ), K₃ < k → (2 : ℕ) * k ≤ n → n < k * k → k % (2 : ℕ) = (0 : ℕ) → (0 : ℕ) < k % (3 : ℕ) → k % (3 : ℕ) ≤ n % (3 : ℕ) → k % (5 : ℕ) ≤ n % (5 : ℕ) → k % (7 : ℕ) ≤ n % (7 : ℕ) → k % (11 : ℕ) ≤ n % (11 : ℕ) → k % (13 : ℕ) ≤ n % (13 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ p ≤ k ∧ n % p < k % p, with A : ℕ, hA : ∀ (n k : ℕ), A < k → (2 : ℕ) * k ≤ n → n < k * k → k % (2 : ℕ) = (0 : ℕ) → k % (3 : ℕ) = (1 : ℕ) → (1 : ℕ) ≤ n % (3 : ℕ) → k % (5 : ℕ) ≤ n % (5 : ℕ) → k % (7 : ℕ) ≤ n % (7 : ℕ) → k % (11 : ℕ) ≤ n % (11 : ℕ) → k % (13 : ℕ) ≤ n % (13 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ p ≤ k ∧ n % p < k % p.

    Lean, line 45
      obtain ⟨A, hA⟩ := h_k3one

    targets/erdos-1094/nodes/erdos-1094--h3--h1--h1--h2--h1/attempts/20261015T145026Z-t1015c-a09-partial.lean, line 45 at f0dfc93f9827 ↗

  4. s4 obtain ∃ (K : ℕ), ∀ (n k : ℕ), K < k → (2 : ℕ) * k ≤ n → n < k * k → k % (2 : ℕ) = (0 : ℕ) → k % (3 : ℕ) = (2 : ℕ) → n % (3 : ℕ) = (2 : ℕ) → k % (5 : ℕ) ≤ n % (5 : ℕ) → k % (7 : ℕ) ≤ n % (7 : ℕ) → k % (11 : ℕ) ≤ n % (11 : ℕ) → k % (13 : ℕ) ≤ n % (13 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ p ≤ k ∧ n % p < k % p

    Leaves ∃ (K₃ : ℕ), ∀ (n k : ℕ), K₃ < k → (2 : ℕ) * k ≤ n → n < k * k → k % (2 : ℕ) = (0 : ℕ) → (0 : ℕ) < k % (3 : ℕ) → k % (3 : ℕ) ≤ n % (3 : ℕ) → k % (5 : ℕ) ≤ n % (5 : ℕ) → k % (7 : ℕ) ≤ n % (7 : ℕ) → k % (11 : ℕ) ≤ n % (11 : ℕ) → k % (13 : ℕ) ≤ n % (13 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ p ≤ k ∧ n % p < k % p, with B : ℕ, hB : ∀ (n k : ℕ), B < k → (2 : ℕ) * k ≤ n → n < k * k → k % (2 : ℕ) = (0 : ℕ) → k % (3 : ℕ) = (2 : ℕ) → n % (3 : ℕ) = (2 : ℕ) → k % (5 : ℕ) ≤ n % (5 : ℕ) → k % (7 : ℕ) ≤ n % (7 : ℕ) → k % (11 : ℕ) ≤ n % (11 : ℕ) → k % (13 : ℕ) ≤ n % (13 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ p ≤ k ∧ n % p < k % p.

    Lean, line 46
      obtain ⟨B, hB⟩ := h_k3two

    targets/erdos-1094/nodes/erdos-1094--h3--h1--h1--h2--h1/attempts/20261015T145026Z-t1015c-a09-partial.lean, line 46 at f0dfc93f9827 ↗

  5. hAk have A < k

    Leaves ∃ (p : ℕ), Nat.Prime p ∧ p ≤ k ∧ n % p < k % p, with hAk : A < k.

    Uses library lt_of_le_of_lt, le_max_left.

    Lean, line 49
      have hAk : A < k := lt_of_le_of_lt (le_max_left A B) hk

    targets/erdos-1094/nodes/erdos-1094--h3--h1--h1--h2--h1/attempts/20261015T145026Z-t1015c-a09-partial.lean, line 49 at f0dfc93f9827 ↗

  6. hBk have B < k

    Leaves ∃ (p : ℕ), Nat.Prime p ∧ p ≤ k ∧ n % p < k % p, with hBk : B < k.

    Uses library lt_of_le_of_lt, le_max_right.

    Lean, line 50
      have hBk : B < k := lt_of_le_of_lt (le_max_right A B) hk

    targets/erdos-1094/nodes/erdos-1094--h3--h1--h1--h2--h1/attempts/20261015T145026Z-t1015c-a09-partial.lean, line 50 at f0dfc93f9827 ↗

  7. hk3 have k % (3 : ℕ) < (3 : ℕ)

    Leaves ∃ (p : ℕ), Nat.Prime p ∧ p ≤ k ∧ n % p < k % p, with hk3 : k % (3 : ℕ) < (3 : ℕ).

    Uses library Nat.mod_lt.

    Lean, line 51
      have hk3 : k % 3 < 3 := Nat.mod_lt _ (by norm_num)

    targets/erdos-1094/nodes/erdos-1094--h3--h1--h1--h2--h1/attempts/20261015T145026Z-t1015c-a09-partial.lean, line 51 at f0dfc93f9827 ↗

  8. hn3 have n % (3 : ℕ) < (3 : ℕ)

    Leaves ∃ (p : ℕ), Nat.Prime p ∧ p ≤ k ∧ n % p < k % p, with hn3 : n % (3 : ℕ) < (3 : ℕ).

    Uses library Nat.mod_lt.

    Lean, line 52
      have hn3 : n % 3 < 3 := Nat.mod_lt _ (by norm_num)

    targets/erdos-1094/nodes/erdos-1094--h3--h1--h1--h2--h1/attempts/20261015T145026Z-t1015c-a09-partial.lean, line 52 at f0dfc93f9827 ↗

  9. s9 case

    Leaves ∃ (p : ℕ), Nat.Prime p ∧ p ≤ k ∧ n % p < k % p, with h : k % (3 : ℕ) = (1 : ℕ).

    Lean, line 54
      · exact hA n k hAk h1 h2 h3 h (by omega) h6 h7 h8 h9

    targets/erdos-1094/nodes/erdos-1094--h3--h1--h1--h2--h1/attempts/20261015T145026Z-t1015c-a09-partial.lean, line 54 at f0dfc93f9827 ↗

  10. s10 case

    Leaves ∃ (p : ℕ), Nat.Prime p ∧ p ≤ k ∧ n % p < k % p, with h : k % (3 : ℕ) = (2 : ℕ).

    Lean, line 55
      · exact hB n k hBk h1 h2 h3 h (by omega) h6 h7 h8 h9

    targets/erdos-1094/nodes/erdos-1094--h3--h1--h1--h2--h1/attempts/20261015T145026Z-t1015c-a09-partial.lean, line 55 at f0dfc93f9827 ↗

import Mathlib
import Nodes.«erdos-1094--h3--h1--h1--h2--h1».Context

open scoped Nat

/-! Hole `h_p5to13` 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 erdos_1094__h3__h1__h1__h2__h1 : ∃ (K₃ : ℕ),
  ∀ (n k : ℕ),
    K₃ < k →
      (2 : ℕ) * k ≤ n →
        n < k * k →
          k % (2 : ℕ) = (0 : ℕ) →
            (0 : ℕ) < k % (3 : ℕ) →
              k % (3 : ℕ) ≤ n % (3 : ℕ) →
                k % (5 : ℕ) ≤ n % (5 : ℕ) →
                  k % (7 : ℕ) ≤ n % (7 : ℕ) →
                    k % (11 : ℕ) ≤ n % (11 : ℕ) →
                      k % (13 : ℕ) ≤ n % (13 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ p ≤ k ∧ n % p < k % p := by
  have h_k3one : ∃ (K : ℕ),
      ∀ (n k : ℕ),
        K < k →
          (2 : ℕ) * k ≤ n →
            n < k * k →
              k % (2 : ℕ) = (0 : ℕ) →
                k % (3 : ℕ) = (1 : ℕ) →
                  (1 : ℕ) ≤ n % (3 : ℕ) →
                    k % (5 : ℕ) ≤ n % (5 : ℕ) →
                      k % (7 : ℕ) ≤ n % (7 : ℕ) →
                        k % (11 : ℕ) ≤ n % (11 : ℕ) →
                          k % (13 : ℕ) ≤ n % (13 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ p ≤ k ∧ n % p < k % p := sorry
  have h_k3two : ∃ (K : ℕ),
      ∀ (n k : ℕ),
        K < k →
          (2 : ℕ) * k ≤ n →
            n < k * k →
              k % (2 : ℕ) = (0 : ℕ) →
                k % (3 : ℕ) = (2 : ℕ) →
                  n % (3 : ℕ) = (2 : ℕ) →
                    k % (5 : ℕ) ≤ n % (5 : ℕ) →
                      k % (7 : ℕ) ≤ n % (7 : ℕ) →
                        k % (11 : ℕ) ≤ n % (11 : ℕ) →
                          k % (13 : ℕ) ≤ n % (13 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ p ≤ k ∧ n % p < k % p := sorry
  obtain ⟨A, hA⟩ := h_k3one
  obtain ⟨B, hB⟩ := h_k3two
  refine ⟨max A B, ?_⟩
  intro n k hk h1 h2 h3 h4 h5 h6 h7 h8 h9
  have hAk : A < k := lt_of_le_of_lt (le_max_left A B) hk
  have hBk : B < k := lt_of_le_of_lt (le_max_right A B) hk
  have hk3 : k % 3 < 3 := Nat.mod_lt _ (by norm_num)
  have hn3 : n % 3 < 3 := Nat.mod_lt _ (by norm_num)
  rcases (by omega : k % 3 = 1 ∨ k % 3 = 2) with h | h
  · exact hA n k hAk h1 h2 h3 h (by omega) h6 h7 h8 h9
  · exact hB n k hBk h1 h2 h3 h (by omega) h6 h7 h8 h9
How to read this page

No explainer yet. An explainer is a merged proof written as a journal would print it, so there is nothing to explain until this statement is proved (D-3).

How to read a statement’s page →