---

Claim. The answer to Problem 658 is yes. The claimed result is Theorem 1.1 of J. Solymosi, A note on a question of Erdős and Graham: for every real $\delta>0$ there is $N_0(\delta)$ such that for $N>N_0$ every $S\subseteq[N]^2$ with $|S|\ge\delta N^2$ contains a quadruple $\{(a,b),(a+d,b),(a,b+d),(a+d,b+d)\}$ with integer $d\ne0$, where $[N]=\{0,\ldots,N-1\}$. The grid differs from the site's $\{1,\ldots,N\}^2$ by a translation, and an axis-parallel square is a square, so the theorem gives the site's conclusion in Graham's axis-parallel form and hence in the form allowing any square. The proof lifts $S$ to $S\times[N]\subseteq[N]^3$, where a square corresponds to a quadruple $\{(a,b,c),(a+d,b,c),(a,b+d,c),(a+d,b+d,c+d)\}$, $d\ne0$, and builds a four-partite $3$-uniform hypergraph whose vertices are the planes parallel to the four faces of that configuration, with an edge for each triple of planes from distinct classes that meets in a point of the lifted set. Four planes, one from each class, form a complete subgraph when each of their triples meets in the set: the four planes through one point give a degenerate one, and a non-degenerate one is exactly a quadruple. If the set contains no quadruple, every edge lies in exactly one complete subgraph, so the Frankl–Rödl theorem gives $o(N^3)$ edges, while the hypergraph has $4|S\times[N]|=4N|S|$ edges; so $|S|\ge\delta N^2$ forces a quadruple once $N$ is large. The paper states no bound: its Remark says that, because the Frankl–Rödl theorem rests on the regularity lemma, the method's bound on $N_0$ is at best of tower type. The statement, the one-page proof and the lifting are recorded on the source card; the argument takes the Frankl–Rödl theorem as an external premise (claims checked; proof not verified). The qualitative statement was known before, from the density Hales–Jewett theorem; the paper's contribution is a combinatorial argument whose bound, though not stated, is at best of tower type.

Depends on. Nothing in this wiki.

Acceptance. Refereed publication: Combin. Probab. Comput. 13 (2004), no. 2, 263--267, doi:10.1017/S0963548303005959; the Crossref record dates the issue to March 2004, filled to the first of the month for this page's name (received 29 August 2002, revised 17 November 2002). Reviewed: the site's curator, Thomas Bloom, labels the problem proved and credits the quantitative proof to Solymosi in the problem page's commentary (accessed; empty proof-claim tab). A Lean 4 development, src/latest/ErdosProblems/Erdos658.lean of Boris Alexeev's lean-proofs repository (1,532 lines at the pinned commit of 2026-09-15, first added 2026-05-12), declares itself a formalization of this paper's Theorem 1.1: its header names Solymosi, Frankl and Rödl as informal authors and Aristotle (Harmonic) and John Jennings as formal authors, and its erdos_658 states the theorem over Finset (ℤ × ℤ) and [N]^2 with d ≠ 0, applying Theorem_1_1 to frankl_roedl_theorem, a theorem of the repository's Util.FranklRodl module derived from the repository's hypergraph removal development, not an axiom. The file records #print axioms output propext, Classical.choice and Quot.sound for Theorem_1_1 and Theorem_1_2 and no output for erdos_658. It grew from two gists that John Jennings posted on the site's thread on 2026-04-20 and 2026-04-21, the first conditional on the Frankl–Rödl theorem and the second stating it as an axiom; the formal-conjectures statement for the problem (pinned above at its commit of 2026-10-06, accessed 2026-10-07) is tagged solved and names line 1516 of the file, the theorem, as its formal proof. This corpus has not built the development, so the page lists no formalized evidence.