/-
Copyright 2025 The Formal Conjectures Authors.
Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at
https://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/
module
public import FormalConjecturesUtilErdős Problem 263
Reference: erdosproblems.com/263
@[expose] public sectionopen Filteropen scoped Topologynamespace Erdos263We 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.
def IsIrrationalitySequence (a : ℕ → ℕ) : Prop :=
(∀ n : ℕ, a n > 0) ∧
StrictMono a ∧
(∀ b : ℕ → ℕ, (∀ n : ℕ, b n > 0) ∧
atTop.Tendsto (fun n : ℕ => (a n : ℝ) / (b n : ℝ)) (𝓝 1) →
Irrational (∑' n, 1 / (b n : ℝ)))
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.
def IsWeakIrrationalitySequence (a : ℕ → ℕ) : Prop :=
(∀ n : ℕ, a n > 0) ∧
Monotone a ∧
(∀ b : ℕ → ℕ, (∀ n : ℕ, b n > 0) ∧
atTop.Tendsto (fun n : ℕ => (a n : ℝ) / (b n : ℝ)) (𝓝 1) →
Irrational (∑' n, 1 / (b n : ℝ)))Is $a_n = 2^{2^n}$ an irrationality sequence in the above sense?
@[category research open, AMS 11]
theorem erdos_263.parts.i : answer(sorry) ↔ IsIrrationalitySequence (fun n : ℕ => 2 ^ 2 ^ n) := ⊢ True ↔ IsIrrationalitySequence fun n ↦ 2 ^ 2 ^ n
All goals completed! 🐙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
@[category research open, AMS 11]
theorem erdos_263.parts.ii : answer(sorry) ↔
∀ a : ℕ → ℕ,
IsIrrationalitySequence a →
atTop.Tendsto (fun n : ℕ => (a n : ℝ) ^ (1 / (n : ℝ))) atTop := ⊢ True ↔ ∀ (a : ℕ → ℕ), IsIrrationalitySequence a → Tendsto (fun n ↦ ↑(a n) ^ (1 / ↑n)) atTop atTop
All goals completed! 🐙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.
@[category research solved, AMS 11]
theorem erdos_263.variants.folklore (a : ℕ -> ℕ)
(ha : atTop.Tendsto (fun n : ℕ => (a n : ℝ) ^ (1 / (2 ^ n : ℝ))) atTop) :
Irrational <| ∑' n, (1 : ℝ) / (a n : ℝ) := a:ℕ → ℕha:Tendsto (fun n ↦ ↑(a n) ^ (1 / 2 ^ n)) atTop atTop⊢ Irrational (∑' (n : ℕ), 1 / ↑(a n))
All goals completed! 🐙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).
@[category research solved, AMS 11]
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 := a:ℕ → ℕha':StrictMono aha'':Summable fun n ↦ 1 / ↑(a n)ha''':Tendsto (fun n ↦ ↑(a (n + 1)) / ↑(a n) ^ 2) atTop (𝓝 0)⊢ ¬IsIrrationalitySequence a
All goals completed! 🐙
On the other hand, if there exists some $\varepsilon > 0$ such that $a_n$ satisfies
$\liminf \frac{a_{n+1}}{a_n^{2+\varepsilon}} > 0$, then $a_n$ is an irrationality sequence
by the above folklore result erdos_263.variants.folklore.
@[category research solved, AMS 11,
formal_proof using lean4 at "https://github.com/arex1337/erdos-263-lean/blob/95de79a5cd49050df80e95be6cfc161580830799/Erdos263/Folklore.lean#L700"]
theorem erdos_263.variants.super_doubly_exponential (a: ℕ -> ℕ)
(ha : ∀ n : ℕ, a n > 0)
(ha' : StrictMono a)
(ha'' : ∃ ε : ℝ, ε > 0 ∧
Filter.atTop.liminf (fun n : ℕ => (a (n + 1) : ℝ) / a n ^ (2 + ε)) > 0) :
IsIrrationalitySequence a := a:ℕ → ℕha:∀ (n : ℕ), a n > 0ha':StrictMono aha'':∃ ε > 0, liminf (fun n ↦ ↑(a (n + 1)) / ↑(a n) ^ (2 + ε)) atTop > 0⊢ IsIrrationalitySequence a
All goals completed! 🐙
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$.
@[category research solved, AMS 11]
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 := a:ℕ → ℕha:∀ (n : ℕ), a n > 0ha':StrictMono aha'':∃ ε c, 0 < ε ∧ 0 < c ∧ ∀ᶠ (n : ℕ) in atTop, c * ↑(a n) ^ (2 + ε) ≤ ↑(a (n + 1))⊢ IsIrrationalitySequence a
All goals completed! 🐙
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).
@[category research solved, AMS 11]
theorem erdos_263.variants.doubly_exponential_all_but_countable :
∀ᶠ (α : ℝ) in .cocountable, α > 1 →
IsWeakIrrationalitySequence (fun n : ℕ => ⌊α ^ 2 ^ n⌋₊) := ⊢ ∀ᶠ (α : ℝ) in cocountable, α > 1 → IsWeakIrrationalitySequence fun n ↦ ⌊α ^ 2 ^ n⌋₊
All goals completed! 🐙end Erdos263