An elementary reduction of the {0,1} square problem

We establish an elementary equivalence for Guy’s Problem F24, the open question asking whether there exists a non-trivial integer n (not a power of 10) whose square contains only decimal digits 0 and 1. We prove such an integer n exists if and only if there exists a non-negative integer m such that 2m(m+1) contains only digits 5 and 0. The argument relies only on basic modular arithmetic and simple algebraic identities, requiring no unproven hypotheses. We also derive modular restrictions on m that accelerate computational searches for candidate solutions. Formal verification of core reasoning has been completed with an automated proof assistant.