Erdős problem 813 — wave w015

Date: 2026-07-28 UTC

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 fetched <https://www.erdosproblems.com/813> through the Bright Data browser path on 2026-07-28 UTC. The live page said OPEN. It 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:

| Range | Lower bound | Upper bound | Classification | |---|---|---|---| | \(1\le n\le6\) | every nonempty graph has \(K_1\) | the edgeless graph | [A] | | \(7\le n\le12\) | the condition itself supplies a triangle | induced subgraphs of \(I_{12}\) below | lower [A], upper [D] | | \(13\le n\le17\) | \(F_v(3,3;4)=14\), or the independent SAT replication below | induced subgraphs of \(W_{17}\) below | lower [B] (also [D]), upper [D] | | \(n=18\) | monotonicity from \(h(13)=4\) | \(W_{18}\) below | lower [A]+[B], upper [D] |

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):

| \(\Delta=d\) | Clauses | CaDiCaL 1.9.5 | Kissat 4.0.4 | |---:|---:|---:|---:| | 2 | 6,447 | UNSAT, 0.009 s | UNSAT, 0.044 s | | 3 | 10,022 | UNSAT, 0.035 s | UNSAT, 0.100 s | | 4 | 13,883 | UNSAT, 0.495 s | UNSAT, 0.930 s | | 5 | 15,599 | UNSAT, 4.804 s | UNSAT, 7.906 s | | 6 | 13,883 | UNSAT, 35.412 s | UNSAT, 40.291 s |

[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 next case

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\).

[A]+[B] Monotonicity and \(h(13)=4\) give \(h(18)\ge4\), so

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

# 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 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 four in combinations(vertices, 4):
    clauses.append([-edge(u, v) for u, v in combinations(four, 2)])

5. Precise walls

5.1 The unresolved finite boundary

[D] To decide whether \(h(18)=4\) or \(5\), it is enough to decide whether a \(K_5\)-free valid graph on 18 vertices exists. The unsplit direct CNF has

variables and

clauses. One unguided CaDiCaL run was externally stopped after 180 seconds, and a run phased from \(W_{18}\) was stopped after 60 seconds; neither returned SAT or UNSAT. This is no evidence for either answer.

[A]+[B] A hypothetical \(K_5\)-free valid graph has \(\Delta\le12\): every neighbourhood is \(K_4\)-free, and 13 neighbours would induce a forbidden 13-vertex \(K_4\)-free valid graph. Thus an exact next computation can split on a maximum-degree vertex with \(d=2,\ldots,12\), exactly as in the order-13 check.

[C] A sensible certified pilot is 11 degree cases times two solvers times one core-hour, about 22 core-hours. Allowing proof logging and independent proof checking makes 40–100 core-hours a more realistic initial budget, not a guarantee. At a typical on-demand CPU price of roughly \(\$0.05\)–\(\$0.10\) per core-hour, that is about \(\$2\)–\(\$10\). This computation was not run 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.

PARTIAL: Verified exactly h(n)=1 for 1<=n<=6, h(n)=3 for 7<=n<=12, and h(n)=4 for 13<=n<=17; also verified 4<=h(18)<=5, with explicit constructions and a reproducible two-solver n=13 lower-bound check.