qedbot

Erdős·erdos:266

Erdős Problem 266

problem formal record: solved source: disproved (Lean)no F2 declared

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 work

No AI contribution recorded against this statement.

Does the formal statement say what was claimed?

F2 declared The correspondence is declared through an alignment table and written divergences.

declares divergences from its source declares 2 unproved goals reviewed by its authors only

Computed from what the project declares and what the register holds, never from reading the mathematics. How fidelity is graded.

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

    project registered at a pinned commit·2026-08-20·commit aa0cd43fb45d

    PALOMAR-2026-08-20-000008 — names this problem; not counted as a check of the claim

Declared by the projects

1

Read from each project's formalization.yaml. A declaration is what the authors say about their own work, recorded so that a check can confirm or contradict it.

Erdős problem #266: the Kovač–Tao disproof of Stolarsky's conjecturebenkeene/erdos266 · joined by names · Palomar

Read formalization.yaml

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 discussion

Discussion and bounties for this problem load here.

Formal material

Formal statements · 1
Cited proofs · 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