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

Residue form, k and n odd

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

open

Hole h_odd of erdos-1094--h3--h1 (split by 20261009T125000Z-t1009-a-partial.lean).

$\displaystyle \exists K_2\ \forall n,k\in\mathbb{N}:\quad K_2<k,\ \ 2k\le n<k^2,\ \ k \text{ odd},\ \ n \text{ odd} \implies \exists\,p\le k \text{ prime with } n \bmod p < k \bmod p$

Lean writes $k^2$ as k * k, and "odd" as k % 2 = 1 and n % 2 = 1.
n % p is the least non-negative residue, so the condition reads $n \bmod p < k \bmod p$.
Nothing is said about even $k$, or about odd $k$ with even $n$.

By Kummer's theorem such a $p$ divides $\binom{n}{k}$, since subtracting $k$ from $n$ in base $p$ borrows at the last digit. The statement itself mentions no binomial coefficient.

unverified · history

Lean

theorem erdos_1094__h3__h1__h2 : ∃ (K₂ : ℕ),
  ∀ (n k : ℕ),
    K₂ < k →
      (2 : ℕ) * k ≤ n →
        n < k * k → k % (2 : ℕ) = (1 : ℕ) → n % (2 : ℕ) = (1 : ℕ) → ∃ (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 20261014T112100Z-t1014-z-partial.lean (merged in b272cb8cb9cb, attestation 000523).

h_odd_k3 → erdos-1094--h3--h1--h2--h1 (open)
$\displaystyle \exists K_1\ \forall n,k\in\mathbb{N}:\quad K_1<k,\ \ 2k\le n<k^2,\ \ k \text{ odd},\ \ n \text{ odd},\ \ 3\mid k \implies \exists\,p\le k \text{ prime with } n \bmod p < k \bmod p$
h_odd_rest → erdos-1094--h3--h1--h2--h2 (open)
$\displaystyle \exists K_2\ \forall n,k\in\mathbb{N}:\quad K_2<k,\ \ 2k\le n<k^2,\ \ k \text{ odd},\ \ n \text{ odd},\ \ 3\nmid k,\ \ k \bmod 3 \le n \bmod 3 \implies \exists\,p\le k \text{ prime with } n \bmod p < k \bmod p$

Read the partial proof (Lean)

theorem erdos_1094__h3__h1__h2 : ∃ (K₂ : ℕ),
  ∀ (n k : ℕ),
    K₂ < k →
      (2 : ℕ) * k ≤ n →
        n < k * k → k % (2 : ℕ) = (1 : ℕ) → n % (2 : ℕ) = (1 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ p ≤ k ∧ n % p < k % p := by
  have hall : (∃ K₁ : ℕ, ∀ n k : ℕ, K₁ < k → 2 * k ≤ n → n < k * k → k % 2 = 1 → n % 2 = 1 →
        k % 3 = 0 → ∃ p : ℕ, Nat.Prime p ∧ p ≤ k ∧ n % p < k % p) ∧
      (∃ K₂ : ℕ, ∀ n k : ℕ, K₂ < k → 2 * k ≤ n → n < k * k → k % 2 = 1 → n % 2 = 1 →
        0 < k % 3 → k % 3 ≤ n % 3 → ∃ p : ℕ, Nat.Prime p ∧ p ≤ k ∧ n % p < k % p) := by
    refine ⟨?_, ?_⟩
    · have h_odd_k3 : ∃ K₁ : ℕ, ∀ n k : ℕ, K₁ < k → 2 * k ≤ n → n < k * k → k % 2 = 1 →
          n % 2 = 1 → k % 3 = 0 → ∃ p : ℕ, Nat.Prime p ∧ p ≤ k ∧ n % p < k % p := by sorry
      exact h_odd_k3
    · have h_odd_rest : ∃ K₂ : ℕ, ∀ n k : ℕ, K₂ < k → 2 * k ≤ n → n < k * k → k % 2 = 1 →
          n % 2 = 1 → 0 < k % 3 → k % 3 ≤ n % 3 →
          ∃ p : ℕ, Nat.Prime p ∧ p ≤ k ∧ n % p < k % p := by sorry
      exact h_odd_rest
  obtain ⟨K₁, h₁⟩ := hall.1
  obtain ⟨K₂, h₂⟩ := hall.2
  refine ⟨max K₁ (max K₂ 2), fun n k hk h2k hnk hk2 hn2 => ?_⟩
  have hK₁ : K₁ < k := lt_of_le_of_lt (le_max_left _ _) hk
  have hK₂ : K₂ < k := lt_of_le_of_lt (le_trans (le_max_left _ _) (le_max_right _ _)) hk
  have hk3 : 3 ≤ k := lt_of_le_of_lt (le_trans (le_max_right K₂ 2) (le_max_right _ _)) hk
  by_cases h0 : k % 3 = 0
  · exact h₁ n k hK₁ h2k hnk hk2 hn2 h0
  · by_cases hlt : n % 3 < k % 3
    · exact ⟨3, Nat.prime_three, hk3, hlt⟩
    · exact h₂ n k hK₂ h2k hnk hk2 hn2 (Nat.pos_of_ne_zero h0) (Nat.le_of_not_lt hlt)

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--h2/attempts/20261014T112100Z-t1014-z-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

Notes

Numerical check (2026-10-12, finite range, not a proof): smallest working $K$ in range $K_2=39$; pairs found: 93 failures. full text →

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 (3 versions)

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--h2».Context

open scoped Nat

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

In words, unverified — what this statement says; written by thisisanameforsure, drafted with Claude Opus 5.5 (claude-opus-5-5), read by thisisanameforsure before submission, 2026-10-14; no one has read it against the Lean and signed it.

Draft · drafted, by the model named above

$\displaystyle \exists K_2\ \forall n,k\in\mathbb{N}:\quad K_2<k,\ \ 2k\le n<k^2,\ \ k \text{ odd},\ \ n \text{ odd} \implies \exists\,p\le k \text{ prime with } n \bmod p < k \bmod p$

Lean writes $k^2$ as k * k, and "odd" as k % 2 = 1 and n % 2 = 1.
n % p is the least non-negative residue, so the condition reads $n \bmod p < k \bmod p$.
Nothing is said about even $k$, or about odd $k$ with even $n$.

By Kummer's theorem such a $p$ divides $\binom{n}{k}$, since subtracting $k$ from $n$ in base $p$ borrows at the last digit. The statement itself mentions no binomial coefficient.

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

History: 3 versions on record

2026-10-09 · written by t1009-a, drafted with Claude Opus 5.5 (claude-opus-5-5) as agent t1009-a · not signed · gloss/a6faaba2dc6a….md · the first version of its chain
Read this version
There is a natural number K₂ such that, for all natural numbers n and k with k greater than K₂, k odd, n odd, n at least 2k and n less than k squared, there is a prime p at most k for which the remainder of n on division by p is smaller than the remainder of k on division by p.

Here n % p and k % p are natural-number remainders. Nothing is said about even k or even n, and nothing about C(n, k) itself.
2026-10-14 · written by thisisanameforsure, drafted with Claude Opus 5.5 (claude-opus-5-5), read by thisisanameforsure before submission · not signed · gloss/a2ee721ef615….md · diff to its predecessor
Read this version
$\displaystyle \exists K_2\ \forall n,k\in\mathbb{N}:\quad K_2<k,\ \ 2k\le n<k^2,\ \ k \text{ odd},\ \ n \text{ odd} \implies \exists\,p\le k \text{ prime with } n \bmod p < k \bmod p$
- Lean writes $k^2$ as k * k, and "odd" as k % 2 = 1 and n % 2 = 1.
- n % p is the least non-negative residue, so the condition reads $n \bmod p < k \bmod p$.
- Nothing is said about even $k$, or about odd $k$ with even $n$.
By Kummer's theorem such a $p$ divides $\binom{n}{k}$, since subtracting $k$ from $n$ in base $p$ borrows at the last digit. The statement itself mentions no binomial coefficient.
2026-10-18 · written by f29-words, drafted with Claude Fable 5.1 (claude-fable-5-1) · not signed · current · gloss/56985d0ad05c….md · diff to its predecessor
Read this version
$\displaystyle \exists K_2\ \forall n,k\in\mathbb{N}:\quad K_2<k,\ \ 2k\le n<k^2,\ \ k \text{ odd},\ \ n \text{ odd} \implies \exists\,p\le k \text{ prime with } n \bmod p < k \bmod p$
- Lean writes $k^2$ as k * k, and "odd" as k % 2 = 1 and n % 2 = 1.
- n % p is the least non-negative residue, so the condition reads $n \bmod p < k \bmod p$.
- Nothing is said about even $k$, or about odd $k$ with even $n$.
By Kummer's theorem such a $p$ divides $\binom{n}{k}$, since subtracting $k$ from $n$ in base $p$ borrows at the last digit. The statement itself mentions no binomial coefficient.

Diff of a2ee721ef615 against a6faaba2dc6a

@@ -1,3 +1,7 @@
-There is a natural number K₂ such that, for all natural numbers n and k with k greater than K₂, k odd, n odd, n at least 2k and n less than k squared, there is a prime p at most k for which the remainder of n on division by p is smaller than the remainder of k on division by p.
+$$\exists K_2\ \forall n,k\in\mathbb{N}:\quad K_2<k,\ \ 2k\le n<k^2,\ \ k \text{ odd},\ \ n \text{ odd} \implies \exists\,p\le k \text{ prime with } n \bmod p < k \bmod p$$
 
-Here n % p and k % p are natural-number remainders. Nothing is said about even k or even n, and nothing about C(n, k) itself.
+- Lean writes $k^2$ as `k * k`, and "odd" as `k % 2 = 1` and `n % 2 = 1`.
+- `n % p` is the least non-negative residue, so the condition reads $n \bmod p < k \bmod p$.
+- Nothing is said about even $k$, or about odd $k$ with even $n$.
+
+By Kummer's theorem such a $p$ divides $\binom{n}{k}$, since subtracting $k$ from $n$ in base $p$ borrows at the last digit. The statement itself mentions no binomial coefficient.

Diff of 56985d0ad05c against a2ee721ef615

(the words are the same)

Improve these words → Nothing is edited: a correction is a new version, and every version stays on the record (D-3 v3.30).

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

Depends on (2), each in words

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

erdos-1094--h3--h1--h2--h1: $\exists K_1\ \forall n,k\in\mathbb{N}:\quad K_1<k,\ \ 2k\le n<k^2,\ \ k \text{ odd},\ \ n \text{ odd},\ \ 3\mid k \implies \exists\,p\le k \text{ prime with } n \bmod p < k \bmod p$
erdos-1094--h3--h1--h2--h2: $\exists K_2\ \forall n,k\in\mathbb{N}:\quad K_2<k,\ \ 2k\le n<k^2,\ \ k \text{ odd},\ \ n \text{ odd},\ \ 3\nmid k,\ \ k \bmod 3 \le n \bmod 3 \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/000523.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--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-z; merged in b272cb8cb9cb under attestations/000523.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--h2/attempts/20261014T112100Z-t1014-z-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 20261014T112100Z-t1014-z-partial.lean, extracted by the gate at f97b6921b55b 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.

hall have (∃ (K₁ : ℕ), ∀ (n k : ℕ), K₁ < k → (2 : ℕ) * k ≤ n → n < k * k → k % (2 : ℕ) = (1 : ℕ) → n % (2 : ℕ) = (1 : ℕ) → k % (3 : ℕ) = (0 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ p ≤ k ∧ n % p < k % p) ∧ ∃ (K₂ : ℕ), ∀ (n k : ℕ), K₂ < k → (2 : ℕ) * k ≤ n → n < k * k → k % (2 : ℕ) = (1 : ℕ) → n % (2 : ℕ) = (1 : ℕ) → (0 : ℕ) < k % (3 : ℕ) → k % (3 : ℕ) ≤ n % (3 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ p ≤ k ∧ n % p < k % p
Leaves ∃ (K₂ : ℕ), ∀ (n k : ℕ), K₂ < k → (2 : ℕ) * k ≤ n → n < k * k → k % (2 : ℕ) = (1 : ℕ) → n % (2 : ℕ) = (1 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ p ≤ k ∧ n % p < k % p, with hall : (∃ (K₁ : ℕ), ∀ (n k : ℕ), K₁ < k → (2 : ℕ) * k ≤ n → n < k * k → k % (2 : ℕ) = (1 : ℕ) → n % (2 : ℕ) = (1 : ℕ) → k % (3 : ℕ) = (0 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ p ≤ k ∧ n % p < k % p) ∧ ∃ (K₂ : ℕ), ∀ (n k : ℕ), K₂ < k → (2 : ℕ) * k ≤ n → n < k * k → k % (2 : ℕ) = (1 : ℕ) → n % (2 : ℕ) = (1 : ℕ) → (0 : ℕ) < k % (3 : ℕ) → k % (3 : ℕ) ≤ n % (3 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ p ≤ k ∧ n % p < k % p.
Uses library Nat.Prime, And.intro.
Lean, lines 14–25
```
  have hall : (∃ K₁ : ℕ, ∀ n k : ℕ, K₁ < k → 2 * k ≤ n → n < k * k → k % 2 = 1 → n % 2 = 1 →
        k % 3 = 0 → ∃ p : ℕ, Nat.Prime p ∧ p ≤ k ∧ n % p < k % p) ∧
      (∃ K₂ : ℕ, ∀ n k : ℕ, K₂ < k → 2 * k ≤ n → n < k * k → k % 2 = 1 → n % 2 = 1 →
        0 < k % 3 → k % 3 ≤ n % 3 → ∃ p : ℕ, Nat.Prime p ∧ p ≤ k ∧ n % p < k % p) := by
    refine ⟨?_, ?_⟩
    · have h_odd_k3 : ∃ K₁ : ℕ, ∀ n k : ℕ, K₁ < k → 2 * k ≤ n → n < k * k → k % 2 = 1 →
          n % 2 = 1 → k % 3 = 0 → ∃ p : ℕ, Nat.Prime p ∧ p ≤ k ∧ n % p < k % p := by sorry
      exact h_odd_k3
    · have h_odd_rest : ∃ K₂ : ℕ, ∀ n k : ℕ, K₂ < k → 2 * k ≤ n → n < k * k → k % 2 = 1 →
          n % 2 = 1 → 0 < k % 3 → k % 3 ≤ n % 3 →
          ∃ p : ℕ, Nat.Prime p ∧ p ≤ k ∧ n % p < k % p := by sorry
      exact h_odd_rest
```
targets/erdos-1094/nodes/erdos-1094--h3--h1--h2/attempts/20261014T112100Z-t1014-z-partial.lean, lines 14–25 at 6ba7fea98468 ↗
1. hall.s1 case
  Leaves ∃ (K₁ : ℕ), ∀ (n k : ℕ), K₁ < k → (2 : ℕ) * k ≤ n → n < k * k → k % (2 : ℕ) = (1 : ℕ) → n % (2 : ℕ) = (1 : ℕ) → k % (3 : ℕ) = (0 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ p ≤ k ∧ n % p < k % p.
  Lean, lines 19–21
  · have h_odd_k3 : ∃ K₁ : ℕ, ∀ n k : ℕ, K₁ < k → 2 * k ≤ n → n < k * k → k % 2 = 1 → n % 2 = 1 → k % 3 = 0 → ∃ p : ℕ, Nat.Prime p ∧ p ≤ k ∧ n % p < k % p := by sorry exact h_odd_k3
  targets/erdos-1094/nodes/erdos-1094--h3--h1--h2/attempts/20261014T112100Z-t1014-z-partial.lean, lines 19–21 at 6ba7fea98468 ↗
  hall.s1.h_odd_k3 hole ∃ (K₁ : ℕ), ∀ (n k : ℕ), K₁ < k → (2 : ℕ) * k ≤ n → n < k * k → k % (2 : ℕ) = (1 : ℕ) → n % (2 : ℕ) = (1 : ℕ) → k % (3 : ℕ) = (0 : ℕ) → ∃ (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 : ℕ) = (1 : ℕ) → n % (2 : ℕ) = (1 : ℕ) → k % (3 : ℕ) = (0 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ p ≤ k ∧ n % p < k % p, with h_odd_k3 : ∃ (K₁ : ℕ), ∀ (n k : ℕ), K₁ < k → (2 : ℕ) * k ≤ n → n < k * k → k % (2 : ℕ) = (1 : ℕ) → n % (2 : ℕ) = (1 : ℕ) → k % (3 : ℕ) = (0 : ℕ) → ∃ (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--h2--h1 (open).
  Lean, lines 19–20
  · have h_odd_k3 : ∃ K₁ : ℕ, ∀ n k : ℕ, K₁ < k → 2 * k ≤ n → n < k * k → k % 2 = 1 → n % 2 = 1 → k % 3 = 0 → ∃ p : ℕ, Nat.Prime p ∧ p ≤ k ∧ n % p < k % p := by sorry
  targets/erdos-1094/nodes/erdos-1094--h3--h1--h2/attempts/20261014T112100Z-t1014-z-partial.lean, lines 19–20 at 6ba7fea98468 ↗
2. hall.s2 case
  Leaves ∃ (K₂ : ℕ), ∀ (n k : ℕ), K₂ < k → (2 : ℕ) * k ≤ n → n < k * k → k % (2 : ℕ) = (1 : ℕ) → n % (2 : ℕ) = (1 : ℕ) → (0 : ℕ) < k % (3 : ℕ) → k % (3 : ℕ) ≤ n % (3 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ p ≤ k ∧ n % p < k % p.
  Lean, lines 22–25
  · have h_odd_rest : ∃ K₂ : ℕ, ∀ n k : ℕ, K₂ < k → 2 * k ≤ n → n < k * k → k % 2 = 1 → n % 2 = 1 → 0 < k % 3 → k % 3 ≤ n % 3 → ∃ p : ℕ, Nat.Prime p ∧ p ≤ k ∧ n % p < k % p := by sorry exact h_odd_rest
  targets/erdos-1094/nodes/erdos-1094--h3--h1--h2/attempts/20261014T112100Z-t1014-z-partial.lean, lines 22–25 at 6ba7fea98468 ↗
  hall.s2.h_odd_rest hole ∃ (K₂ : ℕ), ∀ (n k : ℕ), K₂ < k → (2 : ℕ) * k ≤ n → n < k * k → k % (2 : ℕ) = (1 : ℕ) → n % (2 : ℕ) = (1 : ℕ) → (0 : ℕ) < k % (3 : ℕ) → k % (3 : ℕ) ≤ n % (3 : ℕ) → ∃ (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 : ℕ) = (1 : ℕ) → n % (2 : ℕ) = (1 : ℕ) → (0 : ℕ) < k % (3 : ℕ) → k % (3 : ℕ) ≤ n % (3 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ p ≤ k ∧ n % p < k % p, with h_odd_rest : ∃ (K₂ : ℕ), ∀ (n k : ℕ), K₂ < k → (2 : ℕ) * k ≤ n → n < k * k → k % (2 : ℕ) = (1 : ℕ) → n % (2 : ℕ) = (1 : ℕ) → (0 : ℕ) < k % (3 : ℕ) → k % (3 : ℕ) ≤ n % (3 : ℕ) → ∃ (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--h2--h2 (open).
  Lean, lines 22–24
  · have h_odd_rest : ∃ K₂ : ℕ, ∀ n k : ℕ, K₂ < k → 2 * k ≤ n → n < k * k → k % 2 = 1 → n % 2 = 1 → 0 < k % 3 → k % 3 ≤ n % 3 → ∃ p : ℕ, Nat.Prime p ∧ p ≤ k ∧ n % p < k % p := by sorry
  targets/erdos-1094/nodes/erdos-1094--h3--h1--h2/attempts/20261014T112100Z-t1014-z-partial.lean, lines 22–24 at 6ba7fea98468 ↗
s2 obtain ∃ (K₁ : ℕ), ∀ (n k : ℕ), K₁ < k → (2 : ℕ) * k ≤ n → n < k * k → k % (2 : ℕ) = (1 : ℕ) → n % (2 : ℕ) = (1 : ℕ) → k % (3 : ℕ) = (0 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ p ≤ k ∧ n % p < k % p
Leaves ∃ (K₂ : ℕ), ∀ (n k : ℕ), K₂ < k → (2 : ℕ) * k ≤ n → n < k * k → k % (2 : ℕ) = (1 : ℕ) → n % (2 : ℕ) = (1 : ℕ) → ∃ (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 : ℕ) = (1 : ℕ) → n % (2 : ℕ) = (1 : ℕ) → k % (3 : ℕ) = (0 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ p ≤ k ∧ n % p < k % p.
Lean, line 26
```
  obtain ⟨K₁, h₁⟩ := hall.1
```
targets/erdos-1094/nodes/erdos-1094--h3--h1--h2/attempts/20261014T112100Z-t1014-z-partial.lean, line 26 at 6ba7fea98468 ↗
s3 obtain ∃ (K₂ : ℕ), ∀ (n k : ℕ), K₂ < k → (2 : ℕ) * k ≤ n → n < k * k → k % (2 : ℕ) = (1 : ℕ) → n % (2 : ℕ) = (1 : ℕ) → (0 : ℕ) < k % (3 : ℕ) → k % (3 : ℕ) ≤ n % (3 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ p ≤ k ∧ n % p < k % p
Leaves ∃ (K₂ : ℕ), ∀ (n k : ℕ), K₂ < k → (2 : ℕ) * k ≤ n → n < k * k → k % (2 : ℕ) = (1 : ℕ) → n % (2 : ℕ) = (1 : ℕ) → ∃ (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 : ℕ) = (1 : ℕ) → n % (2 : ℕ) = (1 : ℕ) → (0 : ℕ) < k % (3 : ℕ) → k % (3 : ℕ) ≤ n % (3 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ p ≤ k ∧ n % p < k % p.
Lean, line 27
```
  obtain ⟨K₂, h₂⟩ := hall.2
```
targets/erdos-1094/nodes/erdos-1094--h3--h1--h2/attempts/20261014T112100Z-t1014-z-partial.lean, line 27 at 6ba7fea98468 ↗
hK1 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 29
```
  have hK₁ : K₁ < k := lt_of_le_of_lt (le_max_left _ _) hk
```
targets/erdos-1094/nodes/erdos-1094--h3--h1--h2/attempts/20261014T112100Z-t1014-z-partial.lean, line 29 at 6ba7fea98468 ↗
hK2 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_trans, le_max_left, le_max_right.
Lean, line 30
```
  have hK₂ : K₂ < k := lt_of_le_of_lt (le_trans (le_max_left _ _) (le_max_right _ _)) hk
```
targets/erdos-1094/nodes/erdos-1094--h3--h1--h2/attempts/20261014T112100Z-t1014-z-partial.lean, line 30 at 6ba7fea98468 ↗
hk3 have (3 : ℕ) ≤ k
Leaves ∃ (p : ℕ), Nat.Prime p ∧ p ≤ k ∧ n % p < k % p, with hk3 : (3 : ℕ) ≤ k.
Uses library lt_of_le_of_lt, le_trans, le_max_right.
Lean, line 31
```
  have hk3 : 3 ≤ k := lt_of_le_of_lt (le_trans (le_max_right K₂ 2) (le_max_right _ _)) hk
```
targets/erdos-1094/nodes/erdos-1094--h3--h1--h2/attempts/20261014T112100Z-t1014-z-partial.lean, line 31 at 6ba7fea98468 ↗
s7 case
Leaves ∃ (p : ℕ), Nat.Prime p ∧ p ≤ k ∧ n % p < k % p, with h0 : k % (3 : ℕ) = (0 : ℕ).
Lean, line 33
```
  · exact h₁ n k hK₁ h2k hnk hk2 hn2 h0
```
targets/erdos-1094/nodes/erdos-1094--h3--h1--h2/attempts/20261014T112100Z-t1014-z-partial.lean, line 33 at 6ba7fea98468 ↗
s8 case
Leaves ∃ (p : ℕ), Nat.Prime p ∧ p ≤ k ∧ n % p < k % p, with h0 : ¬k % (3 : ℕ) = (0 : ℕ).
Lean, lines 34–36
```
  · by_cases hlt : n % 3 < k % 3
    · exact ⟨3, Nat.prime_three, hk3, hlt⟩
    · exact h₂ n k hK₂ h2k hnk hk2 hn2 (Nat.pos_of_ne_zero h0) (Nat.le_of_not_lt hlt)
```
targets/erdos-1094/nodes/erdos-1094--h3--h1--h2/attempts/20261014T112100Z-t1014-z-partial.lean, lines 34–36 at 6ba7fea98468 ↗
1. s8.s1 case
  Leaves ∃ (p : ℕ), Nat.Prime p ∧ p ≤ k ∧ n % p < k % p, with hlt : n % (3 : ℕ) < k % (3 : ℕ).
  Uses library Exists.intro, Nat.prime_three.
  Lean, line 35
  · exact ⟨3, Nat.prime_three, hk3, hlt⟩
  targets/erdos-1094/nodes/erdos-1094--h3--h1--h2/attempts/20261014T112100Z-t1014-z-partial.lean, line 35 at 6ba7fea98468 ↗
2. s8.s2 case
  Leaves ∃ (p : ℕ), Nat.Prime p ∧ p ≤ k ∧ n % p < k % p, with hlt : ¬n % (3 : ℕ) < k % (3 : ℕ).
  Uses library Nat.pos_of_ne_zero, Nat.le_of_not_lt.
  Lean, line 36
  · exact h₂ n k hK₂ h2k hnk hk2 hn2 (Nat.pos_of_ne_zero h0) (Nat.le_of_not_lt hlt)
  targets/erdos-1094/nodes/erdos-1094--h3--h1--h2/attempts/20261014T112100Z-t1014-z-partial.lean, line 36 at 6ba7fea98468 ↗

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

open scoped Nat

/-! Hole `h_odd` 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__h2 : ∃ (K₂ : ℕ),
  ∀ (n k : ℕ),
    K₂ < k →
      (2 : ℕ) * k ≤ n →
        n < k * k → k % (2 : ℕ) = (1 : ℕ) → n % (2 : ℕ) = (1 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ p ≤ k ∧ n % p < k % p := by
  have hall : (∃ K₁ : ℕ, ∀ n k : ℕ, K₁ < k → 2 * k ≤ n → n < k * k → k % 2 = 1 → n % 2 = 1 →
        k % 3 = 0 → ∃ p : ℕ, Nat.Prime p ∧ p ≤ k ∧ n % p < k % p) ∧
      (∃ K₂ : ℕ, ∀ n k : ℕ, K₂ < k → 2 * k ≤ n → n < k * k → k % 2 = 1 → n % 2 = 1 →
        0 < k % 3 → k % 3 ≤ n % 3 → ∃ p : ℕ, Nat.Prime p ∧ p ≤ k ∧ n % p < k % p) := by
    refine ⟨?_, ?_⟩
    · have h_odd_k3 : ∃ K₁ : ℕ, ∀ n k : ℕ, K₁ < k → 2 * k ≤ n → n < k * k → k % 2 = 1 →
          n % 2 = 1 → k % 3 = 0 → ∃ p : ℕ, Nat.Prime p ∧ p ≤ k ∧ n % p < k % p := by sorry
      exact h_odd_k3
    · have h_odd_rest : ∃ K₂ : ℕ, ∀ n k : ℕ, K₂ < k → 2 * k ≤ n → n < k * k → k % 2 = 1 →
          n % 2 = 1 → 0 < k % 3 → k % 3 ≤ n % 3 →
          ∃ p : ℕ, Nat.Prime p ∧ p ≤ k ∧ n % p < k % p := by sorry
      exact h_odd_rest
  obtain ⟨K₁, h₁⟩ := hall.1
  obtain ⟨K₂, h₂⟩ := hall.2
  refine ⟨max K₁ (max K₂ 2), fun n k hk h2k hnk hk2 hn2 => ?_⟩
  have hK₁ : K₁ < k := lt_of_le_of_lt (le_max_left _ _) hk
  have hK₂ : K₂ < k := lt_of_le_of_lt (le_trans (le_max_left _ _) (le_max_right _ _)) hk
  have hk3 : 3 ≤ k := lt_of_le_of_lt (le_trans (le_max_right K₂ 2) (le_max_right _ _)) hk
  by_cases h0 : k % 3 = 0
  · exact h₁ n k hK₁ h2k hnk hk2 hn2 h0
  · by_cases hlt : n % 3 < k % 3
    · exact ⟨3, Nat.prime_three, hk3, hlt⟩
    · exact h₂ n k hK₂ h2k hnk hk2 hn2 (Nat.pos_of_ne_zero h0) (Nat.le_of_not_lt hlt)

Annexes (1), in full

Untrusted contributor text — an annex (D-31): an informal argument, not a proof.

Untrusted: annex (D-31), by thisisanameforsure, drafted with Claude Opus 5.5 (claude-opus-5-5), read by thisisanameforsure before submission, 2026-10-14T07:36:08Z, licence CC-BY-4.0. Rendered from targets/erdos-1094/nodes/erdos-1094--h3--h1--h2/annex/9ef97f2b625cd3fc98c7c4b1abfb886513f9d7c83d2011c20712342dc9761776.md.

Numerical check (2026-10-12, finite range, not a proof): smallest working $K$ in range $K_2=39$; pairs found: 93 failures.

Range searched: every odd $k\le 1000$, every odd $n$ with $2k\le n<k^2$ (complete in that range).
Pairs $(n,k)$ found that force $K\ge k$: 93 failures, the last $(1469,39)$.
Smallest $K$ that works in this range: $K_2=39$.

The method, the cross-checks and the code are in the numerical annex on erdos-1094 (the root), dated 2026-10-12.

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 →