Erdős Problem 260

Erdős Problem 260 asks whether every sufficiently sparse binary expansion of the form $\sum_{n\ge1}2^{-a_n}$, with $a_n/n\to\infty$, is irrational. A June 2026 preprint claims an affirmative proof.

June–August 2026 claimed proof and formalization

The June preprint claims a stronger positive-density theorem for the support of a rational binary expansion and derives the stated irrationality result. It reports that the associated Lean project covered only part of the stopping-time argument and finite checks; by August, the repository itself claimed a complete Lean proof without placeholders or project-level axioms. The mathematical proof and formalization remain unverified independently.

Current status (as of August 2026): A preprint claims the irrationality theorem and the repository claims a complete Lean formalization, but independent validation of both the argument and its formalization is still absent.