Erdoes #742 - working report - Erdős Problem a Day

Erdős problem 742 — live audit, exact reductions, and computation

Accessed 2026-07-28. The notation used below is:

[a] elementary-rigorous: proved here from definitions.
[b] rigorous-modulo-named-theorem: the dependency is named and linked.
[c] plausible/structural-unverified: heuristic or extrapolation only.
[d] computational-only: exact code/instance, but no proof-producing UNSAT certificate is claimed.

0. Mandatory live-page gate

I fetched the Cloudflare-protected live page and its linked LaTeX, discussion, and history pages through the Bright Data browser path. The authoritative live page says DECIDABLE.

The current statement, verbatim from the page's LaTeX view, is:

Let $G$ be a graph on $n$ vertices with diameter $2$, such that deleting any edge increases the diameter of $G$. Is it true that $G$ has at most $n^2/4$ edges?

The page's listed information is:

It calls this a conjecture of Murty and Plesnik, notes the Murty--Simon/Ore

attribution reported by Füredi, and observes that complete bipartite graphs make the proposed bound sharp.

It says Füredi proved the assertion for sufficiently large $n$.
Its displayed references are L. Caccetta and R. Häggkvist, *On diameter

critical graphs, Discrete Math. 28 (1979), 223--229 (DOI90129-8)), and Z. Füredi, The maximum number of edges in a minimal graph of diameter 2*, J. Graph Theory 16 (1992), 81--98 (DOI).

The page reports 0 claimed proofs.
“Interested in collaborating” is None.
“Currently working on this problem” is None.
The sole comment is by

Terence Tao (2025-09-01): the sufficiently-large theorem leaves a finite, hence decidable, check, but the problem remains open.

Thus the mandatory stop condition did not fire: there is neither a claimed solution/falsification nor a current worker. [a: this is a direct page transcription, not a mathematical inference.]

1. Bottom line

I did not find a counterexample or a uniform proof. The useful outputs are:

an elementary exact local characterization of edge criticality, yielding a

compact SAT reduction; [a]

a standalone verifier with two independent definition checks, an exhaustive

labelled self-test, a nauty scan, and SAT search; [d]

a computational maximum $e(G)=49$ for order $n=14$, one order beyond the

most recent published exhaustive-search claim I found (but not beyond Fan's analytic theorem through $n=24$); [d]

an exact reduction of the first analytically unresolved order $n=25$ to

five instances: \[ e(G)=157,\qquad \Delta(G)\in\{13,14,15,16,17\}; \] [b]

a precise compute wall: even the apparently easiest reduced

$\Delta=17$ instance did not finish in 60 CPU seconds. [d]

The standalone code is erdos742_wavew012_verify.py.

2. Elementary structure used by the checker

Write $N(x)$ for the open neighborhood of $x$.

Lemma (local critical-edge witnesses)

Let $G$ have diameter at most $2$, and let $uv\in E(G)$. Then $\operatorname{diam}(G-uv)>2$ if and only if at least one of the following holds:

$N(u)\cap N(v)=\varnothing$;
there is a vertex $w$ with $vw\in E(G)$, $uw\notin E(G)$, and

$N(u)\cap N(w)=\{v\}$;

the symmetric version of (2), interchanging $u$ and $v$.

Proof. Conditions (1)--(3) plainly give, after deleting $uv$, a pair $(u,v)$, $(u,w)$, or $(v,w)$ with no path of length at most $2$. Conversely, suppose deleting $uv$ makes some pair $x,y$ farther than $2$. A path of length at most $2$ destroyed by deleting $uv$ must have $u$ or $v$ as an endpoint: a two-edge path whose endpoints are both outside $\{u,v\}$ cannot contain $uv$. If the affected pair is $u,v$, (1) holds. Otherwise it is, say, $u,w$, and its only former path of length at most $2$ was $u-v-w$, which is exactly (2). $\square$ [a]

This lemma is also a complete explanation of the SAT witness clauses; no graph-theory oracle is hidden in the encoding.

Two closed-form checked families

The balanced complete bipartite graph $K_{\lfloor n/2\rfloor,\lceil n/2\rceil}$ is diameter-2-critical and has $\lfloor n^2/4\rfloor$ edges. Its edges lie in no triangle, so deleting an edge makes its endpoints farther than $2$. [a]

There is also the known expanded-$C_5$ family. Replace three consecutive cycle vertices by nonempty independent bags of sizes $a,b,c$; retain the other two vertices as singleton bags; and put all edges between consecutive bags. Here

a+b+c+2=n,\qquad b\in\left\{\left\lfloor\frac{n-3}{2}\right\rfloor, \left\lceil\frac{n-3}{2}\right\rceil\right\}.

Every nonedge has a common neighbor, while the graph is triangle-free. Therefore it is diameter-2-critical. Its edge count is

ab+bc+c+1+a=(b+1)(a+c)+1 =\left\lfloor\frac{(n-1)^2}{4}\right\rfloor+1.

This is $\lfloor n/2\rfloor-1$ below the Murty--Simon bound. [a] The script directly checked every allowed $a,b,c$ through $n=25$, using both edge-deletion and local-witness implementations. [d]

3. Exact SAT projection

For each unordered pair $i,j$, the CNF has an edge variable $E_{ij}$.

Diameter at most $2$: for every $i,j$, require $E_{ij}$, or an

auxiliary $C_{ijk}$ implying both $E_{ik}$ and $E_{jk}$, for some $k$. The one-way Tseitin implications are sufficient and exact after projecting to edge variables.

Criticality: for every possible edge $uv$, require either the endpoint

witness or one of the two oriented witnesses in the lemma.

A sequential cardinality encoding imposes

$e(G)\ge\lfloor n^2/4\rfloor+1$ (and, when requested, an upper edge bound).

In maximum-degree branch $d$, vertex $0$ is fixed to have degree $d$,

its neighbors are $1,\ldots,d$, and every other vertex has degree at most $d$. Every graph in that branch has such a relabeling.

Permutations within $N(0)$ and outside $N[0]$ remain. The code chooses

the lexicographically least adjacency vector in each orbit by imposing $x\le_{\rm lex}\tau(x)$ for every within-part transposition $\tau$. A finite orbit always has such a least representative, so this loses no isomorphism class.

The lemma proves that an edge assignment extends to a CNF model exactly when it is a diameter-2-critical graph satisfying the selected numerical constraints. The maximum-degree and lex arguments prove that the branch union is exhaustive. [a] A solver's UNSAT answer itself remains [d] because I did not archive/check a DRAT/LRAT proof.

4. Reverification performed

Environment: Python 3.12.3, python-sat 1.9.dev7, nauty 2.8.8, CaDiCaL 1.9.5 through python-sat.

4.1 Exhaustive encoding self-test

Command:

python runs/erdos742_wavew012_verify.py selftest --max-n 6

For every one of the $2^{\binom n2}$ labelled graphs, the script:

deleted each edge and recomputed all distance-$\le2$ pairs from scratch;
applied the local lemma independently;
fixed every SAT edge variable and checked whether the auxiliaries could be

extended.

All three answers agreed. The numbers of labelled D2C graphs were:

| $n$ | labelled graphs checked | labelled D2C graphs | |---:|---:|---:| | 3 | 8 | 3 | | 4 | 64 | 7 | | 5 | 1,024 | 27 | | 6 | 32,768 | 571 |

[d]

4.2 Independent canonical scan through $n=10$

Command:

python runs/erdos742_wavew012_verify.py geng --min-n 3 --max-n 10

nauty-geng -c produced one canonical connected graph in every isomorphism class with more than $\lfloor n^2/4\rfloor$ edges. The script has its own graph6 decoder and its own D2C test. (I also cross-checked the first 1,000 decoded records against NetworkX; they agreed.)

| $n$ | first forbidden $m$ | canonical candidates | D2C candidates | |---:|---:|---:|---:| | 3 | 3 | 1 | 0 | | 4 | 5 | 2 | 0 | | 5 | 7 | 8 | 0 | | 6 | 10 | 32 | 0 | | 7 | 13 | 239 | 0 | | 8 | 17 | 2,462 | 0 | | 9 | 21 | 59,707 | 0 | | 10 | 26 | 2,328,166 | 0 |

Total: 2,390,617 canonical candidates, with none D2C. [d]

4.3 SAT maximum at $n=14$

For a counterexample at $n=14$, handshaking gives $\Delta\ge\lceil 2(50)/14\rceil=8$. All maximum-degree branches returned UNSAT:

| $\Delta$ | variables | clauses | CaDiCaL seconds | result | |---:|---:|---:|---:|:---| | 8 | 6,978 | 42,483 | 110.588 | UNSAT | | 9 | 7,026 | 42,933 | 124.096 | UNSAT | | 10 | 7,098 | 43,621 | 43.143 | UNSAT | | 11 | 7,194 | 44,547 | 1.403 | UNSAT | | 12 | 7,158 | 45,555 | 0.067 | UNSAT | | 13 | 7,458 | 47,282 | 0.033 | UNSAT |

The total solver time was 279.330 seconds. The separately checked $K_{7,7}$ has 49 edges, so the computed maximum is exactly 49. [d] The same branch method returned no counterexample at $n=11,12,13$, while the nauty scan covers $n\le10$. [d]

This computation is an independent verification, not a new theorem: Fan's 1987 theorem already covers every $n\le24$. [b]

5. Literature audit

Fan proved the conjectured bound for $n\le24$ and $n=26$, and for

$n\ge25$ proved the strict inequality \[ e(G)<\frac{n^2}{4}+\frac{n^2-16.2n+56}{320}. \] This is quoted with the formula in the primary-source manuscript Wang--Wang--Yu, arXiv:1205.4397 and is bibliographically the 1987 paper (DOI90174-9)). [b]

Füredi proved the conjecture for $n>n_0$, with the reported explicit

$n_0$ bounded by roughly a tower of twos of height $10^{14}$. Thus this is a genuine finite reduction, but not a practical enumeration. The publisher record and the later primary papers agree on the sufficiently-large result. [b]

Dailly, Foucaud, and Hansberg's 2019 paper

(arXiv:1812.08420, DOI) records: triangle-free graphs and graphs with a dominating edge satisfy the conjecture; any D2C graph with a dominating edge satisfies the sharp bound; and their computer search treated graphs through order 11. [b]

Haynes, Henning, van der Merwe, and Yeo prove the conjecture when

$\Delta\ge0.7n$ (and improve $0.7$ for $n\ge2000$) in A maximum degree theorem for diameter-2-critical graphs. [b]

Wang, Wang, and Yu prove it when the complement has diameter 3

(arXiv:1205.4397); their sequel proves it for complements of vertex connectivity $1,2,3$ and some independent cuts (arXiv:1301.0460). [b]

Radosavljević's 2023 paper

Diameter-2-critical graphs with at most 13 nodes claims a full nauty-based list through $n=13$. There is an internal inconsistency: its Table 3 prints maximum D2C size $37$ at $n=13$, but $K_{6,7}$ is D2C with 42 edges. The standalone direct checker verifies $K_{6,7}$ from the definition. This could be a reporting/table error, so I do not infer that the entire enumeration is wrong, but I also do not use that table as a certificate. [a for the contradiction; source reliability diagnosis only.]

The 2024 paper Primitive diameter 2-critical graphs

(DOI) reports an order-12, 32-edge exception to a stronger second-extremal conjecture. It is not a counterexample here: $32<12^2/4=36$, and it has a dominating edge. [b]

arXiv:2409.17491 (Wang--Zhang--Zhu,

2024) exists and explicitly still states Murty--Simon as a conjecture; its new general bound concerns diameter $k\ge3$, not this $k=2$ case. [b]

Lin and Wang (2025,

DOI) prove that a sufficiently large $C_5$-free D2C graph with at least $\lfloor(n-1)^2/4\rfloor+1$ edges is complete bipartite. This is another structural partial result, not a solution of the unrestricted finite range. [b]

I found no primary source claiming a resolution, consistent with the live page's current status.

6. Exact first-open-order reduction

Fan covers $n\le24$ and $n=26$, so the first order not covered by that theorem is $n=25$. Substitution into Fan's strict bound gives

e(G)<156.25+\frac{625-405+56}{320}=157.1125.

A counterexample has $e(G)\ge157$, hence it must have exactly 157 edges. [b]

The maximum-degree theorem rules out $\Delta\ge0.7(25)=17.5$, hence $\Delta\le17$. Handshaking gives

\Delta\ge\left\lceil\frac{2e}{25}\right\rceil =\left\lceil\frac{314}{25}\right\rceil=13.

Therefore the first unknown order is precisely the union of the five cases

(n,e,\Delta)=(25,157,d),\quad d=13,14,15,16,17.

[b: Fan + maximum-degree theorem; handshaking is elementary.]

Moreover, standard solved classes let us require that a counterexample contains a triangle and has no dominating edge. The --reduced switch adds exactly those two constraints. [b]

The resulting CNF sizes are:

| $\Delta$ | variables | clauses | |---:|---:|---:| | 13 | 85,085 | 506,986 | | 14 | 85,154 | 507,625 | | 15 | 85,269 | 508,722 | | 16 | 85,430 | 510,277 | | 17 | 85,637 | 512,290 |

Example reproduction command:

timeout 60s python runs/erdos742_wavew012_verify.py sat 25 \
  --min-edges 157 --max-edges 157 --max-degree 17 \
  --reduced --solver cadical195

That command timed out after 60.01 wall seconds / 59.83 CPU seconds, using 247,928 KB peak RSS. It returned neither SAT nor UNSAT. [d]

7. Precise wall and what is missing

The exact finite lemma missing at the first open order is:

No 25-vertex diameter-2-critical graph with 157 edges and maximum degree $13,14,15,16,$ or $17$ exists.

Proving this would settle $n=25$, but would not close the problem: orders $27\le n\le n_0$ would remain. Uniform closure needs either a regularity-free density lemma for the remaining class (non-bipartite, triangle-containing, no dominating edge, $\Delta<0.7n$, with the relevant critical complement structure), or certified finite checks throughout the enormous Füredi range. [b]

Why the standard routes stop is now concrete:

Mantel handles only triangle-free graphs.
Total-domination/dominating-edge machinery handles that special class.
The maximum-degree theorem stops below $0.7n$.
Fan misses the target by one edge at $n=25$.
The attractive average-edge-degree inequality was disproved by Loh and Ma

(arXiv:1406.6736).

Füredi's regularity argument is uniform only beyond a tower-type threshold.
Generic canonical generation grows disastrously: the 2023 computation

reports about 43,718 sequential seconds already for all connected graphs at $n=12$, and more than a month for its $n=13$ run.

The present counterexample-specific SAT encoding is fast through $n=14$

but already stalls at $n=15$ in low-degree branches and at $n=25$ in a high-degree reduced branch. [d]

A defensible next computation is a proof-logging portfolio run on the five $n=25$ instances, initially capped at 24 core-hours each: 120 core-hours, about US$6 at a representative US$0.05/core-hour, before storage and proof checking. This is an exploratory budget, not a completeness estimate. [c] Naively extrapolating the observed hardest-branch growth $2.3\text{s}\to20\text{s}\to124\text{s}$ for $n=12,13,14$ by even a factor six per additional vertex gives roughly $1.25\times10^7$ core-hours for one $n=25$ branch (about US$625,000 at the same rate). Solver scaling is too instance-sensitive for that figure to be more than a warning. [c]

8. Reproduction summary

# Syntax and complete small encoding audit
python -m py_compile runs/erdos742_wavew012_verify.py
python runs/erdos742_wavew012_verify.py selftest --max-n 6

# Closed-form constructions
python runs/erdos742_wavew012_verify.py construction --max-n 25

# Independent canonical scan
python runs/erdos742_wavew012_verify.py geng --min-n 3 --max-n 10

# Full maximum-degree branch union at one order (n=14 takes several minutes)
python runs/erdos742_wavew012_verify.py certify 14

# First open-order branch, with all safe structural reductions used here
python runs/erdos742_wavew012_verify.py sat 25 \
  --min-edges 157 --max-edges 157 --max-degree 17 --reduced

No conjectural construction, solver timeout, or small-$n$ list is promoted to a theorem, and no claim of closure is made.

PARTIAL: Exact reproducible checks find no counterexample through n=14 and reduce the first open order n=25 to five SAT instances (maximum degree 13 through 17); the uniform conjecture remains open.

This is the AI working report, labelled by outcome — not an independently verified claim unless marked PROVED. ← ledger