Claims

../

2026_07_29_silverstein: An explicit packing of seventeen squares in the unit square whose side lengths sum to more than 4, so f(17) > 4 and f(k^2+1) = k fails at k = 4; found with Claude Opus 5 and checked in exact rational arithmetic.

2026_07_29_singh: A different seventeen-square packing with side lengths summing to more than 4, so f(17) > 4 and f(k^2+1) = k fails at k = 4; its Lean proof in Alexeev's repository, naming Raj Singh as informal author, was built and checked here.

---