238.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 10 curated AI-written annotations and 7190 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

2 declarations, 2 contain sorry, 0 declared as axioms

Erdős Problem 238

Reference: erdosproblems.com/238

Imports (1)

FormalConjecturesUtil

theorem Erdos238.erdos_238 Let c₁, c₂ > 0 sorry line 38 source
Source documentation
Let c₁, c₂ > 0. Is it true that for any sufficiently large x, there exists more than c₁ * log x many consecutive primes ≤ x such that the difference between any two is > c₂?

depends on sorry what this means
Statement uses: Iff, True, Real, GT.gt, OfNat.ofNat, Nat, Filter.Eventually, Exists, And, LT.lt, HMul.hMul, Real.log, Fin, LE.le, Eq, Nat.nth, Nat.Prime, HAdd.hAdd, HSub.hSub, primeGap and 1 more
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
32 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_238 : answer(sorry) ↔ ∀ᵉ (c₁ > 0) (c₂ > 0), ∀ᶠ (x : ℝ) in atTop, ∃ (k : ℕ),
    c₁ * log x < k ∧ ∃ f : Fin k → ℕ, ∃ m, (∀ i, f i ≤ x ∧ f i = (m + i.1).nth Nat.Prime)
    ∧ ∀ i : Fin (k - 1), c₂ < primeGap (m + i.1) := by
…
```
Mentions: primeGap
theorem Erdos238.erdos_238.variants.small_c1 It is well-known that the conjecture above is true when c₁ is sufficiently small sorry line 47 source
Source documentation
It is well-known that the conjecture above is true when c₁ is sufficiently small.

depends on sorry what this means
Statement uses: Nat, GT.gt, OfNat.ofNat, Filter.Eventually, Real, Exists, And, LT.lt, HMul.hMul, Real.log, Fin, LE.le, Eq, Nat.nth, Nat.Prime, HAdd.hAdd, HSub.hSub, primeGap, Filter.atTop, nhdsWithin and 1 more
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
38 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_238.variants.small_c1 : ∀ c₂ > 0, ∀ᶠ c₁ in 𝓝[>] 0, ∀ᶠ (x : ℝ) in atTop, ∃ (k : ℕ),
    c₁ * log x < k ∧ ∃ f : Fin k → ℕ, ∃ m, (∀ i, f i ≤ x ∧ f i = (m + i.1).nth Nat.Prime)
    ∧ ∀ i : Fin (k - 1), c₂ < primeGap (m + i.1) := by
…
```
Mentions: primeGap