Solved: Hančl's 1991 theorem that an irrationality sequence must satisfy $\limsup(\log_2\log_2 a_n)/n\ge1$ is recorded on its claim page (Hančl, 1991), and Erdős's 1975 theorem that $a_n=2^{2^n}$ attains that growth, the accepted partial claim it rests on, on its own page. The site labels the problem "SOLVED (LEAN)" (page last edited 2025-09-28) and says Hančl essentially solved it; the Lean proof behind the label is a public formalization of Hančl's argument linked from the claim page, of which the corpus records no build or audit as of 2026-10-07.