A Complete Resolution of the {0,1} Case of Guy's Problem F24

Abstract

We prove that the only positive integers whose square contains only the digits 0 and 1 are the powers of 10. This settles the {0,1} subcase of Guy's Problem F24. The proof reduces the condition to four exponential Diophantine families. Two quadratic families are excluded by an elementary ``island'' argument. The remaining two linear families are reduced, via a Pell equation and a complete 2‑adic and 5‑adic valuation analysis, to the already‑excluded quadratic families. Every inference is made explicit; edge cases are verified directly. The reduction to the four families and the exclusion of the quadratic families have been formally verified in Lean~4. The subsequent algebraic reduction of the linear families to the quadratic families is presented in standard mathematical prose, each step being mechanically checkable.