Problems / erdos-1094 / erdos-1094--h3--h1--h1--h2--h1--h1
Residue form, k even, k ≡ 1 (mod 3), no carry at 3 to 13
erdos-1094--h3--h1--h1--h2--h1--h1
open
Hole h_k3one of erdos-1094--h3--h1--h1--h2--h1 (split by 20261015T145026Z-t1015c-a09-partial.lean).
$\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$
For all large even $k$ with $k\equiv 1 \pmod 3$, every $n$ with $2k\le n<k^2$, $n\not\equiv 0 \pmod 3$, and residue mod $q$ at least that of $k$ for each of $q=5,7,11,13$, has a prime $p\le k$ whose residue of $n$ is smaller than its residue of $k$. Lean writes the residue hypotheses as k % 3 = 1, 1 ≤ n % 3 and 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).
Lean
theorem erdos_1094__h3__h1__h1__h2__h1__h1 : ∃ (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 := by
sorryWhy 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 closes it.
What is known
Work on it
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--h1».Context
open scoped Nat
/-! Hole `h_k3one` 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__h1 : ∃ (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 := by
sorryA 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\ \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$
For all large even $k$ with $k\equiv 1 \pmod 3$, every $n$ with $2k\le n<k^2$, $n\not\equiv 0 \pmod 3$, and residue mod $q$ at least that of $k$ for each of $q=5,7,11,13$, has a prime $p\le k$ whose residue of $n$ is smaller than its residue of $k$. Lean writes the residue hypotheses as k % 3 = 1, 1 ≤ n % 3 and 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/31444fe269bc….md · Improve these words →
Rendered from targets/erdos-1094/nodes/erdos-1094--h3--h1--h1--h2--h1--h1/Statement.lean. Origin: compiler-derived.
Witness
Not checked — no run on this page records step 7 passing for it.
9fba8a70264a.import Mathlib import Nodes.«erdos-1094--h3--h1--h1--h2--h1--h1».Context open scoped Nat /-! The witness slot for a hole (D-29, F07-R6). Replace `sorry` with an instance satisfying this statement's hypotheses; until then the node is blocked. -/ 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 →
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).