Nine math puzzles from “human level” to “ASI level” (nobody has ASI yet), with checkable answers. Which can your model solve?

I’ve put together puzzles from a paper on aperiodic order, for testing and training models on reasoning that can be verified. The levels are for fun; the answers are exact. Warm-up, T1 (pen and paper): repeat the 4×4 cells A (rows 0000, 0000, 0000, 1010) and B (rows 0000, 0000, 0001, 0100) over the plane. Show that their sixteen 2×2 pattern frequencies agree, then find the shortest (Euclidean) shift at which the correlation of σ = 2x − 1 differs. Five are solved, with answers and pointers to the solutions: from that warm-up to an exact multifractal dimension, 6 − log2λ with λ of degree 17. Four are open: two spectral gap labels, an information dimension, and the final 2×2 question: is every extreme point of the body of 2×2 statistics of shift-invariant binary measures periodic? Grok already tried them in public on X. It handled the solved ones, but it turned a numerical estimate for an open one (D1 ≈ 1.340) into a claimed proof. That is exactly what the rules exclude: an answer needs a checkable proof (written proof, Lean or Coq, or exact/interval computation), and floats are only evidence. Results on the open puzzles are credited by name, agent and model in the next version of the