/- Copyright 2026 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. -/ import FormalConjecturesUtil

Erdős Problem 1049

References:

    erdosproblems.com/1049

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

namespace Erdos1049open ArithmeticFunction Filter

Let $t>1$ be a rational number. Is $\sum_{n=1}^\infty\frac{1}{t^n-1}=\sum_{n=1}^\infty \frac{\tau(n)}{t^n}$ irrational, where $\tau(n)$ counts the divisors of $n$?

A conjecture of Chowla.

@[category research open, AMS 11] theorem erdos_1049 : answer(sorry) t : , t > 1 Irrational (∑' n : ℕ+, 1 / ((t : ) ^ (n : ) - 1)) := True t > 1, Irrational (∑' (n : ℕ+), 1 / (t ^ n - 1)) All goals completed! 🐙

Erdős [Er48] proved that this is true if $t\geq 2$ is an integer.

@[category research solved, AMS 11] theorem erdos_1049.variants.geq_2_integer : t : , t 2 Irrational (∑' n : ℕ+, 1 / ((t : ) ^ (n : ) - 1)) := t 2, Irrational (∑' (n : ℕ+), 1 / (t ^ n - 1)) All goals completed! 🐙

Convergent case (|t| > 1).

Substitute r := t⁻¹ so ‖r‖ < 1, then apply Mathlib's series identity tsum_pow_div_one_sub_eq_tsum_sigma at k = 0: $$\sum_{n \ge 1} \frac{r^n}{1 - r^n} = \sum_{n \ge 1} \sigma_0(n) \cdot r^n.$$ After clearing denominators, both sides match the Lambert identity: LHS becomes 1/(t^n - 1) and RHS becomes τ(n) / t^n.

t:ht:1 < |t|ht0:t 0htn: (n : ), t ^ n 0r: := t⁻¹hr_def:r = t⁻¹hr_norm:r < 1h:∑' (n : ℕ+), n ^ 0 * r ^ n / (1 - r ^ n) = ∑' (n : ℕ+), ((sigma 0) n) * r ^ nn:ℕ+hp:t ^ n 0hrn:r ^ n = (t ^ n)⁻¹(↑n).divisors.card / t ^ n = (↑n).divisors.card * (t ^ n)⁻¹; All goals completed! 🐙

Divergent case (|t| ≤ 1).

Both tsums equal 0 in this regime, but for different reasons in each sub-case. We split on t ∈ {1, 0, -1} and the generic |t| < 1, t ≠ 0 remainder, and use the same key non-summability lemma below to handle the cases where the series diverges.

    t = 1: every LHS term is 1 / (1 - 1) = 0 (Lean convention), so the LHS sum is trivially 0. RHS is Σ τ(n), non-summable.

    t = 0: every RHS term is τ(n) / 0 = 0 (Lean convention), so the RHS sum is trivially 0. LHS is Σ (-1), non-summable.

    t = -1: alternating; LHS vanishes at even n but odd n give terms of magnitude 1/2, an infinite set. RHS terms have magnitude τ(n) ≥ 1.

    |t| < 1, t ≠ 0: standard; bounded denominator gives lower-bounded reciprocal on LHS, and |t^n| ≤ 1 plus τ(n) ≥ 1 gives the RHS bound.

In every case, Lean's tsum_eq_zero_of_not_summable collapses the non- summable side to 0, matching the 0 on the other side.

All goals completed! 🐙

The classical Lambert series identity: $\sum_{n=1}^\infty \frac{1}{t^n - 1} = \sum_{n=1}^\infty \frac{\tau(n)}{t^n}$, where $\tau(n)$ counts the divisors of $n$.

@[category textbook, AMS 11] theorem lambert_series_eq_num_divisor_sum : t : , ∑' n : ℕ+, 1 / ((t : ) ^ (n : ) - 1) = ∑' n : ℕ+, (n : ).divisors.card / ((t : ) ^ (n : )) := (t : ), ∑' (n : ℕ+), 1 / (t ^ n - 1) = ∑' (n : ℕ+), (↑n).divisors.card / t ^ n t:∑' (n : ℕ+), 1 / (t ^ n - 1) = ∑' (n : ℕ+), (↑n).divisors.card / t ^ n t:ht:1 < |t|∑' (n : ℕ+), 1 / (t ^ n - 1) = ∑' (n : ℕ+), (↑n).divisors.card / t ^ nt:ht:|t| 1∑' (n : ℕ+), 1 / (t ^ n - 1) = ∑' (n : ℕ+), (↑n).divisors.card / t ^ n t:ht:1 < |t|∑' (n : ℕ+), 1 / (t ^ n - 1) = ∑' (n : ℕ+), (↑n).divisors.card / t ^ n All goals completed! 🐙 t:ht:|t| 1∑' (n : ℕ+), 1 / (t ^ n - 1) = ∑' (n : ℕ+), (↑n).divisors.card / t ^ n All goals completed! 🐙end Erdos1049