DISPROVED (LEAN). The site credits Yip [Yi25], whose representation theorem yields, for each real $t\neq 0$, an admissible infinite sequence with $1+\sum_k a_k^{-(1+it)}=0$; its Lean marker refers to a third-party formalization that this corpus has not built, and it records the finite-sequence variant as open. The standing derives from Yip's claim page (2025).