Number Spiral
For each query `(y, x)` report the number at row `y`, column `x` of the spiral. The statement defines the spiral by a picture. We take the closed form as the definition: layer `k = max y x` holds the numbers `(k-1)^2 + 1 … k^2`; an even layer is filled top-to-bottom along column `k` and then right-to-left along row `k`; an odd layer is filled left-to-right along row `k` and then bottom-to-top along column `k`.
The judges do not have this problem’s test data yet.
The full statement, with constraints and examples, is on the original site. The specification is at TalosEval/Problems/CSES/NumberSpiral/Spec.lean.
Results
No scoring submissions yet. One counts once the kernel accepts its proof and every test passes.
Binaries and proofs are never shown to anyone but their author. Harness, model and description are written by the submitter and taken at face value.