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

6 declarations, 5 contain sorry, 0 declared as axioms

Erdős Problem 382

References:

erdosproblems.com/382
[ErGr80] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathematique (1980).

Imports (1)

FormalConjecturesUtil

def Erdos382.LargestPrimeRepeated Documented declaration: LargestPrimeRepeated line 42 source
Source documentation
LargestPrimeRepeated u v means that $1 \leq u \leq v$ and the largest prime $p$ dividing $\prod_{u \leq m \leq v} m$ appears in it with exponent at least $2$, that is $p^2$ divides the product.
We require $u \geq 1$, since for $u = 0$ the product is $0$ and Nat.maxPrimeFac 0 = 0. We also require $v \geq 2$: the only other pair is $u = v = 1$, where the product is $1$, which has no prime factor, and the junk value Nat.maxPrimeFac 1 = 1 would make the condition hold.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: And, LE.le, OfNat.ofNat, Dvd.dvd, HPow.hPow, Nat.maxPrimeFac, Finset.prod, Finset.Icc
10 instances, coercions and auxiliary constants left out.
```
def LargestPrimeRepeated (u v : ℕ) : Prop :=
…
```
theorem Erdos382.largestPrimeRepeated_48_50 The pair $(48, 50)$ satisfies the condition: $48 \cdot 49 \cdot 50 = 2^5 \cdot 3 \cdot 5^2 \cdot 7^2$, and the largest prime $7$ appears with exponent $2$ sorry line 49 source
Source documentation
The pair $(48, 50)$ satisfies the condition: $48 \cdot 49 \cdot 50 = 2^5 \cdot 3 \cdot 5^2 \cdot 7^2$, and the largest prime $7$ appears with exponent $2$.

depends on sorry what this means
Statement uses: Erdos382.LargestPrimeRepeated, OfNat.ofNat, Nat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
2 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem largestPrimeRepeated_48_50 : LargestPrimeRepeated 48 50 := by
…
```
Mentions: Erdos382.LargestPrimeRepeated
theorem Erdos382.lt_two_mul_of_largestPrimeRepeated If the condition holds, then $v < 2u$ sorry line 58 source
Source documentation
If the condition holds, then $v < 2u$.
Otherwise $2u \leq v$, and by Bertrand's postulate there is a prime $q$ with $v/2 < q \leq v$, so $u \leq q \leq v$. The largest prime $p$ of the product satisfies $p \geq q > v/2$. Hence $p$ divides exactly one factor $m \in [u, v]$, namely $m = p$, and $p$ appears with exponent $1$.

depends on sorry what this means
Statement uses: Nat, Erdos382.LargestPrimeRepeated, LT.lt, HMul.hMul, OfNat.ofNat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
8 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem lt_two_mul_of_largestPrimeRepeated {u v : ℕ} (h : LargestPrimeRepeated u v) :
    v < 2 * u := by
…
```
Mentions: Erdos382.LargestPrimeRepeated
theorem Erdos382.erdos_382.parts.i Let $u \leq v$ be such that the largest prime dividing $\prod_{u \leq m \leq v} m$ appears with exponent at least $2$ sorry line 72 source
Source documentation
Let $u \leq v$ be such that the largest prime dividing $\prod_{u \leq m \leq v} m$ appears with exponent at least $2$. Is it true that $v - u = v^{o(1)}$?
We read this as: for every $\epsilon > 0$, every such pair with $v$ large enough satisfies $v - u \leq v^{\epsilon}$. Cambie observed that this question reduces to old conjectures on gaps between primes; for example, it follows from Cramér's conjecture. See also Erdős Problems 380 and 383.

depends on sorry what this means
Statement uses: Iff, True, Real, GT.gt, OfNat.ofNat, Filter.Eventually, Nat, Erdos382.LargestPrimeRepeated, LE.le, HSub.hSub, HPow.hPow, Filter.atTop
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
23 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_382.parts.i : answer(sorry) ↔
    ∀ ε > (0 : ℝ), ∀ᶠ v : ℕ in atTop, ∀ u : ℕ, LargestPrimeRepeated u v →
      ((v - u : ℕ) : ℝ) ≤ (v : ℝ) ^ ε := by
…
```
Mentions: Erdos382.LargestPrimeRepeated
theorem Erdos382.erdos_382.parts.ii Let $u \leq v$ be such that the largest prime dividing $\prod_{u \leq m \leq v} m$ appears with exponent at least $2$ sorry line 85 source
Source documentation
Let $u \leq v$ be such that the largest prime dividing $\prod_{u \leq m \leq v} m$ appears with exponent at least $2$. Can $v - u$ be arbitrarily large?
That is, for every $k$, is there such a pair with $v - u \geq k$? Cambie gives a heuristic that suggests the answer is yes.

depends on sorry what this means
Statement uses: Iff, True, Nat, Exists, And, Erdos382.LargestPrimeRepeated, LE.le, HSub.hSub
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat
7 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_382.parts.ii : answer(sorry) ↔
    ∀ k : ℕ, ∃ u v : ℕ, LargestPrimeRepeated u v ∧ k ≤ v - u := by
…
```
Mentions: Erdos382.LargestPrimeRepeated
theorem Erdos382.erdos_382.variants.ramachandra Erdős and Graham [ErGr80] report that it follows from results of Ramachandra that $v - u \leq v^{1/2+o(1)}$ for every pair $u \leq v$ as in Erdos382.erdos_382.parts.i sorry line 97 source
Source documentation
Erdős and Graham [ErGr80] report that it follows from results of Ramachandra that $v - u \leq v^{1/2+o(1)}$ for every pair $u \leq v$ as in Erdos382.erdos_382.parts.i.
That is, for every $\epsilon > 0$, every such pair with $v$ large enough satisfies $v - u \leq v^{1/2+\epsilon}$.

depends on sorry what this means
Statement uses: Real, GT.gt, OfNat.ofNat, Filter.Eventually, Nat, Erdos382.LargestPrimeRepeated, LE.le, HSub.hSub, HPow.hPow, HAdd.hAdd, HDiv.hDiv, Filter.atTop
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
44 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_382.variants.ramachandra :
    ∀ ε > (0 : ℝ), ∀ᶠ v : ℕ in atTop, ∀ u : ℕ, LargestPrimeRepeated u v →
      ((v - u : ℕ) : ℝ) ≤ (v : ℝ) ^ ((1 : ℝ) / 2 + ε) := by
…
```
Mentions: Erdos382.LargestPrimeRepeated