---

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 erdosproblems.com's $\{1,\ldots,N\}^2$ by a translation, and an axis-parallel square is a square, so the theorem gives erdosproblems.com'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 paper was received 29 August 2002 and revised 17 November 2002. The Crossref record dates the issue to March 2004, and the publisher's page gives the online publication as 3 March 2004, which dates this page.

Reviewed: the erdosproblems.com curator, Thomas Bloom, credits the quantitative proof to Solymosi in the problem page's commentary (accessed 2026-10-07) and labeled the problem proved; the proof-claim tab was empty.

A Lean 4 development declares itself a formalization of this paper's Theorem 1.1. It is src/latest/ErdosProblems/Erdos658.lean of Boris Alexeev's lean-proofs repository, first added 2026-05-12, with 1,532 lines at the pinned commit of 2026-09-15. Its header names Solymosi, Frankl and Rödl as informal authors and Aristotle (Harmonic) and John Jennings as formal authors. Its erdos_658 states the theorem over Finset (ℤ × ℤ) and [N]^2 with d ≠ 0. It applies Theorem_1_1 to frankl_roedl_theorem. That is a theorem of the repository's Util.FranklRodl module, derived from the repository's hypergraph removal development, and 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.

The development grew from two gists that John Jennings posted on the erdosproblems.com thread on 2026-04-20 and 2026-04-21. The first was conditional on the Frankl–Rödl theorem, and the second stated 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. It 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.