Skip to content

Erdős problem 1138

Erdős Problem 1138. Let x/2<y<xx/2 < y < x and C>1C > 1. If d=max⁡pn<x(pn+1−pn)d = \max_{p_n < x}(p_{n+1} - p_n), where pnp_n denotes the nn-th prime, then is it true that π(y+Cd)−π(y)∼Cdlog⁡y\pi(y + Cd) - \pi(y) \sim \frac{Cd}{\log y}?

No current result

No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.

Retained declaration

FormalConjectures/ErdosProblems/1138.lean

Formal Conjectures

FormalConjectures/ErdosProblems/1138.leanErdos1138.erdos_11385 linesExact file
False ↔  ∀ C > 1,    Asymptotics.IsEquivalent Erdos1138.snd_gt_half_fst (Erdos1138.primeCount_Ioc_mul_const C) fun x =>      match x with      | (x, y) => C * ↑(Erdos1138.sup_primeGap x) / Real.log y
SolvedProof has a holeformal conjecturesexternal proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.

Proof manifests naming this Problem

  • Jayyhk Erdős Leanjayyhk:erdos:1138
  • PLBY Lean proofsErdosProblems.Erdos1138

Reported activity

Work these sources record against this Problem. Source-reported attribution, not reviewed here.

  • AI collaborating with humans

    Erdős AI contributions wiki · 25 Apr, 2026

    Machine
    GPT-5.5 Pro, GPT-5.5 Thinking
    People
    Kireet Cheri, Sourish Kumrawat, Hrishi Sunder
    Open the source record

  • Formalization

    Erdős AI contributions wiki · 4 May, 2026

    Machine
    Aristotle
    Open the source record

  • construction

    VibeMathed

    Machine
    GPT-5.5 Pro, GPT-5.5 Thinking
    People
    Kireet Cheri, Sourish Kumrawat, Hrishi Sunder
    Reported outcome
    resolved
    Open the source record

Continue

Start a contributionBrowse the source filesOpen the collection entry

Search problems.science

Find a Problem, Result, source, or page