Erdős Problem 971
Let p(a, d) be the least prime congruent to a (mod d). Does there exist a constant c > 0 such that for all large d, p(a, d) > (1 + c) * φ(d) * log d for ≫ φ(d) many values of a?
Mathematical statement
Let p(a, d) be the least prime congruent to a (mod d).
Does there exist a constant c > 0 such that for all large d,
p(a, d) > (1 + c) * φ(d) * log d for ≫ φ(d) many values of a?
Statement source: Erdős Problems statement material
Statement terms: Source-specific
Source-specific terms. Therefore does not assert reuse rights beyond attributed display.
Statement artifacts, not proofs
These records expose exact Lean propositions and statement-only wrappers. Defining a proposition does not supply a proof of it. A placeholder-bearing target also contains no proof. Elaboration checks syntax and types; it does not certify that a formalization perfectly captures every nuance of the informal problem.
Pinned Lean formulation 1
erdos_971
theorem erdos_971 : answer(sorry) ↔ ∃ c > (0 : ℝ), ∃ C > (0 : ℝ), ∀ᶠ d in atTop, C * (d.totient : ℝ) ≤ #{a < d | a.Coprime d ∧ (leastCongruentPrime a d : ℝ) > (1 + c) * d.totient * log d} := by sorry- Statement source
- Formal Conjectures
- Lean version
- v4.27.0
- Placeholder
- Present; no proof artifact
- Source evidence
- Pinned source index
- Fidelity review
- Community formulation
References