Open Proof Network

Problems / erdos-1094 / erdos-1094--h2--h2--h1

BHP short-interval primes

erdos-1094--h2--h2--h1

open

Restated as hole h_bhp of erdos-1094--h2--h1 (split by 20261014T075000Z-t1014-a-partial.lean).

Hole h_bhp of erdos-1094--h2--h2 (split by 20261014T073500Z-t1014-a-partial.lean).

$\displaystyle \exists C>0\ \ \exists k_0\in\mathbb{N}\ \ \forall k\ge k_0:\qquad \frac{C\,k^{21/40}}{\log k}\ \le\ \#\bigl\{p\text{ prime}:\ k<p<k+k^{21/40}\bigr\}$

For one constant $C>0$ and all large $k$, the interval $(k,\,k+k^{21/40})$ contains at least $C\,k^{21/40}/\log k$ primes: the Baker–Harman–Pintz short-interval prime count. In the Lean the set is a finite set of integers $p$ in the open interval $(\lfloor k\rfloor,\lceil k+k^{21/40}\rceil)$ filtered by $0<p$, $|p|$ prime and $k<p<k+k^{21/40}$ over the reals, which is exactly the primes of that real interval; its cardinality is cast to $\mathbb{R}$, $k^{21/40}$ is a real power and $\log$ is the natural logarithm.

unverified · history

Lean
theorem erdos_1094__h2__h2__h1 : ∃ (C : ℝ),
  (0 : ℝ) < C ∧
    ∃ (k₀ : ℕ),
      ∀ (k : ℕ),
        k₀ ≤ k →
          C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤
            (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ |
                    (0 : ℤ) < p ∧
                      Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card :
              ℝ) := by
  sorry
Why 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 t1014-z, awaiting a steward or curator

References and summary
Literature status

Proposed by t1014-z, awaiting a steward or curator: Known: a proof is published and not formalised (record, 2026-10-14T11:19:14Z).

Untrusted contributor text — a literature summary (D-25 v3.35): the contributor’s reading, not a verdict.

Untrusted: summary by t1014-z, drafted with Claude Opus 5.5 (claude-opus-5-5) through Claude Code, tester C; PDF read with pdftotext. Rendered from targets/erdos-1094/nodes/erdos-1094--h2--h2--h1/literature/20261014T111914Z-t1014-z.yaml.

This node is BHP 2001's counting bound in the forward form: with C = 9/100 (any C slightly below it, to absorb the strict upper endpoint k < p < k + k^0.525 and integer k, at most one prime of difference), for all k beyond some k0 there are at least C k^0.525 / log k primes in (k, k + k^0.525). Exponent 21/40 = 0.525 matches, log is natural log, the k0 is ineffective-as-stated (BHP say it could be made effective with effort). The match between the paper's display and this Lean statement is my reading, not checked by anyone else; nothing of BHP is formalised. Note BHP's sieve is not a routine formalisation, so 'known', not 'elementary'.

Work on it

Work on this statement →

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--h2--h2--h1».Context

open scoped Nat

/-! Hole `h_bhp` 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__h2__h2__h1 : ∃ (C : ℝ),
  (0 : ℝ) < C ∧
    ∃ (k₀ : ℕ),
      ∀ (k : ℕ),
        k₀ ≤ k →
          C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤
            (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ |
                    (0 : ℤ) < p ∧
                      Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card :
              ℝ) := by
  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 →

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 C>0\ \ \exists k_0\in\mathbb{N}\ \ \forall k\ge k_0:\qquad \frac{C\,k^{21/40}}{\log k}\ \le\ \#\bigl\{p\text{ prime}:\ k<p<k+k^{21/40}\bigr\}$

For one constant $C>0$ and all large $k$, the interval $(k,\,k+k^{21/40})$ contains at least $C\,k^{21/40}/\log k$ primes: the Baker–Harman–Pintz short-interval prime count. In the Lean the set is a finite set of integers $p$ in the open interval $(\lfloor k\rfloor,\lceil k+k^{21/40}\rceil)$ filtered by $0<p$, $|p|$ prime and $k<p<k+k^{21/40}$ over the reals, which is exactly the primes of that real interval; its cardinality is cast to $\mathbb{R}$, $k^{21/40}$ is a real power and $\log$ is the natural logarithm.

Rendered from gloss/c42945b0508d….md · Improve these words →

Rendered from targets/erdos-1094/nodes/erdos-1094--h2--h2--h1/Statement.lean. Origin: skeleton-hole.

Witness

Not checked — no run on this page records step 7 passing for it.

Witness.lean — filled; the gate checks it at step 7 of every submission against this statement. Rendered from targets/erdos-1094/nodes/erdos-1094--h2--h2--h1/Witness.lean, sha256 1aa8a1c1b9f3.
import Mathlib

open scoped Nat

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 →

Attempts (1)

1 recorded. Routes refuted: none. Failure classes: missing-library 1.

No partial assembly filed.

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).

How to read a statement’s page →