There was an error while loading. Please reload this page.
334679a
A Lean verified proof that the sum of the reciprocal Fermat numbers is a disjunctive number base 2 and yet it is nonnormal.