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

10 declarations, 6 contain sorry, 0 declared as axioms

Erdős Problem 291

References:

erdosproblems.com/291
[ErGr80, p.34] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathematique (1980).
[Sh16] P. Shiu, The denominators of harmonic numbers. arXiv:1607.02863 (2016).
[WuYa22] Wu, Bing-Ling and Yan, Xiao-Hui, On the denominators of harmonic numbers. {IV}. C. R. Math. Acad. Sci. Paris (2022), 53--57.

Imports (1)

FormalConjecturesUtil

def Erdos291.L $L_n$ is the least common multiple of $\{1,\ldots,n\}$ line 41 source
Source documentation
$L_n$ is the least common multiple of $\{1,\ldots,n\}$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: Finset.lcm, Finset.Icc, OfNat.ofNat
6 instances, coercions and auxiliary constants left out.
```
def L (n : ℕ) : ℕ :=
…
```
theorem Erdos291.L_eval line 45 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: And, Eq, Nat, Erdos291.L, OfNat.ofNat
Proof uses: of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl
4 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
def Erdos291.a $a_n$ is defined by $\sum_{1\leq k\leq n}\frac{1}{k}=\frac{a_n}{L_n}$ line 50 source
Source documentation
$a_n$ is defined by $\sum_{1\leq k\leq n}\frac{1}{k}=\frac{a_n}{L_n}$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: Finset.sum, Finset.Icc, OfNat.ofNat, HDiv.hDiv, Erdos291.L
6 instances, coercions and auxiliary constants left out.
```
def a (n : ℕ) : ℕ :=
…
```
theorem Erdos291.a_eval line 54 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: And, Eq, Nat, Erdos291.a, OfNat.ofNat
Proof uses: of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl
4 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem Erdos291.erdos_291.parts.i Let $n\geq 1$ and define $L_n$ to be the least common multiple of $\{1,\ldots,n\}$ and $a_n$ by $\sum_{1\leq k\leq n}\frac{1}{k}=\frac{a_n}{L_n}$ sorry line 63 source
Source documentation
Let $n\geq 1$ and define $L_n$ to be the least common multiple of $\{1,\ldots,n\}$ and $a_n$ by $\sum_{1\leq k\leq n}\frac{1}{k}=\frac{a_n}{L_n}$.
Is it true that $(a_n,L_n)=1$ occurs for infinitely many $n$?

depends on sorry what this means
Statement uses: Iff, True, Set.Infinite, Nat, Set.ofPred, Eq, Nat.gcd, Erdos291.a, Erdos291.L, OfNat.ofNat
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 erdos_291.parts.i :
    answer(sorry) ↔
      { n : ℕ | Nat.gcd (a n) (L n) = 1 }.Infinite := by
…
```
Mentions: Erdos291.a, Erdos291.L
theorem Erdos291.erdos_291.parts.ii Is it true that $(a_n,L_n)>1$ occurs for infinitely many $n$? sorry line 75 source
Source documentation
Is it true that $(a_n,L_n)>1$ occurs for infinitely many $n$?
Steinerberger has observed that the answer to the second question is trivially yes: for example, any $n$ which begins with a $2$ in base $3$ has $3\mid (a_n,L_n)$.

depends on sorry what this means
Statement uses: Iff, True, Set.Infinite, Nat, Set.ofPred, GT.gt, Nat.gcd, Erdos291.a, Erdos291.L, OfNat.ofNat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
4 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_291.parts.ii :
    answer(True) ↔
      { n : ℕ | Nat.gcd (a n) (L n) > 1 }.Infinite := by
…
```
Mentions: Erdos291.a, Erdos291.L
theorem Erdos291.erdos_291.variants.steinerberger_generalization More generally, if the leading digit of $n$ in base $p$ is $p-1$ then $p\mid (a_n,L_n)$ sorry line 89 source
Source documentation
More generally, if the leading digit of $n$ in base $p$ is $p-1$ then $p\mid (a_n,L_n)$. There is in fact a necessary and sufficient condition: a prime $p\leq n$ divides $(a_n,L_n)$ if and only if $p$ divides the numerator of $1+\cdots+\frac{1}{k}$, where $k$ is the leading digit of $n$ in base $p$. This can be seen by writing $a_n = \frac{L_n}{1}+\cdots+\frac{L_n}{n}$ and observing that the right-hand side is congruent to $1+\cdots+1/k$ modulo $p$. (The previous claim about $p-1$ follows immediately from Wolstenholme's theorem.)

depends on sorry what this means
Statement uses: Nat, Nat.Prime, LE.le, HDiv.hDiv, HPow.hPow, Nat.log, Iff, Dvd.dvd, Nat.gcd, Erdos291.a, Erdos291.L, Int, Rat.num, Finset.sum, Rat, Finset.Icc, OfNat.ofNat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
36 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_291.variants.steinerberger_generalization (n p : ℕ) (hp : p.Prime) (hpn : p ≤ n) :
    let k := n / p ^ Nat.log p n;
…
```
theorem Erdos291.erdos_291.variants.shiu_heuristic_asymptotic This leads to a heuristic prediction (see for example a preprint of Shiu [Sh16]) of $\asymp\frac{x}{\log x}$ for the number of $n\in [1,x]$ such that $(a_n,L_n)=1$ sorry line 99 source
Source documentation
This leads to a heuristic prediction (see for example a preprint of Shiu [Sh16]) of $\asymp\frac{x}{\log x}$ for the number of $n\in [1,x]$ such that $(a_n,L_n)=1$.

depends on sorry what this means
Statement uses: Asymptotics.IsTheta, Nat, Real, Filter.atTop, Finset.card, Finset.filter, Eq, Nat.gcd, Erdos291.a, Erdos291.L, OfNat.ofNat, Finset.Icc, HDiv.hDiv, Real.log
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
20 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_291.variants.shiu_heuristic_asymptotic :
    Asymptotics.IsTheta atTop
      (fun x : ℕ ↦ ((((Finset.Icc 1 x).filter (fun n ↦ Nat.gcd (a n) (L n) = 1)).card : ℝ)))
      (fun x : ℕ ↦ (x : ℝ) / Real.log x) := by
…
```
Mentions: Erdos291.a, Erdos291.L
theorem Erdos291.erdos_291.variants.shiu_heuristic_density_zero In particular, there should be infinitely many $n$, but the set of such $n$ should have density zero sorry line 110 source
Source documentation
In particular, there should be infinitely many $n$, but the set of such $n$ should have density zero. Unfortunately this heuristic is difficult to turn into a proof.

depends on sorry what this means
Statement uses: Filter.Tendsto, Nat, Real, HDiv.hDiv, Finset.card, Finset.filter, Eq, Nat.gcd, Erdos291.a, Erdos291.L, OfNat.ofNat, Finset.Icc, Filter.atTop, nhds
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_291.variants.shiu_heuristic_density_zero :
    Filter.Tendsto (fun N : ℕ ↦
      ((((Finset.Icc 1 N).filter (fun n ↦ Nat.gcd (a n) (L n) = 1)).card : ℝ) / (N : ℝ)))
      atTop (nhds 0) := by
…
```
Mentions: Erdos291.a, Erdos291.L
theorem Erdos291.erdos_291.variants.wu_yan Documented declaration: wu_yan sorry line 122 source
Source documentation
Wu and Yan [WuYa22] have proved, conditional on $\frac{1}{\log p}$ being linearly independent over $\mathbb{Q}$ for any finite collection of primes $p$ (itself a consequence of Schanuel's conjecture), that the set of $n$ for which $(a_n,L_n)>1$ has upper density $1$.

depends on sorry what this means
Statement uses: LinearIndependent, Subtype, Nat, Nat.Prime, Rat, Real, HDiv.hDiv, OfNat.ofNat, Real.log, Eq, EReal, Filter.limsup, Finset.card, Finset.filter, GT.gt, Nat.gcd, Erdos291.a, Erdos291.L, Finset.Icc, Filter.atTop
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
90 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_291.variants.wu_yan
    (h_indep : LinearIndependent ℚ (fun p : {p : ℕ // p.Prime} ↦ 1 / Real.log (p : ℝ))) :
    atTop.limsup (fun N : ℕ ↦
      ((((Finset.Icc 1 N).filter (fun n ↦ Nat.gcd (a n) (L n) > 1)).card : ℝ) /
        (N : ℝ) : EReal)) = 1 := by
…
```
Mentions: Erdos291.a, Erdos291.L