The board / graph theory / #765
Erdős Problem #765
SOLVED LEANdatabase updated 2026-05-16
Resolved in some way other than a straight proof or disproof — usual for open-ended questions, or for multi-part problems whose parts went different ways. A solution has also been checked by machine, in Lean.
What the community database records, not our verdict. erdosproblems.com no longer shows statuses (why).
Give an asymptotic formula for \(\mathrm{ex}(n; C_4)\). Erdős and Klein [Er38] proved \(\mathrm{ex}(n; C_4) \asymp n^{3/2}\), and Reiman [Re58] proved \[\frac{1}{2\sqrt 2} \le \lim \frac{\mathrm{ex}(n; C_4)}{n^{3/2}} \le \frac12.\] Erdős and Rényi [ERS66], and independently Brown [Br66], gave a construction showing that if \(n = q^2 + q + 1\) with \(q\) a prime power then \(\mathrm{ex}(n; C_4) \ge \frac12 q (q+1)^2\); together with Reiman's upper bound this gives \(\mathrm{ex}(n; C_4) \sim \frac12 n^{3/2}\). Füredi [Fu83] proved \(\mathrm{ex}(n; C_4) = \frac12 q (q+1)^2\) for \(q > 13\).
Statement as formalized in Formal Conjectures (Google DeepMind, Apache-2.0) · their label: research solved · 1 further variant / known partial result in the Lean file. The authoritative wording is on erdosproblems.com/765.Prizenone
Topicsgraph theory, turan number
Statement in LeanFormal Conjectures
Solution in Leanyes
OEISA006855
Original pageerdosproblems.com/765
Attempts
submit one →If you take a run at this one — with your own AI subscription or without — the guide says how, and the submission form gets you an honest read of what you found.