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

References:

erdosproblems.com/841
[ErSe92] Erdős, Paul and Selfridge, J. L., Problems and Solutions: Solutions: 6655. Amer. Math. Monthly (1992), 791--794.
[BPZ24] Bui, Hung M. and Pratt, Kyle and Zaharescu, Alexandru, A problem of Erdős-Graham-Granville-Selfridge on integral points on hyperelliptic curves. Math. Proc. Cambridge Philos. Soc. (2024), 309--323.
[Gu04] Guy, Richard K., Unsolved problems in number theory. (2004), xviii+437.

Imports (1)

FormalConjecturesUtil

def Erdos841.t t n is the least T such that {n + 1, …, n + T} contains a subset whose product with n is a square; t n = 0 if and only if n is itself a square line 41 source
Source documentation
t n is the least T such that {n + 1, …, n + T} contains a subset whose product with n is a square; t n = 0 if and only if n is itself a square.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: InfSet.sInf, Set.ofPred, Exists, Finset, And, LE.le, Finset.Icc, OfNat.ofNat, IsSquare, HMul.hMul, Finset.prod, HAdd.hAdd
12 instances, coercions and auxiliary constants left out.
```
noncomputable def t (n : ℕ) : ℕ :=
…
```
theorem Erdos841.erdos_841 Let $t_n$ be minimal such that $\{n+1,\ldots,n+t_n\}$ contains a subset whose product with $n$ is a square number (and let $t_n=0$ if $n$ is itself square) sorry line 61 source
Source documentation
Let $t_n$ be minimal such that $\{n+1,\ldots,n+t_n\}$ contains a subset whose product with $n$ is a square number (and let $t_n=0$ if $n$ is itself square). Estimate $t_n$.
A problem of Erdős, Graham, and Selfridge. For example, $t_6=6$ since $6\cdot 8\cdot 12=24^2$. It is trivial that $t_n\geq P(n)$, where $P(n)$ is the largest prime divisor of $n$.
Bui, Pratt, and Zaharescu [BPZ24] proved that the distribution of $t_n$ continues to follow $P(n)$, in that for any fixed $c\in (0,1]$ $$\lim_{x\to \infty}\frac{\lvert \{ n\leq x : t_n\leq n^c\}\rvert}{x} = \lim_{x\to \infty}\frac{\lvert \{ n\leq x : P(n)\leq n^c\}\rvert}{x}.$$ The statement below is that the difference of the two counting functions is $o(x)$.
This was formalized in Lean by Codex.

depends on sorry what this means
Statement uses: Real, Membership.mem, Set, Set.Ioc, OfNat.ofNat, Filter.Tendsto, Nat, HDiv.hDiv, HSub.hSub, Finset.card, Finset.filter, LE.le, Erdos841.t, HPow.hPow, Finset.Icc, Nat.maxPrimeFac, Filter.atTop, nhds
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
46 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_841 (c : ℝ) (hc : c ∈ Set.Ioc 0 1) :
    Tendsto (fun x : ℕ ↦
      ((((Finset.Icc 1 x).filter fun n : ℕ ↦ (t n : ℝ) ≤ (n : ℝ) ^ c).card : ℝ) -
        ((Finset.Icc 1 x).filter fun n : ℕ ↦ (n.maxPrimeFac : ℝ) ≤ (n : ℝ) ^ c).card) / x)
      atTop (𝓝 0) := by
…
```
Mentions: c, Erdos841.t
theorem Erdos841.erdos_841.variants.selfridge_large_prime Selfridge proved that $t_n=P(n)$ if $P(n)>\sqrt{2n}+1$ sorry line 74 source
Source documentation
Selfridge proved that $t_n=P(n)$ if $P(n)>\sqrt{2n}+1$.
This was formalized in Lean by Codex.

depends on sorry what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Real, HAdd.hAdd, Real.sqrt, HMul.hMul, Nat.maxPrimeFac, Eq, Erdos841.t
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
28 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_841.variants.selfridge_large_prime (n : ℕ) (hn : 1 < n)
    (h : √(2 * n) + 1 < (n.maxPrimeFac : ℝ)) : t n = n.maxPrimeFac := by
…
```
Mentions: Erdos841.t
theorem Erdos841.erdos_841.variants.selfridge_sqrt Selfridge proved that $t_n \ll n^{1/2}$ if $P(n)\leq\sqrt{2n}+1$ sorry line 84 source
Source documentation
Selfridge proved that $t_n \ll n^{1/2}$ if $P(n)\leq\sqrt{2n}+1$.
This was formalized in Lean by Codex.

depends on sorry what this means
Statement uses: Exists, Real, Nat, LE.le, Nat.maxPrimeFac, HAdd.hAdd, Real.sqrt, HMul.hMul, OfNat.ofNat, Erdos841.t
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
26 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_841.variants.selfridge_sqrt :
    ∃ C : ℝ, ∀ n : ℕ, (n.maxPrimeFac : ℝ) ≤ √(2 * n) + 1 → (t n : ℝ) ≤ C * √n := by
…
```
Mentions: Erdos841.t
theorem Erdos841.erdos_841.variants.many_small_values Bui, Pratt, and Zaharescu [BPZ24] proved that for at least $x^{1-o(1)}$ many $n\leq x$ we have $$t_n \leq \exp(O(\sqrt{\log n\log\log n})).$$ This was formalized in Lean by Codex sorry line 96 source
Source documentation
Bui, Pratt, and Zaharescu [BPZ24] proved that for at least $x^{1-o(1)}$ many $n\leq x$ we have $$t_n \leq \exp(O(\sqrt{\log n\log\log n})).$$
This was formalized in Lean by Codex.

depends on sorry what this means
Statement uses: Exists, Real, Filter.Tendsto, Nat, HDiv.hDiv, Real.log, Finset.card, Finset.filter, LE.le, Erdos841.t, Real.exp, HMul.hMul, Real.sqrt, Finset.Icc, OfNat.ofNat, Filter.atTop, nhds
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
34 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_841.variants.many_small_values : ∃ K : ℝ,
    Tendsto (fun x : ℕ ↦
      log (((Finset.Icc 1 x).filter fun n ↦
        (t n : ℝ) ≤ exp (K * √(log n * log (log n)))).card : ℝ) / log x) atTop (𝓝 1) := by
…
```
Mentions: Erdos841.t
theorem Erdos841.erdos_841.variants.lower_bound Bui, Pratt, and Zaharescu [BPZ24] proved that for all non-square $n$ $$t_n \gg (\log\log n)^{6/5}(\log\log\log n)^{-1/5}.$$ This was formalized in Lean by Codex sorry line 109 source
Source documentation
Bui, Pratt, and Zaharescu [BPZ24] proved that for all non-square $n$ $$t_n \gg (\log\log n)^{6/5}(\log\log\log n)^{-1/5}.$$
This was formalized in Lean by Codex.

depends on sorry what this means
Statement uses: Exists, Real, And, LT.lt, OfNat.ofNat, Filter.Eventually, Nat, Not, IsSquare, LE.le, HMul.hMul, HPow.hPow, Real.log, HDiv.hDiv, Neg.neg, Erdos841.t, 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_841.variants.lower_bound : ∃ C : ℝ, 0 < C ∧
    ∀ᶠ n : ℕ in atTop, ¬ IsSquare n →
      C * (log (log n) ^ ((6 : ℝ) / 5) * log (log (log n)) ^ (-(1 : ℝ) / 5)) ≤ t n := by
…
```
Mentions: Erdos841.t