---

Claim. Let $f(n)$ be the maximum number of edges of a graph on $n$ vertices containing no quadrilateral, that is, no cycle of length four. Then

$$\lim_{n\to\infty}\frac{f(n)}{n^{3/2}}=\frac12,$$

so $\operatorname{ex}(n;C_4)=(\tfrac12+o(1))n^{3/2}$. This is the statement of Section 3, "Graphs without quadrangles", of W. G. Brown, On graphs that do not contain a Thomsen graph, Canad. Math. Bull. 9 (1966), no. 3, 281--285 (received 7 February 1966; issue 3, August 1966, the month this page's name uses), printed pp. 284--285. Brown cites Kővári, Sós and Turán for $\limsup f(n)n^{-3/2}=\tfrac12$ and supplies the matching lower bound by a construction: for each odd prime $q$, the graph whose vertices are the points of $PG(2,q)$, two distinct points joined when their coordinate triples have zero dot product; $q^2$ of its vertices have degree $q+1$ and $q+1$ have degree $q$, so it has $q^2+q+1$ vertices and $\tfrac12(q^2+q+1)^{3/2}+O(q^2)$ edges and no quadrilateral, the last check left to the reader. Brown records that the construction was also found independently by Rényi, Sós and Erdős, in a paper then forthcoming; that paper, Erdős, Rényi and Sós (1966), records in its footnote on p. 219 that Brown proved its (1.12), the asymptotic, independently and in the same way. The paper's source card has a digest that records the Section 3 statement; its paged result, the main theorem, is the paper's $K_{3,3}$ construction of Section 2.

For Problem 765, which asks for an asymptotic formula for $\operatorname{ex}(n;C_4)$, this is the formula, the same as Corollary 2 of Erdős, Rényi and Sós on their claim page, proved independently by the same polarity-graph construction; the passage from the prime orders $q^2+q+1$ to every large $n$ is not written out in Brown's Section 3, which states the limit and the construction.

Acceptance. Refereed: Canadian Mathematical Bulletin. Reviewed: the site's curator, Thomas Bloom, labels the problem SOLVED (LEAN) and, in the problem's commentary, credits the construction to Erdős and Rényi and, independently, to Brown, and records that with Reiman's upper bound it gives $\operatorname{ex}(n;C_4)\sim\tfrac12n^{3/2}$; Erdős, Rényi and Sós's footnote records Brown's independent proof; Füredi (1983) and Ma and Yang (2023) credit the independent proof to Brown in refereed papers. This corpus supplies no independent proof review; Brown leaves the quadrilateral-free check of his construction to the reader.

Formalization. The file src/latest/ErdosProblems/Erdos765.lean of Boris Alexeev's plby/lean-proofs repository, linked above at a pinned commit, names István Reiman, Paul Erdős, Alfréd Rényi and W. G. Brown as its informal authors, following the exposition of Aigner and Ziegler, and Aristotle and Jeremy Tan Jie Rui as its formal authors; it is therefore a link on this page and on the page of Erdős, Rényi and Sós, which describes its statement, its origin in a gist of 16 May 2026 and what it reports about its axioms. The file adapts that gist, posted with the thread announcement of 16 May 2026 and linked above. This corpus has not built or audited it, so this page lists no formalized evidence.