---

A proof claim submitted on 2026-08-05 to the site's proof-claim tab by the account jstar, with a write-up and a Lean file in a public repository linked from the submission (the tab accessed 2026-09-19 and 2026-10-06). The submitter states that the mathematics, the Lean proof and the summary were all generated by AI systems, naming Fable 5 and Opus 5, and that the submitter could not validate the proof. The write-up's author line reads "Claude Code", and its opening says the proof was found, written and formalized by a multi-agent AI research campaign it names as Claude (Anthropic). The claimant recorded on this page is the submitter, since the publication's author line names an AI system and no person. The site states that a listing on the tab is no guarantee of correctness and that nobody associated with the site has examined the proof.

Submission note. Posted to erdosproblems.com as a proof claim by jstar (account jstar) on 5 August 2026, giving "Fable 5, Opus 5" as the AI used:

The key step is a reformulation: define the deficiency $D(F)=|E_{0}|+|E_{w}|-|A|$, where $E_{0}$ counts edges whose endpoints have no common neighbor, $E_{w}$ counts edges having a witness (a vertex whose only common neighbor with one endpoint is the other), and $A$ counts non-adjacent pairs with a common neighbor; criticality and diameter $2$ force $D(G)=2e-\binom{n}{2}$, making the bound equivalent to $D(G)\le\lfloor n/2\rfloor$. The significant point is that this holds for all graphs (with equality exactly at balanced complete bipartite graphs), which permits induction by deleting the two endpoints of a well-chosen edge --- one needs a single edge whose deletion raises $D$ by at most $1$. A codegree-$0$ edge always works; otherwise a local supply/demand ledger of witness configurations reduces everything to one global counting inequality, proved by an explicit injection of demand units into pairwise-disjoint pools of supply slots. Notes: Everything (the mathematics, the Lean proof, the short summary) was AI-generated. I don't have the background to validate the proof myself, so I apologize if it's incorrect or if anything is missing

The claim. The answer to Problem 742 is yes for every $n$: a graph on $n$ vertices of diameter $2$ in which deleting any edge increases the diameter has at most $\lfloor n^2/4\rfloor$ edges. The route, in this page's words from the write-up (sections 1.2 to 1.4). For a graph $F$ on $n$ vertices let $D(F)$ be the number of edges $uv$ with $N(u)\cap N(v)=\emptyset$, plus the number of edges $uv$ with $N(u)\cap N(v)\ne\emptyset$ that have a witness, a vertex $y\ne u$ not adjacent to $u$ with $N(u)\cap N(y)=\{v\}$ (or the same with $u$ and $v$ exchanged), minus the number of non-edges $\{x,y\}$ with $N(x)\cap N(y)\ne\emptyset$. For a critical graph $G$ of diameter $2$ with $e$ edges, $D(G)=2e-\binom n2$, so the bound is equivalent to $D(G)\le\lfloor n/2\rfloor$. The claim is that $D(F)\le\lfloor n/2\rfloor$ for every graph $F$ on $n$ vertices (attained by balanced complete bipartite graphs and by perfect matchings; the write-up characterizes no equality case), by induction on $n$: both ends of an edge are removed, the edge chosen so that $D$ grows by at most $1$. Such an edge is at hand whenever two adjacent vertices share no neighbor; failing that, the witness configurations near a candidate edge are counted and the step reduces to one inequality between two of these counts, established by an injection from one side into the other. The write-up claims the bound for every $n$, says that no step closes by exhaustion, and says that it does not prove the equality clause; the write-up is linked at the commit of 5 August 2026 that added it, the commit after the one the submission pins for the Lean file; its text is unchanged at the repository's head commit of 10 August 2026, accessed 2026-10-07. A comment on the tab of 2026-08-05 stated that the problem was already solved and asked the submitter to summarize what was new; the comment refers, in this page's reading, to the large-$n$ theorem. The submitter answered on 2026-08-10 that the equality clause also follows and linked a second write-up and a second Lean file for it on the repository's main branch.

Depends on. Nothing in this wiki; the argument as summarized is self-contained.

Standing. Claimed: the submission is pending on the site's tab with two comments and no review, the site's label and commentary are unchanged, no other posting of the result was found in the search, this corpus has reviewed neither the write-up nor the Lean file and has built neither, and the claim is not refereed. The Lean file's statement is unaudited by this corpus, so the formalization is a posting of the claim and not evidence. If correct, the claim would close the finite remainder that Füredi's theorem leaves and would prove the bound for every $n$ by a different argument.