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

9 declarations, 7 contain sorry, 0 declared as axioms

Erdős Problem 263

Reference: erdosproblems.com/263

Imports (1)

FormalConjecturesUtil

Imported by 1 file

FormalConjectures/Subsets/FC100SolvedSet1.lean

def Erdos263.IsIrrationalitySequence We call a strictly increasing sequence line 46 source
Source documentation
We call a strictly increasing sequence $a_n$ of positive integers an irrationality sequence if for any sequence $b_n$ of positive integers with $\frac{a_n}{b_n} \to 1$ as $n \to \infty$, the sum $\sum \frac{1}{b_n}$ converges to an irrational number.
Note: erdosproblems.com/263 was corrected on 2026-04-02 to require the sequence to be increasing; the pre-correction statement (no monotonicity hypothesis) had a counterexample to Q2 that is not increasing (see erdos_263.parts.ii below).
Note: This is one of many possible notions of "irrationality sequences". See FormalConjectures/ErdosProblems/264.lean for another possible definition.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: And, GT.gt, OfNat.ofNat, StrictMono, Filter.Tendsto, Real, HDiv.hDiv, Filter.atTop, nhds, Irrational, tsum, SummationFilter.unconditional
14 instances, coercions and auxiliary constants left out.
```
def IsIrrationalitySequence (a : ℕ → ℕ) : Prop :=
…
```
def Erdos263.IsWeakIrrationalitySequence Documented declaration: IsWeakIrrationalitySequence line 56 source
Source documentation
The nondecreasing version of IsIrrationalitySequence, as used by Koizumi [Ko25]: the sequence is positive and nondecreasing, and every positive sequence asymptotic to it has irrational reciprocal sum.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: And, GT.gt, OfNat.ofNat, Monotone, Filter.Tendsto, Real, HDiv.hDiv, Filter.atTop, nhds, Irrational, tsum, SummationFilter.unconditional
14 instances, coercions and auxiliary constants left out.
```
def IsWeakIrrationalitySequence (a : ℕ → ℕ) : Prop :=
…
```
theorem Erdos263.erdos_263.parts.i Is $a_n = 2^{2^n}$ an irrationality sequence in the above sense? sorry line 67 source
Source documentation
Is $a_n = 2^{2^n}$ an irrationality sequence in the above sense?

depends on sorry what this means
Statement uses: Iff, True, Erdos263.IsIrrationalitySequence, Nat, HPow.hPow, OfNat.ofNat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
10 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_263.parts.i : answer(sorry) ↔ IsIrrationalitySequence (fun n : ℕ => 2 ^ 2 ^ n) := by
…
```
Mentions: Erdos263.IsIrrationalitySequence
theorem Erdos263.erdos_263.parts.ii Must every irrationality sequence $a_n$ in the above sense satisfy $a_n^{1/n} \to \infty$ as $n \to \infty$? sorry line 82 source
Source documentation
Must every irrationality sequence $a_n$ in the above sense satisfy $a_n^{1/n} \to \infty$ as $n \to \infty$?
Note: this was answered false for the pre-correction statement, which did not require monotonicity — the counterexample sequence is not increasing. The problem was corrected on erdosproblems.com on 2026-04-02 to require increasing sequences; for the corrected statement this question is open. The earlier formal proof (for the pre-correction definition) is preserved at https://github.com/google-deepmind/formal-conjectures/blob/c8cf651906abe91051cf835d4232ad5648412113/FormalConjectures/ErdosProblems/263.lean#L298

depends on sorry what this means
Statement uses: Iff, True, Nat, Erdos263.IsIrrationalitySequence, Filter.Tendsto, Real, HPow.hPow, HDiv.hDiv, OfNat.ofNat, 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_263.parts.ii : answer(sorry) ↔
    ∀ a : ℕ → ℕ,
      IsIrrationalitySequence a →
        atTop.Tendsto (fun n : ℕ => (a n : ℝ) ^ (1 / (n : ℝ))) atTop := by
…
```
Mentions: Erdos263.IsIrrationalitySequence
theorem Erdos263.erdos_263.variants.folklore A folklore result states that any $a_n$ satisfying $\lim_{n \to \infty} a_n^{\frac{1}{2^n}} = \infty$ has $\sum \frac{1}{a_n}$ converging to an irrational number sorry line 93 source
Source documentation
A folklore result states that any $a_n$ satisfying $\lim_{n \to \infty} a_n^{\frac{1}{2^n}} = \infty$ has $\sum \frac{1}{a_n}$ converging to an irrational number.

depends on sorry what this means
Statement uses: Nat, Filter.Tendsto, Real, HPow.hPow, HDiv.hDiv, OfNat.ofNat, Filter.atTop, Irrational, tsum, SummationFilter.unconditional
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_263.variants.folklore (a : ℕ -> ℕ)
    (ha : atTop.Tendsto (fun n : ℕ => (a n : ℝ) ^ (1 / (2 ^ n : ℝ))) atTop) :
    Irrational <| ∑' n, (1 : ℝ) / (a n : ℝ) := by
…
```
theorem Erdos263.erdos_263.variants.sub_doubly_exponential Kovač and Tao [KoTa24] proved that any strictly increasing sequence sorry line 107 source
Source documentation
Kovač and Tao [KoTa24] proved that any strictly increasing sequence $a_n$ such that $\sum \frac{1}{a_n}$ converges and $\lim \frac{a_{n+1}}{a_n^2} = 0$ is not an irrationality sequence in the above sense.
[KoTa24] Kovač, V. and Tao T., On several irrationality problems for Ahmes series. arXiv:2406.17593 (2024).

depends on sorry what this means
Statement uses: Nat, StrictMono, Summable, Real, HDiv.hDiv, OfNat.ofNat, SummationFilter.unconditional, Filter.Tendsto, HAdd.hAdd, HPow.hPow, Filter.atTop, nhds, Not, Erdos263.IsIrrationalitySequence
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
42 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_263.variants.sub_doubly_exponential (a: ℕ -> ℕ)
    (ha' : StrictMono a)
    (ha'' : Summable (fun n : ℕ => 1 / (a n : ℝ)))
    (ha''' : atTop.Tendsto (fun n : ℕ => (a (n + 1) : ℝ) / a n ^ 2) (𝓝 0)) :
    ¬ IsIrrationalitySequence a := by
…
```
Mentions: Erdos263.IsIrrationalitySequence
theorem Erdos263.erdos_263.variants.super_doubly_exponential sorry line 121 source
depends on sorry what this means
Statement uses: Nat, GT.gt, OfNat.ofNat, StrictMono, Exists, Real, And, Filter.liminf, HDiv.hDiv, HAdd.hAdd, HPow.hPow, Filter.atTop, Erdos263.IsIrrationalitySequence
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
42 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem Erdos263.erdos_263.variants.super_doubly_exponential_eventual The same folklore result with the growth hypothesis stated as an eventual lower bound $a_{n+1} \geq c\, a_n^{2+\varepsilon}$ sorry line 137 source
Source documentation
The same folklore result with the growth hypothesis stated as an eventual lower bound $a_{n+1} \geq c\, a_n^{2+\varepsilon}$. Unlike the real-valued liminf in erdos_263.variants.super_doubly_exponential, this form also covers sequences such as $a_n = 2^{(n+1)!}$, for which the ratio $a_{n+1} / a_n^{2+\varepsilon}$ tends to $+\infty$ and the real liminf defaults to $0$.

depends on sorry what this means
Statement uses: Nat, GT.gt, OfNat.ofNat, StrictMono, Exists, Real, And, LT.lt, Filter.Eventually, LE.le, HMul.hMul, HPow.hPow, HAdd.hAdd, Filter.atTop, Erdos263.IsIrrationalitySequence
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_263.variants.super_doubly_exponential_eventual (a : ℕ → ℕ)
    (ha : ∀ n : ℕ, a n > 0)
    (ha' : StrictMono a)
    (ha'' : ∃ ε c : ℝ, 0 < ε ∧ 0 < c ∧
      ∀ᶠ n in atTop, c * (a n : ℝ) ^ (2 + ε) ≤ (a (n + 1) : ℝ)) :
    IsIrrationalitySequence a := by
…
```
Mentions: c, Erdos263.IsIrrationalitySequence
theorem Erdos263.erdos_263.variants.doubly_exponential_all_but_countable Documented declaration: doubly_exponential_all_but_countable sorry line 155 source
Source documentation
Koizumi [Ko25] showed that $a_n = \lfloor \alpha^{2^n} \rfloor$ is an irrationality sequence for all but countably many $\alpha > 1$, in the nondecreasing sense IsWeakIrrationalitySequence. The strictly increasing predicate would fail on the whole interval $1 < \alpha < 4/3$, where $a_0 = a_1 = 1$.
[Ko25] Koizumi, J., Irrationality of the reciprocal sum of doubly exponential sequences, arXiv:2504.05933 (2025).

depends on sorry what this means
Statement uses: Filter.Eventually, Real, GT.gt, OfNat.ofNat, Erdos263.IsWeakIrrationalitySequence, Nat, Nat.floor, HPow.hPow, Filter.cocountable
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
30 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_263.variants.doubly_exponential_all_but_countable :
    ∀ᶠ (α : ℝ) in .cocountable, α > 1 →
      IsWeakIrrationalitySequence (fun n : ℕ => ⌊α ^ 2 ^ n⌋₊) := by
…
```
Mentions: Erdos263.IsWeakIrrationalitySequence