Erdős Problem 245 to Erdős Problem 268

TheoremErdős Problem 245#

Reference: erdosproblems.com/245

Quoted from FormalConjectures/ErdosProblems/245.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The problem's page on erdosproblems.com: https://www.erdosproblems.com/245.

The file states 2 research or textbook statements: 2 solved.

Erdos245.erdos_245

Solved: stated here without proof.

Let \(A\subseteq\mathbb{N}\) be an infinite set such that \(|A\cap \{1, ..., N\}| = o(N)\). Is it true that

\[ \limsup_{N\to\infty}\frac{|(A + A)\cap \{1, ..., N\}|}{|A \cap \{1, ..., N\}|} \geq 3? \]

The answer is yes, proved by Freiman [Fr73].

[Fr73] Fre\u{\i}man, G. A., Foundations of a structural theory of set addition. (1973), vii+108.

theorem erdos_245 :
    ∀ (A : Set ℕ), A.Infinite →
      atTop.Tendsto (fun N ↦ (A ∩ Icc 1 ⌊N⌋₊ |>.ncard : ℝ) / N) (𝓝 0) →
      3 ≤ atTop.limsup
        fun N : ℝ ↦ ((A + A) ∩ Icc 1 ⌊N⌋₊ |>.ncard : EReal)
          / (A ∩ Icc 1 ⌊N⌋₊).ncard

Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/245.lean, line 46.

Erdos245.erdos_245.variants.two

Solved: stated here without proof.

Let \(A\subseteq\mathbb{N}\) be an infinite set such that \(|A\cap \{1, ..., N\}| = o(N)\). Then

\[ \limsup_{N\to\infty}\frac{|(A + A)\cap \{1, ..., N\}|}{|A \cap \{1, ..., N\}|} \geq 2. \]
theorem erdos_245.variants.two (A : Set ℕ) (h_inf : A.Infinite)
    (hf : atTop.Tendsto (fun N ↦ (A ∩ Icc 1 ⌊N⌋₊ |>.ncard : ℝ) / N) (𝓝 0)) :
    2 ≤ atTop.limsup
      fun N : ℝ ↦ ((A + A) ∩ Icc 1 ⌊N⌋₊ |>.ncard : EReal)
        / (A ∩ Icc 1 ⌊N⌋₊).ncard

Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/245.lean, line 62.

Sources
LeanErdos245.erdos_245 · Erdos245.erdos_245.variants.two

TheoremErdős Problem 246#

References: - erdosproblems.com/246 - [Bi59] Birch, B. J., Note on a problem of Erd\H{o}s. Proc. Cambridge Philos. Soc. (1959), 370-373. - [Ca60] Cassels, J. W. S., On the representation of integers as the sums of distinct summands taken from a fixed set. Acta Sci. Math. (Szeged) (1960), 111-124. - [FaCh17] Fang, Jin-Hui and Chen, Yong-Gao, A quantitative form of the {E}rd\H{o}s-{B}irch theorem. Acta Arith. (2017), 301--311. - [He00b] Hegyv\'{a}ri, N., On the completeness of an exponential type sequence. Acta Math. Hungar. (2000), 127--135. - [Yu24] Yu, Wang-Xing, On the representation of an exponential type sequence. Publ. Math. Debrecen (2024), 253--261.

Quoted from FormalConjectures/ErdosProblems/246.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The problem's page on erdosproblems.com: https://www.erdosproblems.com/246.

The file states 1 research or textbook statement: 1 solved.

Erdos246.erdos_246

Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/main/src/v4.29.1/ErdosProblems/Erdos246.lean.

Let \((a,b)=1\). The set \(\{a^kb^l: k,l\geq 0\}\) is complete - that is, every large integer is the sum of distinct integers of the form \(a^kb^l\) with \(k,l\geq 0\).

We state the nontrivial case \(a,b\geq 2\), proved by Birch [Bi59].

theorem erdos_246 (a b : ℕ) (ha : 2 ≤ a) (hb : 2 ≤ b) (hab : Nat.Coprime a b) :
    IsAddComplete (Gamma a b)

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/246.lean, line 54.

Sources
LeanErdos246.erdos_246

TheoremErdős Problem 247#

Reference: erdosproblems.com/247

Quoted from FormalConjectures/ErdosProblems/247.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The problem's page on erdosproblems.com: https://www.erdosproblems.com/247.

The file states 2 research or textbook statements: 1 open and 1 solved.

Erdos247.erdos_247

Open: stated without proof.

Let \(n_1 < n_2 < \cdots\) be a sequence of integers such that

\[ \limsup \frac{n_k}{k} = \infty. \]

Is

\[ \sum_{k=1}^{\infty} \frac{1}{2^{n_k}} \]

transcendental?

theorem erdos_247 : ∀ (n : ℕ → ℕ), (StrictMono n) →
    atTop.limsup (fun k => (n k / k.succ : EReal)) = ⊤ →
    Transcendental ℚ (∑' k, (1 : ℝ) / 2 ^ n k)

Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/247.lean, line 44.

Erdos247.erdos_247.variants.strong_condition

Solved: stated here without proof.

Erdős proved the answer is yes under the stronger condition that \(\limsup \frac{n_k}{k^t} = \infty\) for all \(t\geq 1\).

[ErGr80] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathematique (1980).

theorem erdos_247.variants.strong_condition (n : ℕ → ℕ)
    (hn : StrictMono n)
    (h : ∀ t ≥ (1 : ℝ),
      atTop.limsup (fun k => n k / (k.succ : ℝ) ^ t |>.toEReal) = ⊤) :
    Transcendental ℚ (∑' k, (1 : ℝ) / 2 ^ n k)

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/247.lean, line 58.

Sources
LeanErdos247.erdos_247 · Erdos247.erdos_247.variants.strong_condition

TheoremErdős Problem 248#

References: - erdosproblems.com/248 - [TaTe25] T. Tao and J. Teräväinen, Quantitative correlations and some problems on prime factors of consecutive integers. arXiv:2512.01739 (2025).

Quoted from FormalConjectures/ErdosProblems/248.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The problem's page on erdosproblems.com: https://www.erdosproblems.com/248.

The file states 1 research or textbook statement: 1 solved.

Erdos248.erdos_248

Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos248.lean#L47.

Are there infinitely many \(n\) such that \(\omega(n + k) \ll k\) for all \(k \geq 1\)? Here \(\omega(n)\) is the number of distinct prime divisors of \(n\).

theorem erdos_248 : (∃ C > (0 : ℝ), { n | ∀ k ≥ 1, ω (n + k) ≤ C * k }.Infinite)

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/248.lean, line 41.

Sources
LeanErdos248.erdos_248

TheoremErdős Problem 249#

Reference: erdosproblems.com/249

Quoted from FormalConjectures/ErdosProblems/249.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The problem's page on erdosproblems.com: https://www.erdosproblems.com/249.

The file states 1 research or textbook statement: 1 open.

Erdos249.erdos_249

Open: stated without proof.

Is

\[\sum_{n} \frac{\phi(n)}{2^n}\]

irrational? Here \(\phi\) is the Euler totient function.

theorem erdos_249 : Irrational (∑' n : ℕ, (φ n) / (2 ^ n))

Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/249.lean, line 38.

Sources
LeanErdos249.erdos_249

TheoremErdős Problem 250#

Reference: erdosproblems.com/250

Quoted from FormalConjectures/ErdosProblems/250.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The problem's page on erdosproblems.com: https://www.erdosproblems.com/250.

The file states 1 research or textbook statement: 1 solved.

Erdos250.erdos_250

Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos250.lean#L97.

Is

\[ \sum_{n=1}^\infty \frac{\sigma(n)}{2^n} \]

irrational? Here \(\sigma(n)\) is the sum of divisors function.

The answer is yes, as shown by Nesterenko [Ne96].

[Ne96] Nesterenko, Yu V., Modular functions and transcendence questions, Mat. Sb. 187 9 (1996), 1319--1348.

theorem erdos_250  : (∀ x, HasSum (fun (n : ℕ) => σ 1 n / (2 : ℝ) ^ n) x → Irrational x)

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/250.lean, line 47.

Sources
LeanErdos250.erdos_250

TheoremErdős Problem 251#

Reference: erdosproblems.com/251

Quoted from FormalConjectures/ErdosProblems/251.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The problem's page on erdosproblems.com: https://www.erdosproblems.com/251.

The file states 1 research or textbook statement: 1 open.

Erdos251.erdos_251

Open: stated without proof.

Is \(\sum_{n=1}^\infty \frac{p_n}{2^n}\) irrational? Here \(p_n\) is the \(n\)-th prime (\(p_1=2, p_2=3, \dots\)).

theorem erdos_251 : Irrational (∑' n : ℕ, (Nat.nth Nat.Prime n) / (2 ^ n))

Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/251.lean, line 34.

Sources
LeanErdos251.erdos_251

TheoremErdő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).

Quoted from FormalConjectures/ErdosProblems/252.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The problem's page on erdosproblems.com: https://www.erdosproblems.com/252.

The file states 9 research or textbook statements: 2 open and 7 solved.

Erdos252.erdos_252

Open: stated without proof.

Erdős Problem 252: irrationality of the sum for a given \(k\).

theorem erdos_252 :
    ∀ k ≥ 1, Irrational (erdos_252_sum k)

Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/252.lean, line 51.

Erdos252.erdos_252.variants.k_eq_zero

Solved: stated here without proof.

∑ σ 0 n / n! is irrational. This is proved in [ErSt71].

theorem erdos_252.variants.k_eq_zero : Irrational (erdos_252_sum 0)

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/252.lean, line 57.

Erdos252.erdos_252.variants.k_eq_one

Solved: stated here without proof.

∑ σ 1 n / n! is irrational. This is proved in [ErSt74].

theorem erdos_252.variants.k_eq_one : Irrational (erdos_252_sum 1)

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/252.lean, line 62.

Erdos252.erdos_252.variants.k_eq_two

Solved: stated here without proof.

∑ σ 2 n / n! is irrational. This is proved in [ErKa54].

theorem erdos_252.variants.k_eq_two : Irrational (erdos_252_sum 2)

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/252.lean, line 68.

Erdos252.erdos_252.variants.k_eq_three

Solved: stated here without proof.

∑ σ 3 n / n! is irrational. This is proved in [ScPu06] and [FLC07].

theorem erdos_252.variants.k_eq_three : Irrational (erdos_252_sum 3)

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/252.lean, line 73.

Erdos252.erdos_252.variants.k_eq_four

Solved: stated here without proof.

∑ σ 4 n / n! is irrational. This is proved in [Pr22].

theorem erdos_252.variants.k_eq_four : Irrational (erdos_252_sum 4)

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/252.lean, line 78.

Erdos252.erdos_252.variants.k_ge_five

Open: stated without proof.

For a fixed k ≥ 5, is ∑ σ k n / n! irrational?.

theorem erdos_252.variants.k_ge_five :
    ∀ k ≥ 5, Irrational (erdos_252_sum k)

Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/252.lean, line 83.

Erdos252.erdos_252.variants.schinzel

Solved: stated here without proof.

If Schinzel's conjecture is true, then ∑ σ k n / n! is irrational for all k. This is proved in [ScPu06].

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)

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/252.lean, line 90.

Erdos252.erdos_252.variants.prime_tuples

Solved: stated here without proof.

If the prime k-tuples conjecture is true, then ∑ σ k n / n! is irrational. This is proved in [FLC07].

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)

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/252.lean, line 99.

Sources
LeanErdos252.erdos_252 · Erdos252.erdos_252.variants.k_eq_zero · Erdos252.erdos_252.variants.k_eq_one · Erdos252.erdos_252.variants.k_eq_two · Erdos252.erdos_252.variants.k_eq_three · Erdos252.erdos_252.variants.k_eq_four · Erdos252.erdos_252.variants.k_ge_five · Erdos252.erdos_252.variants.schinzel · Erdos252.erdos_252.variants.prime_tuples

TheoremErdős Problem 253#

Reference: erdosproblems.com/253

Quoted from FormalConjectures/ErdosProblems/253.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The problem's page on erdosproblems.com: https://www.erdosproblems.com/253.

The file states 1 research or textbook statement: 1 solved.

Erdos253.erdos_253

Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/1268917deaaaa0d674f651287027baa26cea9920/src/latest/ErdosProblems/Erdos253.lean#L699.

Let \(a_1 < a_2 < \dotsc\) be an infinite sequence of positive integers such that \(\frac{a_{i+1}}{a_i} \to 1\). If every arithmetic progression contains infinitely many integers which are the sum of distinct \(a_i\) then every sufficiently large integer is the sum of distinct \(a_i\).

theorem erdos_253 : ¬ ∀ a : ℕ → ℕ, 0 < a 0 →
    RepresentsAPs a → (Filter.atTop.Tendsto (fun n ↦ (a <| n + 1 : ℝ) / a n) (𝓝 1)) →
      subsetSums (Set.range a) ∈ Filter.cofinite

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/253.lean, line 46.

Sources
LeanErdos253.erdos_253

TheoremErdős Problem 254#

References: - erdosproblems.com/254 - [Ca60] Cassels, J. W. S., On the representation of integers as the sums of distinct summands taken from a fixed set. Acta Sci. Math. (Szeged) (1960), 111-124.

Quoted from FormalConjectures/ErdosProblems/254.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The problem's page on erdosproblems.com: https://www.erdosproblems.com/254.

The file states 2 research or textbook statements: 2 solved. It also has 1 API statement, counted here but not shown.

Erdos254.erdos_254

Solved: stated here; a Lean proof is at https://github.com/williamjblair/lean-proofs/blob/4f915a323443bfb1709a6805a013812016dca88a/starfleet/erdos-254/Research/Basic.lean.

Let \(A\subseteq \mathbb{N}\) be such that \(\lvert A\cap [1,2x]\rvert -\lvert A\cap [1,x]\rvert \to \infty\textrm{ as }x\to \infty\) and \(\sum_{n\in A} \{ \theta n\}=\infty\) for every \(\theta\in (0,1)\), where \(\{x\}\) is the distance of \(x\) from the nearest integer. Then every sufficiently large integer is the sum of distinct elements of \(A\).

theorem erdos_254 :
    ∀ (A : Set ℕ),
      (Tendsto (fun x : ℕ ↦ (A ∩ Icc 1 (2 * x)).ncard - (A ∩ Icc 1 x).ncard) atTop atTop) ∧
      (∀ θ : ℝ, 0 < θ → θ < 1 → ¬ Summable (fun n : A ↦ distToNearestInt (θ * (n : ℝ)))) →
        ∀ᶠ m in atTop, IsSumOfDistinct A m

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/254.lean, line 62.

Erdos254.erdos_254.variants.cassels

Solved: stated here without proof.

Cassels [Ca60] proved this under the alternative hypotheses \(\lim \frac{\lvert A\cap [1,2x]\rvert -\lvert A\cap [1,x]\rvert}{\log\log x}=\infty\) and \(\sum_{n\in A} \{ \theta n\}^2=\infty\) for every \(\theta\in (0,1)\).

theorem erdos_254.variants.cassels :
    ∀ (A : Set ℕ),
      (Tendsto (fun x : ℕ ↦ (((A ∩ Icc 1 (2 * x)).ncard : ℝ) -
        ((A ∩ Icc 1 x).ncard : ℝ)) / Real.log (Real.log x)) atTop atTop) ∧
      (∀ θ : ℝ, 0 < θ → θ < 1 → ¬ Summable (fun n : A ↦ (distToNearestInt (θ * (n : ℝ)))^2)) →
        ∀ᶠ m in atTop, IsSumOfDistinct A m

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/254.lean, line 75.

Sources
LeanErdos254.erdos_254 · Erdos254.erdos_254.variants.cassels

TheoremErdős Problem 257#

Reference: erdosproblems.com/257

Quoted from FormalConjectures/ErdosProblems/257.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The problem's page on erdosproblems.com: https://www.erdosproblems.com/257.

The file states 4 research or textbook statements: 1 open, 2 solved and 1 textbook result.

Erdos257.erdos_257

Open: stated without proof.

Let \(A\subseteq\mathbb{N}\) be an infinite set. Is

\[ \sum_{n\in A} \frac{1}{2^n - 1} \]

irrational?

theorem erdos_257 : ∀ (A : Set ℕ), A.Infinite →
    Irrational (∑' n : A, (1 : ℝ) / (2 ^ n.1 - 1))

Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/257.lean, line 38.

Erdos257.erdos_257.variants.tsum_top_eq

Textbook result, proved here.

Show that

\[ \sum_{n} \frac{1}{2^n - 1} = \sum_{n} \frac{d(n)}{2^n}, \]

where \(d(n)\) is the number of divisors of \(n\).

theorem erdos_257.variants.tsum_top_eq :
    ∑' n, 1 / (2 ^ n - 1 : ℝ) = ∑' n, n.divisors.card / (2 ^ n : ℝ)

Category textbook; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/257.lean, line 50.

Erdos257.erdos_257.variants.tsum_top

Solved: stated here; a Lean proof is at https://github.com/wcook04/plectis-erdos-lean/blob/c4eab2571b4692ee9c08d3ec138176f7fbfa09a9/verification/FCMergedIntegerAdapters/research/adapters/FormalConjecturesAdapter.lean#L121-L134.

Show that

\[ \sum_{n} \frac{d(n)}{2^n} \]

is irrational.

[Er48] Erdős, P., On arithmetical properties of Lambert series. J. Indian Math. Soc. (N.S.) (1948), 63-66.

theorem erdos_257.variants.tsum_top :
    Irrational <| ∑' n, n.divisors.card / (2 ^ n : ℝ)

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/257.lean, line 101.

Erdos257.erdos_257.variants.summable_reciprocal_support

Solved: stated here; a Lean proof is at https://github.com/wcook04/plectis-erdos-lean/blob/ec92e5ce12c6117a24e4b532ea565ba332a1df7b/verification/FC257ReciprocalSupport/verification/Solutions/FC257Subtype.lean#L10-L17.

Let \(A \subseteq \mathbb{N}\) be infinite with \(\sum_{a \in A} 1/a < \infty\). For every integer base \(b \ge 2\), the series

\[ \sum_{a \in A} \frac{1}{b^a - 1} \]

is irrational. No pairwise coprimality assumption is needed. Exponent zero contributes zero under Lean's real-division convention.

Erdős stated the coprimality-free result in On the irrationality of certain series, Math. Student 36 (1968), p. 222. A proof and formalisation appear in W. Cook, Reciprocal Mersenne Subseries: https://github.com/wcook04/plectis-erdos/blob/598cd7bac8b73dcfef3687f46922c1ef6da766ae/docs/papers/full-text/erdos257-mersenne-reasoning-surface.md

theorem erdos_257.variants.summable_reciprocal_support
    (b : ℕ) (A : Set ℕ) (hb : 2 ≤ b) (hA : A.Infinite)
    (hsum : Summable fun a : A => 1 / (a : ℝ)) :
    Irrational (∑' n : A, 1 / ((b : ℝ) ^ (n : ℕ) - 1))

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/257.lean, line 123.

Sources
LeanErdos257.erdos_257 · Erdos257.erdos_257.variants.tsum_top_eq · Erdos257.erdos_257.variants.tsum_top · Erdos257.erdos_257.variants.summable_reciprocal_support

TheoremErdős Problem 258#

References: - erdosproblems.com/258 - [Ch26] P. Chojecki and GPT-5.4 Pro, Erdős problem 258 (2026) - [St26] ster-oc, Lean formalisation of Erdős problem 258 (2026)

Quoted from FormalConjectures/ErdosProblems/258.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The problem's page on erdosproblems.com: https://www.erdosproblems.com/258.

The file states 3 research or textbook statements: 3 solved.

Erdos258.erdos_258

Solved: stated here; a Lean proof is at https://gist.githubusercontent.com/ster-oc/2b7adcf9d753cf6e29d782f7374cc57e/raw/689a8483895cbe147634dfbf2d7b1db93a3b5b5f/Erdos258.lean.

Let \(a_n \to \infty\) be a sequence of non-zero natural numbers. Is \(\sum_n \frac{d(n)}{(a_1 ... a_n)}\) irrational, where \(d(n)\) is the number of divisors of \(n\)?

This was proved affirmatively by Chojecki and GPT-5.4 Pro [Ch26], and formalised in Lean by ster-oc [St26].

theorem erdos_258 : ∀ (a : ℕ → ℕ), (∀ n, 2 ≤ a n) →
    Filter.Tendsto a Filter.atTop Filter.atTop →
    Irrational (∑' (n : ℕ), ((n + 1).divisors.card / ∏ i ∈ Finset.Icc 1 (n + 1), a i))

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/258.lean, line 43.

Erdos258.erdos_258.variants.monotone

Solved: stated here without proof.

Let \(2 \leq a_1 \leq a_2 \leq \cdots\) be a monotone sequence with \(a_n \to \infty\). Is \(\sum_n \frac{d(n)}{a_1 \cdots a_n}\) irrational, where \(d(n)\) is the number of divisors of \(n\)?

Solution: True (proved by Erdős and Straus [ErSt71], Lemma 2.2 and Theorem 2.13).

theorem erdos_258.variants.monotone :
    ∀ (a : ℕ → ℕ), (∀ n, 2 ≤ a n) → Monotone a →
    Filter.Tendsto a Filter.atTop Filter.atTop →
    Irrational (∑' (n : ℕ), ((n + 1).divisors.card / ∏ i ∈ Finset.Icc 1 (n + 1), a i))

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/258.lean, line 56.

Erdos258.erdos_258.variants.constant

Solved: stated here; a Lean proof is at https://github.com/wcook04/plectis-erdos-lean/blob/c4eab2571b4692ee9c08d3ec138176f7fbfa09a9/verification/FCMergedIntegerAdapters/research/adapters/FormalConjecturesAdapter.lean#L112-L117.

Is \(\sum_n \frac{d(n)}{t^n}\) irrational, where \(t ≥ 2\) is an integer.

Solution: True (proved by Erdős, see Erdős Problems website)

theorem erdos_258.variants.constant : ∀ t ≥ (2 : ℕ),
    Irrational (∑' (n : ℕ), ((n + 1).divisors.card / t^(n + 1)))

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/258.lean, line 71.

Sources
LeanErdos258.erdos_258 · Erdos258.erdos_258.variants.monotone · Erdos258.erdos_258.variants.constant

TheoremErdős Problem 259#

Reference: erdosproblems.com/259

Quoted from FormalConjectures/ErdosProblems/259.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The problem's page on erdosproblems.com: https://www.erdosproblems.com/259.

The file states 1 research or textbook statement: 1 solved.

Erdos259.erdos_259

Solved: stated here; a Lean proof is at https://gist.githubusercontent.com/ster-oc/c7429943f6b3a634797dc8b2a3b01f2d/raw/8c6b5b7f08021f0aed2312542dd2e9ee7beaa6d6/Erdos259.lean.

Is \(\sum_{n} \mu(n)^2\frac{n}{2^n}\) irrational?

This is true, and was proved by Chen and Ruzsa.

[ChRu99] Chen, Yong-Gao and Ruzsa, Imre Z., On the irrationality of certain series. Period. Math. Hungar. (1999), 31--37.

theorem erdos_259 : Irrational (∑' n : ℕ, (μ n) ^ 2 * n / (2 ^ n))

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/259.lean, line 41.

Sources
LeanErdos259.erdos_259

TheoremErdős Problem 260#

References: - erdosproblems.com/260 - [Wang, Sparse Polynomial-Weighted Expansions] (https://arxiv.org/abs/2606.24972)

Quoted from FormalConjectures/ErdosProblems/260.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The problem's page on erdosproblems.com: https://www.erdosproblems.com/260.

The file states 1 research or textbook statement: 1 solved.

Erdos260.erdos_260

Solved: stated here; a Lean proof is at https://github.com/Hanziwww/erdos260/blob/1f2baf4547f2c2805cdd160611b0b983f43941aa/Erdos260/DeepMind.lean#L92-L132.

Let \(a_1 < a_2 < \cdots\) be an increasing sequence such that \(\frac{a_n}{n} \to \infty\). Is the sum \(\sum_{n}^{\infty} \frac{a_n}{2^{a_n}}\) irrational?

For a proof, see [Wang, Sparse Polynomial-Weighted Expansions] (https://arxiv.org/abs/2606.24972).

theorem erdos_260 :
                  ∀ a : ℕ → ℤ, ∀ s : ℝ,
                  StrictMono a →
                  Tendsto (fun n => (a n : ℝ ) / n ) atTop atTop →
                  HasSum (fun n => (a n : ℝ ) / 2 ^ a n) s → Irrational s

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/260.lean, line 45.

Sources
LeanErdos260.erdos_260

TheoremErdős Problem 261#

References: - erdosproblems.com/261 - [BoLo90] Borwein, Peter and Loring, Terry A., Some questions of Erdős and Graham on numbers of the form \(\sum g_n/2^{g_n}\). Math. Comp. (1990), 377--394. - [Er88c] Erdős, P., On the irrationality of certain series: problems and results. New advances in transcendence theory (Durham, 1986) (1988), 102--109. - [TUZ20] Tengely, Szabolcs and Ulas, Maciej and Zygadlo, Jakub, On a Diophantine equation of Erdős and Graham. J. Number Theory (2020), 445--459. - PALOMAR-2026-10-11-000016

Quoted from FormalConjectures/ErdosProblems/261.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The problem's page on erdosproblems.com: https://www.erdosproblems.com/261.

The file states 7 research or textbook statements: 2 open, 3 solved and 2 textbook results.

Erdos261.erdos_261.variants.borwein_loring

Textbook result, stated without proof. A Lean proof is at https://github.com/linrock/math-proofs/blob/b53791ff6294b4b90e3653970367f127a52fd16e/erdos-261/Solution.lean#L73.

For every positive integer \(m\), if \(n = 2^{m+1} - m - 2\), then

\[\frac{n}{2^n} = \sum_{n < k \le n + m} \frac{k}{2^k}.\]

This construction is due to Borwein and Loring [BoLo90].

theorem erdos_261.variants.borwein_loring (m : ℕ) (hm : 0 < m) :
    let n := 2 ^ (m + 1) - m - 2
    n / (2 ^ n : ℚ) = ∑ k ∈ Finset.Ioc n (n + m), k / (2 ^ k : ℚ)

Category textbook; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/261.lean, line 58.

Erdos261.erdos_261.variants.borwein_loring_property

Textbook result, stated without proof. A Lean proof is at https://github.com/linrock/math-proofs/blob/b53791ff6294b4b90e3653970367f127a52fd16e/erdos-261/Solution.lean#L78.

The Borwein--Loring construction gives the required property when \(m \ge 2\). This lower bound ensures that the representation contains at least two terms.

theorem erdos_261.variants.borwein_loring_property (m : ℕ) (hm : 2 ≤ m) :
    Erdos261Prop (2 ^ (m + 1) - m - 2)

Category textbook; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/261.lean, line 66.

Erdos261.erdos_261.parts.i

Solved: stated here; a Lean proof is at https://github.com/anatoliiohorodnyk/lean-fc-proofs/blob/5da9642575b26c2c816a49bcb56b33fed5456619/Proofs/T_Erdos261_erdos_261_parts_i.lean#L102.

Are there infinitely many positive integers \(n\) such that there exist some \(t \ge 2\) and distinct integers \(a_1, \ldots, a_t \ge 1\) satisfying

\[\frac{n}{2^n} = \sum_{1 \le k \le t} \frac{a_k}{2^{a_k}}?\]

In [Er88c], Erdős notes that Cusick had a simple proof that infinitely many such \(n\) exist.

theorem erdos_261.parts.i : {n : ℕ | 0 < n ∧ Erdos261Prop n}.Infinite

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/261.lean, line 77.

Erdos261.erdos_261.variants.le_10000

Solved: stated here; a Lean proof is at https://github.com/linrock/math-proofs/blob/b53791ff6294b4b90e3653970367f127a52fd16e/erdos-261/Solution.lean#L85.

Tengely, Ulas, and Zygadlo [TUZ20] verified that every positive integer \(n \le 10000\) has the required property.

theorem erdos_261.variants.le_10000 {n : ℕ} (hn_pos : 0 < n) (hn : n ≤ 10000) :
    Erdos261Prop n

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/261.lean, line 84.

Erdos261.erdos_261.parts.ii

Open: stated without proof.

Do all positive integers \(n\) have the required property?

theorem erdos_261.parts.ii : ∀ n > 0, Erdos261Prop n

Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/261.lean, line 90.

Erdos261.erdos_261.parts.iii

Open: stated without proof.

Is there a rational number \(x\) such that

\[x = \sum_{k=1}^{\infty} \frac{a_k}{2^{a_k}}\]

has at least \(2^{\aleph_0}\) representations by pairwise distinct positive integers \(a_k\)?

theorem erdos_261.parts.iii : ∃ x : ℚ,
    𝔠 ≤ #{a : ℕ → ℕ | Erdos261InfiniteRepresentation x a}

Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/261.lean, line 97.

Erdos261.erdos_261.variants.two_representations

Solved: stated here; a Lean proof is at https://github.com/g8r-b8/erdos261-lean/blob/976bddf21eafc93ea86a7a1bfd92b847070a6f31/Erdos261.lean#L87.

In [Er88c], Erdős asks the weaker question of whether there exists a rational \(x\) with at least two representations

\[x = \sum_{k=1}^{\infty} \frac{a_k}{2^{a_k}}\]

by pairwise distinct positive integers \(a_k\).

The answer is yes: Z. Rafik (erdosproblems.com forum, 27 Apr 2026) observed that \(4/2^4 = 5/2^5 + 6/2^6\) and \(\sum_{m \ge 1} m/2^m = 2\), so \(7/4\) is represented both by \(\mathbb{N}_{>0} \setminus \{4\}\) and by \(\mathbb{N}_{>0} \setminus \{5, 6\}\). It is generally believed that "two" here is a misprint for \(2^{\aleph_0}\) (see erdos_261.parts.iii, which remains open).

theorem erdos_261.variants.two_representations : ∃ x : ℚ,
    2 ≤ #{a : ℕ → ℕ | Erdos261InfiniteRepresentation x a}

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/261.lean, line 113.

Sources
LeanErdos261.erdos_261.variants.borwein_loring · Erdos261.erdos_261.variants.borwein_loring_property · Erdos261.erdos_261.parts.i · Erdos261.erdos_261.variants.le_10000 · Erdos261.erdos_261.parts.ii · Erdos261.erdos_261.parts.iii · Erdos261.erdos_261.variants.two_representations

TheoremErdős Problem 263#

Reference: erdosproblems.com/263

Quoted from FormalConjectures/ErdosProblems/263.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The problem's page on erdosproblems.com: https://www.erdosproblems.com/263.

The file states 7 research or textbook statements: 1 open and 6 solved.

Erdos263.erdos_263.parts.i

Open: stated without proof.

Is \(a_n = 2^{2^n}\) an irrationality sequence in the above sense?

theorem erdos_263.parts.i : IsIrrationalitySequence (fun n : ℕ => 2 ^ 2 ^ n)

Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/263.lean, line 67.

Erdos263.erdos_263.parts.ii

Solved: stated here without proof.

Must every irrationality sequence \(a_n\) in the above sense satisfy \(a_n^{1/n} \to \infty\) as \(n \to \infty\)?

The answer is no. Liam Price's construction gives a strictly increasing irrationality sequence with \(\liminf a_n^{1/n} = 1\).

theorem erdos_263.parts.ii :
    ¬ (∀ a : ℕ → ℕ,
      IsIrrationalitySequence a →
        atTop.Tendsto (fun n : ℕ => (a n : ℝ) ^ (1 / (n : ℝ))) atTop)

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/263.lean, line 78.

Erdos263.erdos_263.variants.folklore

Solved: stated here; a Lean proof is at https://github.com/anatoliiohorodnyk/lean-fc-proofs/blob/5da9642575b26c2c816a49bcb56b33fed5456619/Proofs/T_Erdos263_erdos_263_variants_folklore.lean#L399.

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.

theorem erdos_263.variants.folklore (a : ℕ -> ℕ)
    (ha : atTop.Tendsto (fun n : ℕ => (a n : ℝ) ^ (1 / (2 ^ n : ℝ))) atTop) :
    Irrational <| ∑' n, (1 : ℝ) / (a n : ℝ)

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/263.lean, line 90.

Erdos263.erdos_263.variants.sub_doubly_exponential

Solved: stated here without proof.

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

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

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/263.lean, line 104.

Erdos263.erdos_263.variants.super_doubly_exponential

Solved: stated here; a Lean proof is at https://github.com/arex1337/erdos-263-lean/blob/95de79a5cd49050df80e95be6cfc161580830799/Erdos263/Folklore.lean#L700.

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.

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

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/263.lean, line 119.

Erdos263.erdos_263.variants.super_doubly_exponential_eventual

Solved: stated here; a Lean proof is at https://github.com/anatoliiohorodnyk/lean-fc-proofs/blob/5da9642575b26c2c816a49bcb56b33fed5456619/Proofs/T_Erdos263_erdos_263_variants_super_doubly_exponential_eventual.lean#L515.

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\).

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

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/263.lean, line 136.

Erdos263.erdos_263.variants.doubly_exponential_all_but_countable

Solved: stated here without proof.

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

theorem erdos_263.variants.doubly_exponential_all_but_countable :
    ∀ᶠ (α : ℝ) in .cocountable, α > 1 →
      IsWeakIrrationalitySequence (fun n : ℕ => ⌊α ^ 2 ^ n⌋₊)

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/263.lean, line 154.

Sources
LeanErdos263.erdos_263.parts.i · Erdos263.erdos_263.parts.ii · Erdos263.erdos_263.variants.folklore · Erdos263.erdos_263.variants.sub_doubly_exponential · Erdos263.erdos_263.variants.super_doubly_exponential · Erdos263.erdos_263.variants.super_doubly_exponential_eventual · Erdos263.erdos_263.variants.doubly_exponential_all_but_countable

TheoremErdős Problem 264#

Reference: erdosproblems.com/264

Quoted from FormalConjectures/ErdosProblems/264.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The problem's page on erdosproblems.com: https://www.erdosproblems.com/264.

The file states 5 research or textbook statements: 1 open and 4 solved.

Erdos264.erdos_264.parts.i

Solved: stated here without proof.

Is \(2^n\) an example of an irrationality sequence? Kovač and Tao proved that it is not [KoTa24]

[KoTa24] Kovač, V. and Tao T., On several irrationality problems for Ahmes series. arXiv:2406.17593 (2024).

theorem erdos_264.parts.i : ¬IsIrrationalitySequence (2 ^ ·)

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/264.lean, line 56.

Erdos264.erdos_264.parts.ii

Open: stated without proof.

Is \(n!\) an example of an irrationality sequence?

theorem erdos_264.parts.ii : IsIrrationalitySequence Nat.factorial

Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/264.lean, line 62.

Erdos264.erdos_264.variants.example

Solved: stated here without proof.

One example is \(2^{2^n}\).

theorem erdos_264.variants.example : IsIrrationalitySequence (fun n ↦ 2 ^ (2 ^ n))

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/264.lean, line 68.

Erdos264.erdos_264.variants.ko_tao_neg

Solved: stated here without proof.

Kovač and Tao [KoTa24] generally proved that any strictly increasing sequence of positive integers \(a_n\) such that \(\sum \frac{1}{a_n}\) converges and

\[ \liminf_{n \to \infty} (a_n^2 \sum_{k > n} \frac{1}{a_k^2}) > 0 \]

is not an irrationality sequence.

[KoTa24] Kovač, V. and Tao T., On several irrationality problems for Ahmes series. arXiv:2406.17593 (2024).

theorem erdos_264.variants.ko_tao_neg {a : ℕ → ℕ} (h₁ : StrictMono a) (h₂ : 0 ∉ Set.range a)
    (h₃ : Summable ((1 : ℝ) / a ·))
    (h₄ : ∃ C > 0, ∀ᶠ n in atTop, C ≤ a n ^ 2 * ∑' k : Set.Ioi n, (1 : ℝ) / a k ^ 2) :
    ¬IsIrrationalitySequence a

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/264.lean, line 81.

Erdos264.erdos_264.variants.ko_tao_pos

Solved: stated here without proof.

On the other hand, Kovač and Tao [KoTa24] do prove that for any function \(F\) with \(\lim_{n \to \infty} \frac{F(n + 1)}{F(n)} = \infty\) there exists such an irrationality sequence with \(a_n \sim F(n)\).

[KoTa24] Kovač, V. and Tao T., On several irrationality problems for Ahmes series. arXiv:2406.17593 (2024).

theorem erdos_264.variants.ko_tao_pos {F : ℕ → ℕ}
    (hF : atTop.Tendsto (fun n ↦ (F (n + 1) : ℝ) / F n) atTop) :
    ∃ a : ℕ → ℕ, IsIrrationalitySequence a ∧ (fun n ↦ (a n : ℝ)) ~[atTop] fun n ↦ (F n : ℝ)

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/264.lean, line 94.

Sources
LeanErdos264.erdos_264.parts.i · Erdos264.erdos_264.parts.ii · Erdos264.erdos_264.variants.example · Erdos264.erdos_264.variants.ko_tao_neg · Erdos264.erdos_264.variants.ko_tao_pos

TheoremErdős Problem 266#

Reference: erdosproblems.com/266

Quoted from FormalConjectures/ErdosProblems/266.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The problem's page on erdosproblems.com: https://www.erdosproblems.com/266.

The file states 2 research or textbook statements: 2 solved.

Erdos266.erdos_266

Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos266.lean#L306.

Let \(a_n\) be an infinite sequence of positive integers such that \(\sum \frac{1}{a_n}\) converges. There exists some integer \(t \ge 1\) such that \(\sum \frac{1}{a_n + t}\) is irrational.

This was disproven by Kovač and Tao in [KoTa24].

[KoTa24] Kovač, V. and Tao T., On several irrationality problems for Ahmes series. arXiv:2406.17593 (2024).

theorem erdos_266 :
    ¬ ∀ (a : ℕ → ℕ), ((∀ n : ℕ, a n ≥ 1) ∧ Summable ((1 : ℝ) / a ·) →
      ∃ t ≥ (1 : ℕ), Irrational <| ∑' n, (1 : ℝ) / ((a n) + t))

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/266.lean, line 44.

Erdos266.erdos_266.variants.all_rationals

Solved: stated here; a Lean proof is at https://github.com/benkeene/erdos266/blob/ef01b23804a60669f24b25733f1a2b688084609d/Solution.lean#L27.

In fact, Kovač and Tao proved in [KoTa24] that there exists a strictly increasing sequence \(a_n\) of positive integers such that \(\sum \frac{1}{a_n + t}\) converges to a rational number for all \(t \in \mathbb{Q}\) such that \(t \ne -a_n\) for any \(n\).

[KoTa24] Kovač, V. and Tao T., On several irrationality problems for Ahmes series. arXiv:2406.17593 (2024).

Lean formalization by Ben Keene, with AI assistance.

theorem erdos_266.variants.all_rationals:
    ∃ a : ℕ → ℕ, StrictMono a ∧ a 0 ≥ 1 ∧
      (∀ t : ℚ, (¬ ∃ n : ℕ, t = -(a n)) →
        (∃ q : ℚ, HasSum (fun n : ℕ => ((1 : ℝ) / ((a n) + t))) q))

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/266.lean, line 62.

Sources
LeanErdos266.erdos_266 · Erdos266.erdos_266.variants.all_rationals

TheoremErdős Problem 267#

Reference: erdosproblems.com/267

Quoted from FormalConjectures/ErdosProblems/267.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The problem's page on erdosproblems.com: https://www.erdosproblems.com/267.

The file states 4 research or textbook statements: 1 open and 3 solved.

Erdos267.erdos_267

Solved: stated here; a Lean proof is at https://github.com/williamjblair/lean-proofs/blob/4f915a323443bfb1709a6805a013812016dca88a/starfleet/erdos-267/Research/Basic.lean.

Let \(F_1=F_2=1\) and \(F_{n+1} = F_n + F_{n-1}\) be the Fibonacci sequence. Let \(n_1 < n_2 < \dots\) be an infinite sequence with \(\frac{n_{k+1}}{n_k} \ge c > 1\). Must \(\sum_k \frac 1 {F_{n_k}}\) be irrational?

theorem erdos_267 : ∀ᵉ (n : ℕ → ℕ) (c > (1 : ℚ)), StrictMono n → (∀ k, c ≤ n (k+1) / n k) →
    Irrational (∑' k, 1 / (Nat.fib <| n k))

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/267.lean, line 37.

Erdos267.erdos_267.variants.generalisation_ratio_limit_to_infinity

Open: stated without proof.

Let \(F_1=F_2=1\) and \(F_{n+1} = F_n + F_{n-1}\) be the Fibonacci sequence. Let \(n_1 < n_2 < \dots\) be an infinite sequence with \(\frac {n_k}{k} \to \infty\). Must \(\sum_k \frac 1 {F_{n_k}}\) be irrational?

theorem erdos_267.variants.generalisation_ratio_limit_to_infinity : ∀ (n : ℕ → ℕ),
    StrictMono n → Filter.Tendsto (fun k => (n (k+1) / k.succ : ℝ)) Filter.atTop Filter.atTop →
    Irrational (∑' k, 1 / (Nat.fib <| n k))

Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/267.lean, line 47.

Erdos267.erdos_267.variants.specialization_pow_two

Solved: stated here; a Lean proof is at https://github.com/mo271/formal-conjectures/blob/2663234a28260853790aa5752d8d4550ff0ab1ca/FormalConjectures/ErdosProblems/267.lean#L56.

Good [Go74] and Bicknell and Hoggatt [BiHo76] have shown that \(\sum_n \frac 1 {F_{2^n}}\) is irrational.

Formal proof provided by AlphaProof Ref: * [Go74] Good, I. J., A reciprocal series of Fibonacci numbers * [BiHo76] Hoggatt, Jr., V. E. and Bicknell, Marjorie, A reciprocal series of Fibonacci numbers with subscripts \(2\sp{n}k\)

theorem erdos_267.variants.specialization_pow_two :
    Irrational <| ∑' k, 1 / (Nat.fib <| 2^k)

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/267.lean, line 64.

Erdos267.erdos_267.variants.fibonacci_inverse_sum

Solved: stated here without proof.

The sum \(\sum_n \frac 1 {F_{n}}\) itself was proved to be irrational by André-Jeannin.

Ref: André-Jeannin, Richard, Irrationalité de la somme des inverses de certaines suites récurrentes.

theorem erdos_267.variants.fibonacci_inverse_sum :
    Irrational <| ∑' k, 1 / (Nat.fib k)

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/267.lean, line 74.

Sources
LeanErdos267.erdos_267 · Erdos267.erdos_267.variants.generalisation_ratio_limit_to_infinity · Erdos267.erdos_267.variants.specialization_pow_two · Erdos267.erdos_267.variants.fibonacci_inverse_sum

TheoremErdős Problem 268#

Reference: - erdosproblems.com/268 - [KoTa24] Kova\vC, V. and Tao T., On several irrationality problems for Ahmes series.

Quoted from FormalConjectures/ErdosProblems/268.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The problem's page on erdosproblems.com: https://www.erdosproblems.com/268.

The file states 1 research or textbook statement: 1 solved.

Erdos268.erdos_268

Solved: stated here; a Lean proof is at https://gist.githubusercontent.com/madeve-unipi/62a8f68cdb4864b85b81a6752dcb0aa4/raw/5793aaa51089c25c37d8d63f60540367f6abe506/Erdos268.lean.

Let X be the set of points in Fin d → ℝ of the shape fun i : Fin d => ∑' n : A, (1 : ℝ) / (n + i) for some infinite subset A ⊆ ℕ such that 1 / n is summable over A. X has nonempty interior. This is proved in [KoTa24]. -

theorem erdos_268 (d : ℕ) : (interior {x : Fin d → ℝ | ∃ A : Set ℕ, A.Infinite ∧
    Summable (fun n : A => (1 : ℝ) / n ) ∧
    x = fun i : Fin d => ∑' n : A, (1 : ℝ) / (n + i)}).Nonempty

Category research solved; AMS 40 Sequences, series, summability, 54 General topology. Declared in FormalConjectures/ErdosProblems/268.lean, line 39.

Sources
LeanErdos268.erdos_268

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.