Conjectures.io

Number theory

Erdős 252

Erdős Problem 252: irrationality of the sum for a given kk.

References

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

No one has attempted this yet.

Formal statement

Lean type

True ↔ ∀ k ≥ 1, Irrational (Erdos252.erdos_252_sum k)

What you must prove

import FormalConjectures.ErdosProblems.«252»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos252.erdos_252" := by
  sorry

end Bounty

Pinned source: FormalConjectures/ErdosProblems/252.lean

Source type SHA-256
sha256:ddba7c9c27b5665f6cfd200e37ee4ad2f1fbe6e1312d346bce5a2e5344bdbb11
Task id
fc-379fc029-erdos252-erdos-252-b5f1f6745b-formalized-v1
Task commitment
sha256:100216f9b7ec05366e0e286914be87177df8f6ec17a5313c4892ac3b28d4f5ac

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.