---

Zoltán Füredi, The maximum number of edges in a minimal graph of diameter 2, J. Graph Theory 16 (1992), no. 1, 81--98, doi:10.1002/jgt.3190160110 (issued March 1992; Crossref record, 2026-09-19, as the problem page records); the locators are the pages of IMA Preprint Series #408 (March 1988). The preprint is the first posting and its month supplies this page's date; no source cited here records the day. The journal text is not held and was not compared with the preprint.

The result. A graph on $n$ vertices is a minimal graph of diameter $2$ (Füredi's term) when its diameter is $2$ and deleting any edge spoils this. It is the graph of Problem 742, which asks whether such a graph has at most $n^2/4$ edges. Theorem 1.2 (preprint p. 2) states that the paper's Conjecture 1.1, attributed to Simon and Murty, is true for all $n>n_0$: a minimal graph of diameter $2$ on $n>n_0$ vertices has at most $\lfloor n^2/4\rfloor$ edges, with equality only for $K_{\lfloor n/2\rfloor,\lceil n/2\rceil}$. The paper says that $n_0$ is explicitly computable but that its proof yields only "a tower of 2's of height about 1000" (p. 2); no source cited here states a value. Section 3 proves $|E(G)|<(1+o(1))n^2/4$ for every $n$ by deleting $o(n^2)$ edges with the Ruzsa--Szemerédi theorem, Section 4 restores them, and Section 5 adds Theorem 5.1, that for $n>n_0$ a minimal graph of diameter $2$ with more than $\lfloor(n-1)^2/4\rfloor$ edges is complete bipartite or one exceptional non-bipartite graph. The statement is paged at Theorem 1.2, at read depth claims checked, with the proof for structure only.

Covers. Every $n>n_0$, for the inequality the site asks and for the equality clause it does not ask. The problem is thereby reduced to the finite check of the orders $n\le n_0$, which is the site's DECIDABLE label: the check settles the problem, since a yes for every $n\le n_0$ proves the bound for all $n$, and a minimal graph of diameter $2$ on some $n\le n_0$ vertices with more than $\lfloor n^2/4\rfloor$ edges disproves it. Of that remainder, Fan's Theorem (Discrete Math. 67 (1987), part (ii) with its Remark) settles the inequality for $n\le24$ and $n=26$, as Füredi attests on p. 1 (the accepted partial claim Fan 1987), so the unchecked orders are $25\le n\le n_0$ with $n\ne26$, and $n_0$ has no known value. The self-declared formalization of this theorem linked below is no evidence, and the pending proof claim for every $n$ has its own page; this page rests on neither.

Depends on. Nothing in this wiki; the proof is self-contained given the Ruzsa--Szemerédi theorem, which it cites.

Acceptance. Refereed: publication in the Journal of Graph Theory (volume 16, issue 1, March 1992, per the Crossref record, 2026-09-19). As context and not as evidence: the site's curator, Thomas Bloom, credits Füredi [Fu92] in the problem's commentary with the proof for all large $n$, and the site's label DECIDABLE, which the site defines as resolved up to a finite check, rests on that theorem; the label settles neither the problem nor a listed part of it, so the credit is no reviewed evidence. Also as context, the citing literature whose titles the problem page lists (a 2013 survey of progress on the Murty--Simon conjecture, a 2019 strengthening in Discrete Math.; titles) suggests no dispute of the theorem. Read depth: the statements named above; the proof (pp. 2--11) for structure only. Nothing is independently reviewed by this project, and the acceptance does not rest on this project's reading.

Formalization. The file src/latest/ErdosProblems/Erdos742.lean of Boris Alexeev's plby/lean-proofs repository, at the commit linked above, declares itself a formalization of this theorem: its header names Zoltán Füredi as the informal author, the Formal Conjectures authors as statement authors and Codex and GPT-5.6 Sol as formal authors, and describes the file as Füredi's sufficiently-large resolution of the Murty--Simon conjecture. Its main theorem erdos_742 (line 4279) states that there is an $n_0$ such that every diameter-$2$-critical graph on $n\ge n_0$ vertices has at most $\lfloor n^2/4\rfloor$ edges; its proof fixes constants and takes $n_0$ from an eventual statement, so no explicit threshold is available from it either. The formal-conjectures statement file ErdosProblems/742.lean points to this file from its furedi_bound declaration and is a statement, not a formalization link. This corpus has not built the development, printed its axioms or audited its criticality predicate against the problem statement. The development is therefore a link on this page and no formalized evidence.