Erdős #257
Take the fractions 1, 1/3, 1/7, 1/15 and so on, and add up infinitely many of them. Erdős asked whether the total can ever be written as a fraction. In 1968 he stated one case, where the reciprocals of the chosen exponents have a finite sum, and proved it with an extra restriction. Here that case is proved without the restriction, and Lean accepts the proof.
Limits: The question Erdős asked, for every infinite choice, is still open. The papers are written with AI and are not peer reviewed.
Erdős stated this case in 1968. Google DeepMind’s Formal Conjectures lists it as solved.
Lean is a program that checks mathematical proofs.
