FormalConjectures.ErdosProblems.«1138»

/-
Copyright 2026 The Formal Conjectures Authors.

Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at

    https://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/

import FormalConjecturesUtil

Erdős Problem 1138

References:

erdosproblems.com/1138

[Va99] Vardi, I., Prime census. (1999).

[Kum26] Kumrawat, S., Disproof of Erdős Problem 1138.

Note that the conjecture has a claimed disproof found at: https://sourish-kumrawat.github.io/papers/Erdos_1138.pdf, see the discussion section on the Erdos problems website for more information.


open Nat Filter Asymptotics Real Set


namespace Erdos1138

The maximal prime gap below $x$, i.e. $d(x) = \max_{p_n < x}(p_{n+1} - p_n)$, where $p_n$ denotes the $n$-th prime.

noncomputable def sup_primeGap (x : ℝ) : ℕ := (Finset.range (primeCounting' ⌈x⌉₊)).sup primeGap

The filter on $\mathbb{R} \times \mathbb{R}$ corresponding to sending $x \to \infty$ subject to $x/2 < y < x$

abbrev snd_gt_half_fst : Filter (ℝ × ℝ) := atTop.comap Prod.fst ⊓ 𝓟 {p | p.2 ∈ Ioo (p.1 / 2) p.1}

Given a pair $(x,y)$, this is the amount of primes in the interval above $y$, of length equalling the largest prime gap before $x$, scaled by a constant $C$.

noncomputable def primeCount_Ioc_mul_const (C : ℝ) : (ℝ × ℝ) → ℝ :=
  fun (x, y) ↦ (primeCounting ⌊y + C * sup_primeGap x⌋₊ - primeCounting ⌊y⌋₊)

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

@[category research solved, AMS 11,
formal_proof using formal_conjectures at "https://github.com/YanYablonovskiy/formal-conjectures/blob/7c134317104d3b98ecc751afbb79ec0adddf8e7c/FormalConjectures/ErdosProblems/1138a.lean#L496"]
theorem declaration uses 'sorry'erdos_1138 : answer(False) ↔ ∀C > 1,
    primeCount_Ioc_mul_const C ~[snd_gt_half_fst] fun (x, y) ↦
      C * (sup_primeGap x) / Real.log y := by⊢ False ↔
  ∀ C > 1,
    primeCount_Ioc_mul_const C ~[snd_gt_half_fst] fun x =>
      match x with
      | (x, y) => C * ↑(sup_primeGap x) / Real.log y
  sorryAll goals completed! 🐙


end Erdos1138