Problems / erdos-257 / variant-5274cf38--h1--h1
m² primes ≡ 1 mod P between 2^m and 2^(m+m²)
variant-5274cf38--h1--h1
open
Hole hprimes of variant-5274cf38--h1 (split by 20261026T205203Z-t1026-b-partial.lean).
$\displaystyle \forall P \ge 1\ \exists m_0\ \forall m \ge m_0\ \exists S \subseteq \mathbb{P},\ |S| = m^2,\ \forall p \in S:\ p \equiv 1 \pmod P,\ 2^m < p \le 2^{m + m^2}$
A weak quantitative Dirichlet theorem: the prime number theorem in arithmetic progressions gives ≍ 2^{m+m²}/(φ(P) m²) such primes. Mathlib has Dirichlet's theorem only qualitatively; the cyclotomic argument gives a prime ≡ 1 mod n below (n+1)^n, which is too sparse for the averaging step.
Lean
theorem variant_5274cf38__h1__h1 : ∀ (P : ℕ),
(0 : ℕ) < P →
∃ (m₀ : ℕ),
∀ (m : ℕ),
m₀ ≤ m →
∃ (S : Finset ℕ),
S.card = m * m ∧ ∀ p ∈ S, Nat.Prime p ∧ p % P = (1 : ℕ) ∧ (2 : ℕ) ^ m < p ∧ p ≤ (2 : ℕ) ^ (m + m * m) := 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 t1026-b, awaiting a steward or curator
References and summary
Proposed by t1026-b, awaiting a steward or curator: Known: a proof is published and not formalised (record, 2026-10-26T21:35:36Z).
- C. J. de la Vallée Poussin, Recherches analytiques sur la théorie des nombres premiers, Ann. Soc. Sci. Bruxelles 20 (1896), 183–256, 281–397 (the prime number theorem in arithmetic progressions) — π(x; P, 1) ~ x/(φ(P) log x), which gives far more than m² primes ≡ 1 (mod P) in (2^m, 2^(m+m²)] for every large m
- H. Davenport, Multiplicative Number Theory, 3rd ed., GTM 74, Springer 2000, Chapter 20 (the prime number theorem for arithmetic progressions) — textbook statement of the same theorem
- H. L. Montgomery and R. C. Vaughan, Multiplicative Number Theory I: Classical Theory, Cambridge 2007, Theorem 11.16 (Siegel–Walfisz) — uniform form; any effective form of Dirichlet's theorem with a density bound suffices here
Untrusted contributor text — a literature summary (D-25 v3.35): the contributor’s reading, not a verdict.
Untrusted: summary by t1026-b, drafted with Claude Fable 5.1 through Claude Code (tester run 2026-10-26, agent B). Rendered from targets/erdos-257/nodes/variant-5274cf38--h1--h1/literature/20261026T213536Z-t1026-b.yaml.
The statement asks, for each period P, for m² distinct primes ≡ 1 (mod P) between 2^m and 2^(m+m²) once m is large. This is a weak quantitative form of Dirichlet's theorem: by the prime number theorem in arithmetic progressions the interval holds about 2^(m+m²)/(φ(P)(m+m²)) such primes. The pinned Mathlib has Dirichlet's theorem only as 'infinitely many' (Nat.setOf_prime_and_eq_mod_infinite) and the cyclotomic argument (Nat.exists_prime_gt_modEq_one), neither with a bound in this range, so the statement is known and not formalised. It is the only input left in the partial that reduces the purely periodic case of Erdős 257 (Luca–Tachiya 2014, Theorem 1.1 for 0/1 sequences) to it; the rest of Erdős's 1948 argument is proved in that partial's assembly.
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).
- variant-5274cf38--h1--h1 · Known: a proof is published and not formalised · proposed by
t1026-b· 2026-10-26T21:35:36Z · 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.«variant-5274cf38--h1--h1».Context
/-! Hole `hprimes` 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 variant_5274cf38__h1__h1 : ∀ (P : ℕ),
(0 : ℕ) < P →
∃ (m₀ : ℕ),
∀ (m : ℕ),
m₀ ≤ m →
∃ (S : Finset ℕ),
S.card = m * m ∧ ∀ p ∈ S, Nat.Prime p ∧ p % P = (1 : ℕ) ∧ (2 : ℕ) ^ m < p ∧ p ≤ (2 : ℕ) ^ (m + m * m) := 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 t1026-b, drafted with Claude Fable 5.1, 2026-10-26; no one has read it against the Lean and signed it.
Draft · drafted, by the model named above
$\displaystyle \forall P \ge 1\ \exists m_0\ \forall m \ge m_0\ \exists S \subseteq \mathbb{P},\ |S| = m^2,\ \forall p \in S:\ p \equiv 1 \pmod P,\ 2^m < p \le 2^{m + m^2}$
A weak quantitative Dirichlet theorem: the prime number theorem in arithmetic progressions gives ≍ 2^{m+m²}/(φ(P) m²) such primes. Mathlib has Dirichlet's theorem only qualitatively; the cyclotomic argument gives a prime ≡ 1 mod n below (n+1)^n, which is too sparse for the averaging step.
Rendered from gloss/e4dbab930b03….md · Improve these words →
Rendered from targets/erdos-257/nodes/variant-5274cf38--h1--h1/Statement.lean. Origin: compiler-derived.
Witness
Not checked — no run on this page records step 7 passing for it.
9b5b2c3ebb31.import Mathlib theorem witness : ∃ (P : ℕ), (0 : ℕ) < P := ⟨1, Nat.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).