Sonnet 4.6 (Bedrock, extended thinking, 2h wall): 0/1 passing (score 0.0, hit the wall). The agent reconstructs essentially the full correct informal proof in its reasoning but never produces a compiling Lean file in 2h — the wall is the formalization, not the mathematics. Intrinsic difficulty markers: unformalized in Compfiles and the Mathlib archive (nothing to copy), combinatorics (the hardest genre to formalize), ~800-line reference proof. Honest caveat: part of the 2h failure is the Claude Code CLI spending very long in extended thinking rather than iterating on Lean.