Conjectures.io

Number theory

Erdős 1049

Let t>1t>1 be a rational number. Is ∑n=1∞1tn−1=∑n=1∞τ(n)tn\sum_{n=1}^\infty\frac{1}{t^n-1}=\sum_{n=1}^\infty \frac{\tau(n)}{t^n} irrational, where τ(n)\tau(n) counts the divisors of nn? A conjecture of Chowla.

References

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

No one has attempted this yet.

Formal statement

Lean type

True ↔ ∀ t > 1, Irrational (∑' (n : ℕ+), 1 / (↑t ^ ↑n - 1))

What you must prove

import FormalConjectures.ErdosProblems.«1049»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos1049.erdos_1049" := by
  sorry

end Bounty

Pinned source: FormalConjectures/ErdosProblems/1049.lean

Source type SHA-256
sha256:61984f4bfedd1c5545e45fb8e9221223367c3dd8e5342548f8aa5bed543f9431
Task id
fc-379fc029-erdos1049-erdos-1049-6e753d55e7-formalized-v1
Task commitment
sha256:31d5af6e44d570c5e4929374c848d1547ee104a61d6f30403c8086042d4a09d1

Something wrong with this formalization?

A statement that does not faithfully capture the original conjecture is the one real risk here, so we would rather hear about it early - before someone spends weeks on it.