Problems / erdos-1094 / erdos-1094--h3--h3--h2--h1
GR Lemma 5.1: {n/p} below σ carries weight σ Σ log p + o(k)
erdos-1094--h3--h3--h2--h1
open
Hole h_l51 of erdos-1094--h3--h3--h2 (split by 20261015T145123Z-t1015c-a02-partial.lean).
$\displaystyle \forall C\in\mathbb{N},\ \delta>0\ \exists K_5\ \forall n,k\in\mathbb{N},\ K_5<k,\ k^2\le C n\lfloor\log_2 k\rfloor,\ n<k^2,\ \forall \sigma\in[0,1]:\quad \Bigl|\sum_{\substack{p \text{ prime}\\ k/2<p<11k/20}}\ [\{n/p\}<\sigma]\,\log p \;-\; \sigma \sum_{\substack{p \text{ prime}\\ k/2<p<11k/20}} \log p\Bigr| \le \delta k$
For every constant $C$ and real $\delta>0$ there is a threshold $K_5$ such that for all $k>K_5$, all $n<k^2$ with $k^2\le C\,n\lfloor\log_2 k\rfloor$, and every real $\sigma\in[0,1]$, the $\log p$-weighted count of primes $p$ with $k<2p$ and $20p<11k$ whose fractional part $\{n/p\}$ is below $\sigma$ differs from $\sigma$ times the total weight $\sum\log p$ over the same primes by at most $\delta k$. $[\{n/p\}<\sigma]$ stands for Lean's if Int.fract (n / p) < σ then Real.log p else 0 with the quotient taken in $\mathbb{R}$; both sums run over Finset.range k filtered by the three conditions, and the range hypotheses are in $\mathbb{N}$ where Nat.log 2 k is $\lfloor\log_2 k\rfloor$ (and $0$ for $k\le 1$), a natural number, so the right-hand side is a product of naturals.
Lean
theorem erdos_1094__h3__h3__h2__h1 : ∀ (C : ℕ) (δ : ℝ),
(0 : ℝ) < δ →
∃ (K₅ : ℕ),
∀ (n k : ℕ),
K₅ < k →
k * k ≤ C * (n * Nat.log (2 : ℕ) k) →
n < k * k →
∀ (σ : ℝ),
(0 : ℝ) ≤ σ →
σ ≤ (1 : ℝ) →
|(∑ p ∈ Finset.range k with Nat.Prime p ∧ k < (2 : ℕ) * p ∧ (20 : ℕ) * p < (11 : ℕ) * k,
if Int.fract ((↑n : ℝ) / (↑p : ℝ)) < σ then Real.log (↑p : ℝ) else (0 : ℝ)) -
σ *
∑ p ∈ Finset.range k with Nat.Prime p ∧ k < (2 : ℕ) * p ∧ (20 : ℕ) * p < (11 : ℕ) * k,
Real.log (↑p : ℝ)| ≤
δ * (↑k : ℝ) := 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
Literature: Known: a proof is published and not formalised · proposed by t1016-lit, awaiting a steward or curator
References and summary
Proposed by t1016-lit, awaiting a steward or curator: Known: a proof is published and not formalised (record, 2026-10-16T12:14:30Z).
- A. Granville and O. Ramaré, Explicit bounds on exponential sums and the scarcity of squarefree binomial coefficients, Mathematika 43 (1996) 73-107 — Lemma 5.1 (preprint p. 18) with J = 1, and the partial-summation consequence (5.1), applied in the proof of Theorem 8 (section 5e, pp. 24-25). GR quote it from Sander.
- J. W. Sander, Prime power divisors of binomial coefficients, J. Reine Angew. Math. 430 (1992) 1-20 — The source of the equidistribution bound for {x/p} over primes p <= y that GR cite as [Sa2]; proved by exponential sums over primes (Vaughan's identity). Not read.
Untrusted contributor text — a literature summary (D-25 v3.35): the contributor’s reading, not a verdict.
Untrusted: summary by t1016-lit, drafted with Claude Opus 5.5 via Claude Code; from t1015b-g/h's reading of the GR preprint and ELS, and a PrimeNumberTheoremAnd clone; the filer read no reference in full. Rendered from targets/erdos-1094/nodes/erdos-1094--h3--h3--h2--h1/literature/20261016T121430Z-t1016-lit.yaml.
This node is GR's Lemma 5.1 at J = 1, weighted by log p, on primes in (k/2, 11k/20): the fractional parts n/p are equidistributed mod 1 to within delta*k once n >= k^2/(C log k). Published (Sander 1992, quoted by Granville-Ramaré 1996) and not formalised anywhere known to the filer. A translation would follow Sander: Vaughan's identity, bounds for exponential sums e(hx/p) over primes, then Erdős-Turán (or a direct count). It also needs the prime number theorem in the window, which is erdos-1094--h3--h3--h1--h1. Deep: the hardest node in the h3 subtree. The node uses x = n where GR use n - k; the bound is uniform in x.
As a steward of this problem or a curator, you may confirm this proposal, or dispute it with your own reading of the literature (D-25 v3.45).
- erdos-1094--h3--h3--h2--h1 · Known: a proof is published and not formalised · proposed by
t1016-lit· 2026-10-16T12:14:30Z · record
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--h3--h2--h1».Context
open scoped Nat
/-! Hole `h_l51` 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__h3__h2__h1 : ∀ (C : ℕ) (δ : ℝ),
(0 : ℝ) < δ →
∃ (K₅ : ℕ),
∀ (n k : ℕ),
K₅ < k →
k * k ≤ C * (n * Nat.log (2 : ℕ) k) →
n < k * k →
∀ (σ : ℝ),
(0 : ℝ) ≤ σ →
σ ≤ (1 : ℝ) →
|(∑ p ∈ Finset.range k with Nat.Prime p ∧ k < (2 : ℕ) * p ∧ (20 : ℕ) * p < (11 : ℕ) * k,
if Int.fract ((↑n : ℝ) / (↑p : ℝ)) < σ then Real.log (↑p : ℝ) else (0 : ℝ)) -
σ *
∑ p ∈ Finset.range k with Nat.Prime p ∧ k < (2 : ℕ) * p ∧ (20 : ℕ) * p < (11 : ℕ) * k,
Real.log (↑p : ℝ)| ≤
δ * (↑k : ℝ) := 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 \forall C\in\mathbb{N},\ \delta>0\ \exists K_5\ \forall n,k\in\mathbb{N},\ K_5<k,\ k^2\le C n\lfloor\log_2 k\rfloor,\ n<k^2,\ \forall \sigma\in[0,1]:\quad \Bigl|\sum_{\substack{p \text{ prime}\\ k/2<p<11k/20}}\ [\{n/p\}<\sigma]\,\log p \;-\; \sigma \sum_{\substack{p \text{ prime}\\ k/2<p<11k/20}} \log p\Bigr| \le \delta k$
For every constant $C$ and real $\delta>0$ there is a threshold $K_5$ such that for all $k>K_5$, all $n<k^2$ with $k^2\le C\,n\lfloor\log_2 k\rfloor$, and every real $\sigma\in[0,1]$, the $\log p$-weighted count of primes $p$ with $k<2p$ and $20p<11k$ whose fractional part $\{n/p\}$ is below $\sigma$ differs from $\sigma$ times the total weight $\sum\log p$ over the same primes by at most $\delta k$. $[\{n/p\}<\sigma]$ stands for Lean's if Int.fract (n / p) < σ then Real.log p else 0 with the quotient taken in $\mathbb{R}$; both sums run over Finset.range k filtered by the three conditions, and the range hypotheses are in $\mathbb{N}$ where Nat.log 2 k is $\lfloor\log_2 k\rfloor$ (and $0$ for $k\le 1$), a natural number, so the right-hand side is a product of naturals.
Rendered from gloss/295350954d36….md · Improve these words →
Rendered from targets/erdos-1094/nodes/erdos-1094--h3--h3--h2--h1/Statement.lean. Origin: compiler-derived.
Witness
Not checked — no run on this page records step 7 passing for it.
620e317247df.import Mathlib import Nodes.«erdos-1094--h3--h3--h2--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 : ∃ (C : ℕ) (δ : ℝ), (0 : ℝ) < δ := ⟨0, 1, one_pos⟩
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).