252.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, 9 contain sorry, 0 declared as axioms

Erdős Problem 252

References:

erdosproblems.com/252
[ErSt71] Erdös, P., and E. G. Straus. "Some number theoretic results." Pacific J. Math 36 (1971): 635-646.
[ErSt74] Erdős, Paul, and Ernst Straus. "On the irrationality of certain series." Pacific journal of mathematics 55.1 (1974): 85-92.
[ErKa54] P. Erdős, M. Kac, Amer. Math. Monthly 61 (1954), Problem 4518.
[ScPu06] Schlage-Puchta, J. C., The irrationality of a number theoretical series. Ramanujan J. (2006), 455-460.
[FLC07] Friedlander, J. B. and Luca, F. and Stoiciu, M., On the irrationality of a divisor function series. Integers (2007).
[Pr22] Pratt, K., The irrationality of a divisor function series of Erdős and Kac. arXiv:2209.11124 (2022).

Imports (2)

def Erdos252.erdos_252_sum The series ∑ σ k n / n! line 47 source
Source documentation
The series ∑ σ k n / n!.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real
Proof uses: tsum, HDiv.hDiv, ArithmeticFunction, ArithmeticFunction.sigma, Nat.factorial, SummationFilter.unconditional
13 instances, coercions and auxiliary constants left out.
```
noncomputable def erdos_252_sum (k : ℕ) : ℝ := ∑' n, σ k n / (n ! : ℝ)
…
```
theorem Erdos252.erdos_252 Erdős Problem 252: irrationality of the sum for a given $k$ sorry line 51 source
Source documentation
Erdős Problem 252: irrationality of the sum for a given $k$.

depends on sorry what this means
Statement uses: Iff, True, Nat, GE.ge, OfNat.ofNat, Irrational, Erdos252.erdos_252_sum
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_252 :
    answer(sorry) ↔ ∀ k ≥ 1, Irrational (erdos_252_sum k) := by
…
```
Mentions: Erdos252.erdos_252_sum
theorem Erdos252.erdos_252.variants.k_eq_zero ∑ σ 0 n / n! is irrational sorry line 57 source
Source documentation
∑ σ 0 n / n! is irrational. This is proved in [ErSt71].

depends on sorry what this means
Statement uses: Irrational, Erdos252.erdos_252_sum, 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 erdos_252.variants.k_eq_zero : Irrational (erdos_252_sum 0) := by
…
```
Mentions: Erdos252.erdos_252_sum
theorem Erdos252.erdos_252.variants.k_eq_one ∑ σ 1 n / n! is irrational sorry line 62 source
Source documentation
∑ σ 1 n / n! is irrational. This is proved in [ErSt74].

depends on sorry what this means
Statement uses: Irrational, Erdos252.erdos_252_sum, 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 erdos_252.variants.k_eq_one : Irrational (erdos_252_sum 1) := by
…
```
Mentions: Erdos252.erdos_252_sum
theorem Erdos252.erdos_252.variants.k_eq_two ∑ σ 2 n / n! is irrational sorry line 68 source
Source documentation
∑ σ 2 n / n! is irrational. This is proved in [ErKa54].

depends on sorry what this means
Statement uses: Irrational, Erdos252.erdos_252_sum, 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 erdos_252.variants.k_eq_two : Irrational (erdos_252_sum 2) := by
…
```
Mentions: Erdos252.erdos_252_sum
theorem Erdos252.erdos_252.variants.k_eq_three ∑ σ 3 n / n! is irrational sorry line 73 source
Source documentation
∑ σ 3 n / n! is irrational. This is proved in [ScPu06] and [FLC07].

depends on sorry what this means
Statement uses: Irrational, Erdos252.erdos_252_sum, 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 erdos_252.variants.k_eq_three : Irrational (erdos_252_sum 3) := by
…
```
Mentions: Erdos252.erdos_252_sum
theorem Erdos252.erdos_252.variants.k_eq_four ∑ σ 4 n / n! is irrational sorry line 78 source
Source documentation
∑ σ 4 n / n! is irrational. This is proved in [Pr22].

depends on sorry what this means
Statement uses: Irrational, Erdos252.erdos_252_sum, 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 erdos_252.variants.k_eq_four : Irrational (erdos_252_sum 4) := by
…
```
Mentions: Erdos252.erdos_252_sum
theorem Erdos252.erdos_252.variants.k_ge_five For a fixed k ≥ 5, is ∑ σ k n / n! irrational? sorry line 83 source
Source documentation
For a fixed k ≥ 5, is ∑ σ k n / n! irrational?.

depends on sorry what this means
Statement uses: Iff, True, Nat, GE.ge, OfNat.ofNat, Irrational, Erdos252.erdos_252_sum
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_252.variants.k_ge_five :
    answer(sorry) ↔ ∀ k ≥ 5, Irrational (erdos_252_sum k) := by
…
```
Mentions: Erdos252.erdos_252_sum
theorem Erdos252.erdos_252.variants.schinzel If Schinzel's conjecture is true, then ∑ σ k n / n! is irrational for all k sorry line 90 source
Source documentation
If Schinzel's conjecture is true, then ∑ σ k n / n! is irrational for all k. This is proved in [ScPu06].

depends on sorry what this means
Statement uses: Finset, Polynomial, Int, Membership.mem, BunyakovskyCondition, SchinzelCondition, Infinite, Set.ofPred, Prime, Nat, Int.natAbs, Polynomial.eval, Irrational, Erdos252.erdos_252_sum
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat
11 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_252.variants.schinzel (hs : ∀ (fs : Finset (Polynomial ℤ)),
    (∀ f ∈ fs, BunyakovskyCondition f) → SchinzelCondition fs →
    Infinite ↑{n | ∀ f ∈ fs, Prime (Polynomial.eval (↑n) f).natAbs}) :
    ∀ k, Irrational (erdos_252_sum k) := by
…
```
Mentions: BunyakovskyCondition, SchinzelCondition, Erdos252.erdos_252_sum
theorem Erdos252.erdos_252.variants.prime_tuples If the prime k-tuples conjecture is true, then ∑ σ k n / n! is irrational sorry line 99 source
Source documentation
If the prime k-tuples conjecture is true, then ∑ σ k n / n! is irrational. This is proved in [FLC07].

depends on sorry what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Fin, PNat, Nat.Prime, Exists, Not, Dvd.dvd, Finset.prod, Finset.univ, HAdd.hAdd, HMul.hMul, Set.Infinite, Set.ofPred, Irrational, Erdos252.erdos_252_sum
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_252.variants.prime_tuples {k : ℕ} (hk : 4 ≤ k) (hp : ∀ (a : Fin k → ℕ+)
    (b : Fin k → ℕ) (hab : ∀ p, p.Prime → ∃ n, ¬ p ∣ ∏ i, (a i * n + b i)),
    Set.Infinite {n | ∀ i : Fin k, (a i * n + b i).Prime} ) :
    Irrational (erdos_252_sum k) := by
…
```
Mentions: Erdos252.erdos_252_sum