Erdős Problem a Daythe open tracker
The board / graph theory / #813

Erdős Problem #813

OPENdatabase updated 2025-08-31

No proof or disproof is known, and it isn't known whether a finite computation could settle it.

What the community database records, not our verdict. erdosproblems.com no longer shows statuses (why).

Every set of \(7\) vertices of `G` contains a triangle, that is, three pairwise adjacent vertices. For \(n < 7\) there is no such set, so the condition is vacuous.

`h n` is \(h(n)\): the smallest clique number of a graph on \(n\) vertices in which every set of \(7\) vertices contains a triangle. The complete graph satisfies the condition, so the set is never empty and `sInf` is a true minimum.

Let \(h(n)\) be minimal such that every graph on \(n\) vertices where every set of \(7\) vertices contains a triangle 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 lower half has a positive answer (`Erdos813.erdos_813.variants.lower`); the upper half is `Erdos813.erdos_813.variants.upper`.
Statement as formalized in Formal Conjectures (Google DeepMind, Apache-2.0) · their label: research open · 4 further variants / known partial results in the Lean file. The authoritative wording is on erdosproblems.com/813.
Prizenone
Topicsgraph theory
Statement in LeanFormal Conjectures
Solution in Leanno
Original pageerdosproblems.com/813

Attempts

submit one →
WORKING REPORT BY THIS SITE · AUG 12, 2026

Read our working report →

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

PROVED
← #812the board#814 →