Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.
Updated
Problem 270
claims/: The 2 claim pages of Problem 270, one per claimant's result; the problem's standing derives from them.
Statement. Let as . Is it true that
is irrational?
Status. Disproved: Crmarić and Kovač's 2025 theorem that every positive real number is the value of such a series for some is recorded on its claim page. The site (page last edited 2025-09-28) labels the problem DISPROVED (LEAN) and credits them with the negative answer; the Lean proof behind the label is a public formalization of their argument linked from the claim page, not built or audited in this corpus. The variant with nondecreasing , which the statement does not impose, remains open. The case is answered yes: Kovač posted on the site's discussion thread (2026-07-12) that equals with , a Cantor series with increasing integer terms, hence irrational. A manuscript of August 2026 extends the argument to with and claims transcendence, hence irrationality, for every and ; it is a pending partial claim at Lambrinoudis 2026.
Source. erdosproblems.com/270, accessed 2026-09-04. Cite as: T. F. Bloom, Erdős Problem #270, https://www.erdosproblems.com/270.
References.
- [CrKo25] T. Crmarić and V. Kovač, On the irrationality of certain super-polynomially decaying series. arXiv:2504.18712 (2025).
- [Ha75] Hansen, E. R., A Table of Series and Products. Prentice-Hall (1975), 87.
Formalization. Statement in
formal-conjectures
at the linked commit, tagged research solved, whose formal_proof attributes
cite a Lean 4 proof in the public lean-proofs repository at a commit of
2026-09-15; that proof is linked from the claim page and is not built or
audited in this corpus.
Progress
Not yet compiled.
Known Results
Not yet compiled.
Linked library material
These entries are derived from explicit links on library pages. They are navigation only and do not by themselves record mathematical progress.
- crmaric_2025_irrationality_certain_super_polynomially_decaying_series
- crmaric_2025_irrationality_certain_super_polynomially_decaying_series / lemma_4
- crmaric_2025_irrationality_certain_super_polynomially_decaying_series / theorem_1
- crmaric_2025_irrationality_certain_super_polynomially_decaying_series / theorem_2