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

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

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

open

Hole h_k3rest of erdos-1094--h3--h1--h1 (split by 20261014T112100Z-t1014-z-partial.lean).

$\displaystyle \exists K_2\ \forall n,k\in\mathbb{N}:\quad K_2<k,\ \ 2k\le n<k^2,\ \ 2\mid k,\ \ 3\nmid k,\ \ k \bmod 3 \le n \bmod 3 \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 $3$ is at least that of $k$ (so $p=3$ itself gives no 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 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 : ∃ (K₂ : ℕ),
  ∀ (n k : ℕ),
    K₂ < k →
      (2 : ℕ) * k ≤ n →
        n < k * k →
          k % (2 : ℕ) = (0 : ℕ) →
            (0 : ℕ) < k % (3 : ℕ) → k % (3 : ℕ) ≤ n % (3 : ℕ) → ∃ (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 this hole by 20261014T175700Z-t1014-q-partial.lean (merged in 3201a830fa89, attestation 000525).

h_p5to13 → erdos-1094--h3--h1--h1--h2--h1 (open)
$\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$

Read the partial proof (Lean)

theorem erdos_1094__h3__h1__h1__h2 : ∃ (K₂ : ℕ),
  ∀ (n k : ℕ),
    K₂ < k →
      (2 : ℕ) * k ≤ n →
        n < k * k →
          k % (2 : ℕ) = (0 : ℕ) →
            (0 : ℕ) < k % (3 : ℕ) → k % (3 : ℕ) ≤ n % (3 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ p ≤ k ∧ n % p < k % p := by
  have h_p5to13 : ∃ 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
  obtain ⟨K₃, h₃⟩ := h_p5to13
  refine ⟨max K₃ 13, fun n k hk h2k hnk hk2 hk3 hk3n => ?_⟩
  have hK₃ : K₃ < k := lt_of_le_of_lt (le_max_left _ _) hk
  have hk13 : 13 ≤ k := le_of_lt (lt_of_le_of_lt (le_max_right _ _) hk)
  by_cases h5 : n % 5 < k % 5
  · exact ⟨5, by norm_num, by omega, h5⟩
  by_cases h7 : n % 7 < k % 7
  · exact ⟨7, by norm_num, by omega, h7⟩
  by_cases h11 : n % 11 < k % 11
  · exact ⟨11, by norm_num, by omega, h11⟩
  by_cases h13 : n % 13 < k % 13
  · exact ⟨13, by norm_num, hk13, h13⟩
  exact h₃ n k hK₃ h2k hnk hk2 hk3 hk3n (Nat.le_of_not_lt h5) (Nat.le_of_not_lt h7)
    (Nat.le_of_not_lt h11) (Nat.le_of_not_lt h13)

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/attempts/20261014T175700Z-t1014-q-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».Context

open scoped Nat

/-! Hole `h_k3rest` 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 : ∃ (K₂ : ℕ),
  ∀ (n k : ℕ),
    K₂ < k →
      (2 : ℕ) * k ≤ n →
        n < k * k →
          k % (2 : ℕ) = (0 : ℕ) →
            (0 : ℕ) < k % (3 : ℕ) → k % (3 : ℕ) ≤ n % (3 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ p ≤ k ∧ n % p < k % p := by
  sorry

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

Rendered from gloss/968857a022b3….md · Improve these words →

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

Depends on (1), each in words

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

erdos-1094--h3--h1--h1--h2--h1: $\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$

Attestation: none of a proof

No proof of this statement has been merged. A partial assembly merged under attestations/000525.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/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 (1)

1 recorded. Routes refuted: none. Failure classes: none.

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 t1014-q; merged in 3201a830fa89 under attestations/000525.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/attempts/20261014T175700Z-t1014-q-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 20261014T175700Z-t1014-q-partial.lean, extracted by the gate at 15d1d4647b94 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.

h_p5to13 hole ∃ (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 hole
Leaves ∃ (K₂ : ℕ), ∀ (n k : ℕ), K₂ < k → (2 : ℕ) * k ≤ n → n < k * k → k % (2 : ℕ) = (0 : ℕ) → (0 : ℕ) < k % (3 : ℕ) → k % (3 : ℕ) ≤ n % (3 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ p ≤ k ∧ n % p < k % p, with h_p5to13 : ∃ (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.
Uses library Nat.Prime.
Left open as a hole; its statement is erdos-1094--h3--h1--h1--h2--h1 (open).
Lean, lines 16–18
```
  have h_p5to13 : ∃ 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
```
targets/erdos-1094/nodes/erdos-1094--h3--h1--h1--h2/attempts/20261014T175700Z-t1014-q-partial.lean, lines 16–18 at 6ba7fea98468 ↗
s2 obtain ∃ (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
Leaves ∃ (K₂ : ℕ), ∀ (n k : ℕ), K₂ < k → (2 : ℕ) * k ≤ n → n < k * k → k % (2 : ℕ) = (0 : ℕ) → (0 : ℕ) < k % (3 : ℕ) → k % (3 : ℕ) ≤ n % (3 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ p ≤ k ∧ n % p < k % p, with K₃ : ℕ, h₃ : ∀ (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.
Lean, line 19
```
  obtain ⟨K₃, h₃⟩ := h_p5to13
```
targets/erdos-1094/nodes/erdos-1094--h3--h1--h1--h2/attempts/20261014T175700Z-t1014-q-partial.lean, line 19 at 6ba7fea98468 ↗
hK3 have K₃ < k
Leaves ∃ (p : ℕ), Nat.Prime p ∧ p ≤ k ∧ n % p < k % p, with hK₃ : K₃ < k.
Uses library lt_of_le_of_lt, le_max_left.
Lean, line 21
```
  have hK₃ : K₃ < k := lt_of_le_of_lt (le_max_left _ _) hk
```
targets/erdos-1094/nodes/erdos-1094--h3--h1--h1--h2/attempts/20261014T175700Z-t1014-q-partial.lean, line 21 at 6ba7fea98468 ↗
hk13 have (13 : ℕ) ≤ k
Leaves ∃ (p : ℕ), Nat.Prime p ∧ p ≤ k ∧ n % p < k % p, with hk13 : (13 : ℕ) ≤ k.
Uses library le_of_lt, lt_of_le_of_lt, le_max_right.
Lean, line 22
```
  have hk13 : 13 ≤ k := le_of_lt (lt_of_le_of_lt (le_max_right _ _) hk)
```
targets/erdos-1094/nodes/erdos-1094--h3--h1--h1--h2/attempts/20261014T175700Z-t1014-q-partial.lean, line 22 at 6ba7fea98468 ↗
s5 case
Leaves ∃ (p : ℕ), Nat.Prime p ∧ p ≤ k ∧ n % p < k % p, with h5 : n % (5 : ℕ) < k % (5 : ℕ).
Uses library Exists.intro.
Lean, line 24
```
  · exact ⟨5, by norm_num, by omega, h5⟩
```
targets/erdos-1094/nodes/erdos-1094--h3--h1--h1--h2/attempts/20261014T175700Z-t1014-q-partial.lean, line 24 at 6ba7fea98468 ↗
s6 case
Leaves ∃ (p : ℕ), Nat.Prime p ∧ p ≤ k ∧ n % p < k % p, with h7 : n % (7 : ℕ) < k % (7 : ℕ).
Uses library Exists.intro.
Lean, line 26
```
  · exact ⟨7, by norm_num, by omega, h7⟩
```
targets/erdos-1094/nodes/erdos-1094--h3--h1--h1--h2/attempts/20261014T175700Z-t1014-q-partial.lean, line 26 at 6ba7fea98468 ↗
s7 case
Leaves ∃ (p : ℕ), Nat.Prime p ∧ p ≤ k ∧ n % p < k % p, with h11 : n % (11 : ℕ) < k % (11 : ℕ).
Uses library Exists.intro.
Lean, line 28
```
  · exact ⟨11, by norm_num, by omega, h11⟩
```
targets/erdos-1094/nodes/erdos-1094--h3--h1--h1--h2/attempts/20261014T175700Z-t1014-q-partial.lean, line 28 at 6ba7fea98468 ↗
s8 case
Leaves ∃ (p : ℕ), Nat.Prime p ∧ p ≤ k ∧ n % p < k % p, with h13 : n % (13 : ℕ) < k % (13 : ℕ).
Uses library Exists.intro.
Lean, line 30
```
  · exact ⟨13, by norm_num, hk13, h13⟩
```
targets/erdos-1094/nodes/erdos-1094--h3--h1--h1--h2/attempts/20261014T175700Z-t1014-q-partial.lean, line 30 at 6ba7fea98468 ↗
close term ∃ (p : ℕ), Nat.Prime p ∧ p ≤ k ∧ n % p < k % p
Closes the goal.
Uses library Nat.le_of_not_lt.
Lean, lines 31–32
```
  exact h₃ n k hK₃ h2k hnk hk2 hk3 hk3n (Nat.le_of_not_lt h5) (Nat.le_of_not_lt h7)
    (Nat.le_of_not_lt h11) (Nat.le_of_not_lt h13)
```
targets/erdos-1094/nodes/erdos-1094--h3--h1--h1--h2/attempts/20261014T175700Z-t1014-q-partial.lean, lines 31–32 at 6ba7fea98468 ↗

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

open scoped Nat

/-! Hole `h_k3rest` 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 : ∃ (K₂ : ℕ),
  ∀ (n k : ℕ),
    K₂ < k →
      (2 : ℕ) * k ≤ n →
        n < k * k →
          k % (2 : ℕ) = (0 : ℕ) →
            (0 : ℕ) < k % (3 : ℕ) → k % (3 : ℕ) ≤ n % (3 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ p ≤ k ∧ n % p < k % p := by
  have h_p5to13 : ∃ 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
  obtain ⟨K₃, h₃⟩ := h_p5to13
  refine ⟨max K₃ 13, fun n k hk h2k hnk hk2 hk3 hk3n => ?_⟩
  have hK₃ : K₃ < k := lt_of_le_of_lt (le_max_left _ _) hk
  have hk13 : 13 ≤ k := le_of_lt (lt_of_le_of_lt (le_max_right _ _) hk)
  by_cases h5 : n % 5 < k % 5
  · exact ⟨5, by norm_num, by omega, h5⟩
  by_cases h7 : n % 7 < k % 7
  · exact ⟨7, by norm_num, by omega, h7⟩
  by_cases h11 : n % 11 < k % 11
  · exact ⟨11, by norm_num, by omega, h11⟩
  by_cases h13 : n % 13 < k % 13
  · exact ⟨13, by norm_num, hk13, h13⟩
  exact h₃ n k hK₃ h2k hnk hk2 hk3 hk3n (Nat.le_of_not_lt h5) (Nat.le_of_not_lt h7)
    (Nat.le_of_not_lt h11) (Nat.le_of_not_lt h13)

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 →