{"id":"palomar/PALOMAR-2026-08-20-000008","url":"https://github.com/benkeene/erdos266/tree/ef01b23804a60669f24b25733f1a2b688084609d","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-08-20-000008-v2.json","repo":"https://github.com/benkeene/erdos266","tags":["math.NT","math.CA","msc:11J72","msc:40A05","msc:11B83","number-theory","erdos-problems","lean-formalization","egyptian-fractions"],"score":0,"title":"Erdős problem #266: the Kovač–Tao disproof of Stolarsky's conjecture","trust":"high","domain":"math.NT","source":"palomar","authors":["Ben Keene"],"reviews":0,"subject":"math.NT","summary":"A Lean 4 formalization, against Mathlib, of the Kovač–Tao resolution of Erdős problem #266 (a conjecture of Stolarsky): it is not true that every sequence of positive integers with convergent reciprocal sum admits an integer shift t >= 1 making the shifted Ahmes series irrational. The stronger construction is also formalized: a strictly increasing sequence of positive integers whose shifted series has a rational sum for every admissible rational shift.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-12","reactions":{},"formalized":true,"formalizes":[{"title":"On several irrationality problems for Ahmes series","identifier":"https://arxiv.org/abs/2406.17593","relationship":"formalizes"},{"title":"Formal Conjectures: ErdosProblems/266.lean","identifier":"https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/266.lean","relationship":"adapts"}]}