Erdős·erdos:266
Erdős Problem 266
No independent check recorded yet. A formal artifact, declaration or published object is attached, but no rebuild of it is recorded here.
A Palomar registration names this problem. It is shown below but not counted as a check of the claim.
Fidelity F2: The correspondence is declared through an alignment table and written divergences.
irrationality·Source
AI activity
How grades workNo AI contribution recorded against this statement.
Fidelity
How fidelity is gradedF2 declared. The correspondence is declared through an alignment table and written divergences.
Checks
1-
verified·Palomar
Registered by Palomar at aa0cd43f: Comparator confirmed 2 theorems prove the recorded statement within Palomar's axiom policy, replayed through Lean's kernel and the independent nanoda kernel. The project names this problem, which does not establish that it proves the result claimed here, so it is not counted as a check of it
Declared by the projects
1As each project's formalization.yaml states it.
Erdős problem #266: the Kovač–Tao disproof of Stolarsky's conjecture
- authors
- Ben Keene
- method
- agent — Claude Fable 5 (Anthropic)
- review
- self-assessed (Ben Keene)
- axioms
- Classical.choice, Quot.sound, propext
- sorry
- 2 unproved goals declared
- sources
- On several irrationality problems for Ahmes series — formalizes; Erdős problem #266 (erdosproblems.com) — background; Formal Conjectures: ErdosProblems/266.lean — adapts
- divergences
- The arXiv abstract of [KoTa24] states the final construction for integer shifts (t in Z) only; the body of the paper proves more. Checked against arXiv v4 (14 Jul 2025): Erdos266.erdos_266_rational_shifts is Theorem 2.11 verbatim — a strictly increasing sequence of positive integers whose shifted series converges to a rational for every t in Q avoiding {-a_n} — and Section 2.3 states explicitly that the conjecture is disproved "not only when t ranges over the integers" but for rational t. Erdos266.erdos_266 is the negative answer to Stolarsky's conjecture as recorded by Erdős–Graham (integer shifts t >= 1), implied by Theorem 2.11. "Converges to a rational" is rendered as HasSum toward the real embedding of a rational; for these series (all but finitely many terms positive) unconditional and ordered convergence agree.
- checked by
- Palomar
Follow and discuss
All discussionFollow this problem
An email when it has a new claim, check, bounty or discussion. You confirm once and can stop with one click.
Discussion and bounties for this problem load here.
Seen recently
What the monitors picked up in the last thirty days, not yet graded.
Something wrong or missing here? Request a correction or add a claim, with its sources.
Claims and corrections from readers
All of themFormal material
Formal statements · 1
Also known as · 3
- https://www.erdosproblems.com/266
- https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/266.lean
- FormalConjectures/ErdosProblems/266.lean
Cite this record
qed.bot, “Erdős Problem 266”, https://qed.bot/s/erdos-266, as of 30 Sep 2026.