---

Claim. The answer to Problem 106 is no: $f(17)>4$, so $f(k^2+1)=k$ fails at $k=4$. The witness is a packing of seventeen squares in the unit square, sixteen of them parallel to its sides and one rotated, described first in a square of side $4$ and then scaled by one quarter, with side lengths summing to

$$4+\frac{78}{4\cdot 1048735}=4.0000185\ldots$$

The packing differs from the one on Silverstein's claim page, whose sum is $4.000124\ldots$, so it is a separate counterexample rather than a formalization of that one. The Lean file proves that the seventeen squares lie in the unit square with pairwise disjoint interiors and that their side lengths sum to the value above; its theorem Erdos106.four_lt_f_seventeen, $4<f(17)$, carries the claim.

Claimant. The Lean proof was added to Boris Alexeev's repository of formalized Erdős problems on 2026-07-29, about fifteen hours before Silverstein's claim was posted, with OpenAI Codex as its only named author and no informal author; on 2026-08-23 its header was extended to name A. Raj Singh as informal author and Codex and GPT-5.6 Sol as formal authors, which is how the file linked above reads at its pinned commit. No informal manuscript of this packing is recorded, and Singh's paper on the problem, listed among the problem page's references, reformulates the conjecture without a counterexample.

Acceptance. Formalized. This corpus's verification built the module ErdosProblems.Erdos106 of the repository's src/latest folder at the pinned commit of 2026-09-15 (Lean v4.33.0, Mathlib v4.33.0), together with the repository's comparator challenge for the problem, and checked the axioms of Erdos106.four_lt_f_seventeen and Erdos106.not_erdos_106, which are exactly propext, Classical.choice and Quot.sound. The built file is the version at the pinned commit, a revision of the 2026-07-29 posting moved to Lean v4.33.0 and given the extended header; the original posting was not built. The challenge pins only Erdos106.not_erdos_106, $\neg\,\forall k\in\mathbb N,\ f(k^2+1)=k$, with the definitions its type reaches (a square given by its center, a unit side direction and its side length; its closed and open point sets; the box $[0,L]^2$; a packing; the total side length; the set of attainable totals; and $f$ as its supremum), and the fingerprint of that declaration and of each of those definitions was found identical to the challenge. That theorem alone does not carry the claim: it already holds at $k=0$, where the identity asks $f(1)=0$ while one unit square gives $f(1)=1$, and it says nothing about $f(17)$. The claim rests on Erdos106.four_lt_f_seventeen, which the challenge does not pin but which is stated over the same compared $f$. The statement audit found that $f$ is faithful to the problem: the squares may be rotated, each is a closed square of positive side inside the closed unit square, their interiors are pairwise disjoint, and $f(n)$ is the supremum of a nonempty set bounded above, so $4<f(17)$ is exactly the disproof at $k=4$. Not reviewed: the site's curator credits Silverstein's packing (its claim page), not this one, and the site's label notes a Lean verification without linking one; no outside reviewer has published an examination of this development. Not refereed: there is no journal publication of this packing.