Erdős problem 813 — wave w015

Date: 2026-08-12 UTC (original finite report 2026-07-28; exact order-18 computation added 2026-08-12)

Claim labels used throughout:

• [A] elementary-rigorous: a complete mathematical argument is given here.
• [B] rigorous-modulo-named-theorem: the deduction is complete assuming the cited published theorem.
• [C] plausible/structural-unverified: explicitly not asserted as a theorem.
• [D] computational-only: established by the supplied finite computation, without a separately checked proof certificate.

0. Mandatory live-page gate

[D, live-page observation] I refreshed <https://www.erdosproblems.com/813> through the Bright Data browser path on 2026-08-12 UTC. The live page still said OPEN, with 0 comments, 0 claimed proofs, and nobody listed as currently working or interested in collaborating. The original 2026-07-28 gate displayed:

0 comments on this problem

0 claimed proofs for this problem

Likes this problem	None
Interested in collaborating	None
Currently working on this problem	None
This problem looks difficult	None
This problem looks tractable	None

Thus the requested stop condition did not apply. The page also listed “Additional thanks to: Zach Hunter.”

Verbatim live statement

The site's “View the LaTeX source” endpoint, <https://www.erdosproblems.com/latex/813>, gave the following exact statement:

Let $h(n)$ be minimal such that every graph on $n$ vertices where every set of $7$ vertices contains a triangle (a copy of $K_3$) must contain a clique on at least $h(n)$ vertices. Estimate $h(n)$ - in particular, do there exist constants $c_1,c_2>0$ such that\[n^{1/3+c_1}\ll h(n) \ll n^{1/2-c_2}?\]

The exact known-results text at that endpoint was:

A problem of Erd\H{o}s and Hajnal, who could prove that\[n^{1/3}\ll h(n) \ll n^{1/2}.\]Buci\'{c} and Sudakov \cite{BuSu23} have proved\[h(n) \gg n^{5/12-o(1)}.\]

The main page attributed the problem to [Er91] and, after expanding that reference, displayed:

[Er91] Erdős, P., Problems and results in combinatorial analysis and combinatorial number theory. Graph theory, combinatorics, and applications, Vol. 1 (Kalamazoo, MI, 1988) (1991), 397-406. (MR 1170793)

The LaTeX page listed:

[BuSu23] M. Buci\'C and B. Sudakov, Large independent sets from local considerations. arXiv:2007.03667 (2023).

1. Literature audit

[B] The cited paper exists as Matija Bucić and Benny Sudakov, Large Independent Sets from Local Considerations, Combinatorica 43 (2023), 505–546, DOI 10.1007/s00493-023-00023-w, arXiv:2007.03667. Its Theorem 1.3 says that every \(n\)-vertex graph \(H\) with \(\alpha _7(H)\ge3\) has \(\alpha(H)\ge n^{5/12-o(1)}\). This is exactly the live page's lower bound after taking graph complements.

[B] The same paper's Question 4.2 asks whether such a graph always has \(\alpha(H)\ge n^{1/2-o(1)}\). Immediately before it, the authors say their method has a natural limit \(n^{3/7}\), that pushing beyond \(5/12\) should be possible, and that breaking \(3/7\) seems to require new ideas. The author-hosted current thesis copy by Bucić repeats the same question and the same \(5/12\) result.

[C] I searched exact statement phrases, the paper title, arXiv, and the later-citation lists returned by OpenAlex and Semantic Scholar. I opened the primary arXiv/publisher versions of the later mathematically adjacent hits. I found no later paper claiming an improved exponent for the specific \((m,r)=(7,3)\) problem. This is an honest search miss, not a proof that no such paper exists.

[D, bibliographic observation] I verified the [Er91] bibliographic record through the live page and secondary bibliographies, but did not locate an accessible full scan of that exact 1991 proceedings article. I therefore make no claim about wording in [Er91] beyond the live page's quotation and attribution.

One additional primary source is used below:

[B] K. Piwakowski, S. P. Radziszowski, and S. Urbański, Computation of the Folkman Number \(F_e(3,3;5)\), Journal of Graph Theory 32 (1999), 41–49 (author PDF), proves as Theorem 4 that

The paper explicitly describes its computer enumeration and reports that the graph-specific programs were independently implemented by two authors.

2. Exact reformulations

For a graph \(G\), define

[A] The live condition “every seven vertices contain a triangle” is exactly \(\alpha_3(G)\le6\). Hence

[A] If \(H=\overline G\), a triangle in \(G\) is an independent triple in \(H\), and a clique in \(G\) is an independent set in \(H\). Therefore

which is exactly the Bucić–Sudakov local-to-global independence function \(f(n,7,3)\).

[A] If \(\tau_\triangle(G)\) is the minimum number of vertices meeting every triangle, then complements of triangle transversals are precisely triangle-free induced sets. Consequently

[A] The condition is hereditary under taking induced subgraphs of order at least seven. It follows that \(h(n)\) is nondecreasing for \(n\ge7\).

3. Verified finite result

The main concrete result of this run is:

The support and classification are:

3.1 The 12-vertex construction

Let \(I_{12}\) be the graph on \(\{0,\ldots,11\}\) with edge set

(0,1) (0,5) (0,7) (0,8) (0,11)
(1,2) (1,5) (1,6) (1,8)
(2,3) (2,6) (2,8) (2,9)
(3,4) (3,6) (3,9) (3,10)
(4,5) (4,6) (4,10) (4,11)
(5,6) (5,11)
(7,8) (7,9) (7,10) (7,11)
(8,9) (9,10) (10,11)

This is the usual icosahedral graph in one labelling.

[D] Direct enumeration checks that it has 30 edges, is 5-regular, has 20 triangles, has clique number \(3\), and has maximum triangle-free induced set order \(6\). For example, \(\{0,1,5\}\) is a triangle and \(\{0,1,2,3,4,7\}\) is triangle-free. Every one of its \(\binom{12}{7}=792\) seven-sets contains a triangle. Its induced prefixes of orders \(7,\ldots,12\) therefore prove \(h(n)\le3\) on that interval.

3.2 Why order 13 forces a \(K_4\)

There are two independent routes.

Published-theorem route [B]. Suppose a valid 13-vertex graph \(G\) were \(K_4\)-free. In every red/blue vertex colouring of \(G\), one colour class has at least seven vertices, so that class contains a triangle. Thus \(G\to(3,3)^v\). This would be a \(K_4\)-free vertex Folkman graph of order 13, contradicting \(F_v(3,3;4)=14\). Hence every valid 13-vertex graph has a \(K_4\).

Independent finite replication [A setup, D outcome]. In a \(K_4\)-free graph, \(G[N(v)]\) is triangle-free for every vertex \(v\). The local condition therefore forces \(d(v)\le6\), since seven neighbours would form a triangle-free seven-set. A valid graph contains a triangle, so its maximum degree is at least two. Choose a maximum-degree vertex, relabel it as \(0\), and relabel its neighbourhood as \(\{1,\ldots,d\}\). The five cases \(d=2,3,4,5,6\) are exhaustive.

For each case the checker builds a CNF with:

• \(e_{ij}\) for every pair and \(t_{ijk}\) for every triple;
• four clauses imposing

\(t_{ijk}\leftrightarrow(e_{ij}\wedge e_{ik}\wedge e_{jk})\);

• for every seven-set, one clause saying that one of its 35 triangle

variables is true;

• for every four-set, one clause saying that one of its six edges is absent;
• unit clauses fixing \(N(0)=\{1,\ldots,d\}\);
• for every vertex and every \(d+1\) incident edges, a clause saying at

least one is absent.

The variable count is \(\binom{13}{2}+\binom{13}{3}=364\). In the final cross-check run, two distinct CDCL implementations gave (wall times naturally vary slightly):

[D] These are reproducible solver outcomes, not embedded DRAT/LRAT proofs. They independently replicate the stronger statement that no 13-vertex \(K_4\)-free graph has \(\alpha_3\le6\). The published Folkman theorem supplies the separate [B] justification.

3.3 The 17-vertex construction

Define \(W_{17}\) by adjacency masks. Bit \(j\) of row \(i\) is one exactly when \(ij\) is an edge:

i : neighbour mask (hex)
 0: 1f92e    1: 1ce19    2: 172f1    3: 13ef3    4: 031ee
 5: 06b9d    6: 1b31c    7: 05d3c    8: 0bcf1    9: 1d46e
10: 0fb8a   11: 0c5ab   12: 0c7dd   13: 1857d   14: 11ea7
15: 13f43   16: 0e24f

[D] The standard-library checker verifies symmetry and absence of loops, then checks all subsets directly. The graph has 84 edges, 146 triangles, \(\omega(W_{17})=4\), and \(\alpha_3(W_{17})=6\). Explicit witnesses are the \(K_4\) on \(\{0,1,3,11\}\) and the triangle-free six-set \(\{0,1,2,4,8,9\}\). All \(\binom{17}{7}=19,448\) seven-sets contain a triangle. The induced prefixes on \(13,\ldots,17\) all have clique number four, proving the required upper bounds.

3.4 The order-18 upper construction

Define \(W_{18}\) by:

 0: 179de    1: 21ffd    2: 273bb    3: 34457    4: 3ed8f
 5: 3c6c6    6: 1afab    7: 1ea77    8: 33e57    9: 2c5e6
10: 3ab7a   11: 1b5d3   12: 18907   13: 20dd5   14: 382bd
15: 35ef0   16: 2ddf9   17: 1e73e

[D] Direct enumeration gives 100 edges, 223 triangles, \(\omega(W_{18})=5\), and \(\alpha_3(W_{18})=6\). The vertices \(\{0,1,2,3,4\}\) form a \(K_5\), no \(K_6\) exists, and all \(\binom{18}{7}=31,824\) seven-sets contain a triangle. Thus \(h(18)\le5\).

This supplies the upper half of the exact value proved in Section 3.8.

3.5 A complete neighbourhood reduction at order 18

The first 2026-08-12 computation substantially narrowed the order-18 case:

This conclusion is [D]: two independent SAT solvers agree on every finite case, but no DRAT/LRAT proof logs were retained.

Let \(\mathcal C_d\) be the isomorphism classes of \(d\)-vertex graphs which are \(K_4\)-free and have \(\alpha_3\le6\). A complete hereditary census gives

Here is the exact augmentation criterion. Given \(H\in\mathcal C_d\), add a new vertex with neighbourhood \(A\subseteq V(H)\). The child lies in \(\mathcal C_{d+1}\) if and only if:

1. \(A\) is triangle-free, so the new vertex creates no \(K_4\); and
2. for every triangle-free six-set \(S\) in \(H\), \(A\cap S\) contains an

edge, so \(S\) together with the new vertex is not triangle-free.

This is an elementary equivalence, and it enumerates every child because both defining properties are induced-hereditary. The original C producer found 3,989 valid labelled extensions from the 9,133 order-10 parents, canonicalising to 403 order-11 types; 16 extensions then canonicalised to 8 order-12 types; and those 8 have no valid extension. An independent Python implementation rebuilt these transitions directly from the two conditions and matched every canonical graph6 file byte-for-byte:

TRANSITION 9133->403: valid_labelled_extensions=3989  PASS COMPLETE
TRANSITION 403->8:    valid_labelled_extensions=16    PASS COMPLETE
TRANSITION 8->0:      valid_labelled_extensions=0     PASS COMPLETE

As an augmentation-independent anchor, nauty-geng generated all 12,005,168 unlabeled graphs of order 10. Direct definition filtering left 9,133, and canonicalising that list produced exactly the same file as the augmentation census, with SHA-256

234be06b2b8dbadec010e95ec0f62fffbe936a21207654f521742c063321ff0c

Now suppose \(G\) is an 18-vertex witness. For every vertex \(v\), the neighbourhood graph \(G[N(v)]\) is \(K_4\)-free (otherwise \(v\) completes a \(K_5\)) and has \(\alpha_3\le6\). Thus a degree-\(d\) neighbourhood is one of the members of \(\mathcal C_d\).

For each of all 403 order-11 and all 8 order-12 representatives, the check rebuilt the natural 18-vertex formula directly from the definition. It has 153 edge variables and 816 triangle variables, forbids a \(K_5\), requires a triangle in every seven-set, fixes one vertex's neighbourhood, and fixes the induced neighbourhood representative. It does not assume a maximum degree. CaDiCaL 1.9.5 and Kissat 4.0.4 independently returned UNSAT for all 411 formulas. The degree-11 CaDiCaL run used 34,864,416 conflicts and 2,307.669 aggregate solver-seconds; Kissat used 1,621.060 aggregate solver-seconds. The eight degree-12 cases were small. Since \(\mathcal C_{13}\) is empty, degrees at least 13 are impossible as well. Therefore every hypothetical witness has \(\Delta\le10\), modulo those finite solver results.

The certificate distinction is essential: the census has an independent definition-level audit and a full order-10 control, while the final 411 UNSAT verdicts are two-solver assertions rather than independently replayable proof certificates.

3.6 A theorem at the other end: every candidate has \(\Delta\ge7\)

The complementary lower-degree reduction is rigorous modulo Brooks' theorem:

Suppose instead that \(\Delta(G)\le6\). A proper coloring with at most five colors has two largest color classes whose union contains at least \(\lceil36/5\rceil=8\) vertices. That union is bipartite, hence triangle-free, contradicting the seven-set condition. Thus \(\chi(G)\ge6\).

Apply Brooks' theorem componentwise. A nonexceptional component is 6-colorable; a complete component has order at most four because \(G\) is \(K_5\)-free; and an odd-cycle component is 3-colorable. A common palette of six colors therefore gives \(\chi(G)\le6\), so \(\chi(G)=6\).

Fix a proper six-coloring with class sizes \(c_1,\ldots,c_6\). Every union of two classes is triangle-free, so \(c_i+c_j\le6\). Summing all fifteen inequalities gives equality on both sides:

Hence every pair sum is six and all six color classes have size three.

Choose \(z\in C_1\). For each pair \(C_i,C_j\) of the other five classes, the seven-set \(\{z\}\cup C_i\cup C_j\) contains a triangle. Properness forces that triangle to be \(zxy\), with one vertex from each class. Thus \(z\) has a neighbor in every other class, and every pair of those five classes has adjacent neighbors of \(z\). Since \(d(z)\le6\), the neighbor counts are either \((1,1,1,1,1)\) or a permutation of \((2,1,1,1,1)\). In the first case the five neighbors form a \(K_5\). In the second, the four unique neighbors from the singleton classes form a \(K_4\), which together with \(z\) is a \(K_5\). Both contradict the hypothesis.

An independent standard-library audit exhausts the finite steps: all 7,315 five-class size vectors; the unique feasible six-class vector \((3,3,3,3,3,3)\); all six possible neighbor-count vectors; and all 406 cross-class edge patterns covering the ten class pairs. Every last pattern contains the asserted \(K_4\).

Combining this theorem with the two-solver upper reduction gave the intermediate window

for every hypothetical \(h(18)=4\) witness. The lower inequality is rigorous modulo Brooks; the upper inequality retains the computational certificate caveat stated above. Section 3.8 exhausts this window.

3.7 A nine-defect near miss

Local search found the following 18-vertex graph, in hexadecimal adjacency masks:

2575c 3c53c 30fe3 1df83 3ee43 3e1c6
17b35 37e2c 0bc6f 298dd 2699f 1a7dc
2e3c9 2ddf0 134fb 33b3a 0c8fe 0b6b7

A dependency-free audit finds 96 edges, 180 triangles, clique number 4, no \(K_5\), and exactly nine triangle-free seven-sets. Its degree sequence is \(10^6 11^{12}\). It is not a witness: all nine defects matter. Exact SAT found no true witness within seven edge flips, but that bounded search is diagnostic only and gives no global lower bound.

3.8 Exact exhaustion of the degree window

The final computation excludes every degree in the intermediate window and therefore establishes

This conclusion is [D: computer-assisted; solver assertions]. The combinatorial reductions, CNF semantics, canonical censuses, and exact case coverage have independent definition-level audits. Selected difficult cases also have independently replayed DRAT proofs. The complete millions-of-cases sweeps, however, retain solver verdict logs rather than an UNSAT proof for every branch. Thus (5) is an exhaustive, reproducible computational result, not a single end-to-end proof-certificate-verified theorem.

Choose a maximum-degree vertex \(v\), put \(d=d(v)\), \(H=G[N(v)]\), and \(M=G-N[v]\). Section 3.6 gives \(d\ge7\). Section 3.5 already excludes \(d\ge11\) with two solvers, so it remains to exhaust \(7\le d\le10\).

If four vertices \(A\subseteq N(v)\) were independent, then any two \(x,y\in M\) would have to be adjacent: otherwise \(\{v\}\cup A\cup\{x,y\}\) would be a triangle-free seven-set. Hence \(M\) would be a clique. Since the graph is \(K_5\)-free, this would force \(|M|\le4\), or \(d\ge13\), a contradiction. Therefore

For \(d\ge9\), the \(K_4\)-free graph \(H\) contains an independent triple by \(R(4,3)=9\). If \(M\) also contained an independent triple, those six vertices together with \(v\) would be triangle-free. Thus

For completeness, \(R(4,3)=9\) needs no black-box table here. If the complement of a nine-vertex \(K_4\)-free graph had neither a triangle nor an independent four-set, every degree would be at most three. A vertex of degree at most two and the standard \(R(3,3)=6\) argument among its non-neighbours would give an independent four-set. The complement would therefore be 3-regular on nine vertices, contradicting the handshaking lemma.

For each \(d\), the exact CNF relabels \(v\) as 0 and fixes \(N(0)=\{1,\ldots,d\}\). It contains the natural 153 edge variables and 816 triangle variables, forbids every \(K_5\), requires a triangle in every seven-set, and gives every vertex degree at most \(d\) through private sequential counters. An independent checker reconstructs all 43,656 natural clauses and exhaustively projects each counter on all \(2^{17}\) incident-edge assignments. Hence the four formulas are exact maximum-degree branches, not heuristic symmetry restrictions.

Definition filtering and canonicalisation leave the following complete splits. The two dimensions for \(d=9,10\) independently fix the induced graphs on \(M\) and \(H\); cross-edges remain unconstrained. Every listed \(H\)-type lies in the complete census \(\mathcal C_d\) from Section 3.5 (so it is \(K_4\)-free and has \(\alpha_3(H)\le6\)) and also satisfies \(\alpha(H)\le3\). Every listed \(M\)-type is \(K_5\)-free and satisfies \(\alpha(M)\le2\).

Persistent CaDiCaL 1.9.5 solved the branches under signed assumptions. Its learned clauses remain consequences of the common base. Separate coverage auditors parse every output record and verify exact, duplicate-free coverage:

d=7:  unique_cases=353       expected=353       all_UNSAT=YES
d=8:  unique_cases=1829      expected=1829      all_UNSAT=YES
d=9:  unique_pairs=1566787   expected=1566787   all_UNSAT=YES
d=10: unique_pairs=616848    expected=616848    all_UNSAT=YES

The order-7 non-neighbour census was also checked directly against all \(2^{21}\) labelled graphs. The order-8 census was regenerated both by direct definition filtering and by complementing all triangle-free order-8 types with independence number at most four; the canonical sets agree. Fresh nauty-geng runs reproduce the parent neighbourhood censuses at orders 7, 8, and 9, while the earlier audit directly filtered all 12,005,168 unlabeled order-10 graphs. As solver-path controls, one difficult branch at each degree 7 through 10 was materialised as a standalone formula, solved independently by Kissat, and successfully replayed with drat-trim.

There is now no possible maximum degree: at most six is excluded by the human colouring proof, 7 through 10 by the exact sweeps, 11 and 12 by the earlier two-solver census, and at least 13 by the empty neighbourhood census. This proves the lower bound \(h(18)\ge5\) at the stated computational confidence level. The explicitly checked graph \(W_{18}\) supplies \(h(18)\le5\).

4. Reproduction

The standalone checker is erdos813_wavew015_verify.py. It uses only the Python standard library for every explicit-graph and 2-density check. The lower-bound SAT replication additionally needs the installed python-sat package.

Commands:

# Dependency-free construction checks:
python -u runs/erdos813_wavew015_verify.py --witness-only

# Dependency-free audit of the new maximum-degree lower bound:
python -I runs/erdos813_delta7_check.py

# Constructions plus the CaDiCaL lower-bound replication:
python -u runs/erdos813_wavew015_verify.py

# Repeat all five UNSAT instances with both CaDiCaL and Kissat:
python -u runs/erdos813_wavew015_verify.py --cross-check

SHA-256 of the checker:

8ee0af91618b69113d49d54f3a7f24d6b043986b08e6e7252df622c60b940c1d

The new degree-reduction bundle is versioned at verification/813/n18-degree10/ in the site repository. Its central commands are:

python3 -u census_verify.py \
  census_n10.g6 census_n11.g6 census_n12.g6 census_n13.g6

python3 -u neighbourhood_census_sat.py \
  11 census_n11.g6 SHARD SHARDS --solver cadical195

python3 -u neighbourhood_census_sat.py \
  11 census_n11.g6 SHARD SHARDS --solver kissat404

The census audit needs NetworkX and nauty-shortg; the SAT reproduction needs PySAT with the named backends. The bundle includes the census files, both consolidated case tables, all raw shard logs, the near graph, a definition-level hostile audit, and a SHA-256 manifest binding them.

The final exact computation is versioned separately at verification/813/n18-exact/. Its README gives the dependency-free audit commands. The public bundle includes all canonical split files, independent CNF and census checkers, exact case-coverage transcripts, all raw solver logs in one compressed archive, one replayable cross-solver DRAT control, a hostile end-to-end audit, and a SHA-256 manifest. The complete laboratory archive is larger and contains three additional replayed spot controls; no conclusion depends on unmanifested scratch files.

The core CNF clauses are generated from the definition, rather than loaded from a trusted data file:

for triple in combinations(vertices, 3):
    t = triangle(triple)
    es = [edge(u, v) for u, v in combinations(triple, 2)]
    clauses.extend([[-t, e] for e in es])
    clauses.append([-es[0], -es[1], -es[2], t])

for seven in combinations(vertices, 7):
    clauses.append([triangle(T) for T in combinations(seven, 3)])

for five in combinations(vertices, 5):
    clauses.append([-edge(u, v) for u, v in combinations(five, 2)])

5. Precise walls

5.1 The finite boundary is closed; certificate production remains

[D] The maximum-degree split closes the first unknown finite case: \(h(18)=5\). The raw branch logs, exact gap-free coverage audits, canonical censuses, independently reconstructed CNFs, and four replayed spot proofs are all retained.

The remaining verification upgrade would be a compact proof certificate for the entire exclusion. The full d=7 through d=12 sweep did not retain one DRAT/LRAT derivation per branch. Proof-producing monolithic versions of the strengthened d=10, d=11, and d=12 formulas were tried for 1,800 seconds each and timed out; their nonterminal partial traces make no claim. A future run could retain replayable proofs for every canonical branch or compose smaller assumption cores into a global certificate. This would improve the certificate level of the exact value, not change the exhaustive result reported here.

5.2 The asymptotic wall

[A]+[B] The Bucić–Sudakov bound already answers the lower half of the live page's “in particular”: for every fixed \(c_1<1/12\),

Indeed, choose \(\varepsilon<1/12-c_1\) in \(h(n)\ge n^{5/12-o(1)}\).

[B] Their lower-bound machinery naturally stalls at exponent \(3/7\). Their paper identifies the needed improvement with a sharper Ramsey problem for their seven-vertex graph \(H_7\) versus an independent set, even with the extra knowledge that the ambient graph is \(K_4\)-free.

[B] On the construction/upper-bound side, their Proposition 1.4 uses the minimum 2-density

Their Theorem 3.5 together with its tightness example gives \(M(7,3)=2\). Thus this numerical 2-density/LLL route yields exponent \(1/M=1/2\) and cannot produce a fixed power saving merely by sharpening the evaluation of \(M(7,3)\).

[D] The checker independently verifies the tight example: the clique blow-up of \(C_5\) with consecutive part sizes \(1,2,1,1,2\) has seven vertices, 11 edges, independence number two, and 2-density exactly two.

[C] A proof of \(h(n)\ll n^{1/2-c_2}\) therefore needs a construction that exploits the whole family of seven-vertex forbidden graphs jointly (or some comparably new correlated/random-process mechanism), rather than the least-2-dense single obstruction. No such construction was found in this run or in the literature search above.

PROVED: Exhaustive maximum-degree CNFs and complete canonical censuses give h(18)=5 at computer-assisted solver-assertion level; the asymptotic problem remains open.