Erdős Problem #610

Partial progress by Przemek Chojecki with Aristotle and GPT-5.4 Pro (21 Apr 2026): full solution (Lean) (implicit in literature).

Problem
Erdős problem #610 (graph theory); current status: proved (Lean)
Credit
Przemek Chojecki with Aristotle and GPT-5.4 Pro · AI working with humans
Checked
Lean formalizationListed in Tao's wiki
Timeline
First AI contribution 2026-04-21 · wiki data as of 2026-06-30
Sources
Problem page (erdosproblems.com)Tao's AI-contributions wiki
PARTIALPer Tao's AI-contributions wiki

The problem

For a graph GG let τ(G)\tau(G) denote the minimal number of vertices that include at least one from each maximal clique of GG (aside from isolated vertices). This is sometimes called the clique transversal number.

Estimate τ(G)\tau(G). In particular, is it true that if GG has nn vertices then

τ(G)≤n−ω(n)n\tau(G) \leq n-\omega(n)\sqrt{n}

for some ω(n)→∞\omega(n)\to \infty, or even

τ(G)≤n−cnlog⁡n\tau(G) \leq n-c\sqrt{n\log n}

for some absolute constant c>0c>0?

Statement quoted from erdosproblems.com/610, maintained by Thomas Bloom. Original source: [EGT92][Er94][Er99]. Current status there: proved (Lean).

AI contributions

As recorded in Terence Tao's wiki AI contributions to Erdős problems (data as of 30 Jun 2026). 🟢 full, 🟡 partial, ⚪ unverified, 🔴 incorrect.

Date Kind AI systems Humans Outcome
21 Apr, 2026 AI working with humans Aristotle, GPT-5.4 Pro Przemek Chojecki 🟢 Full solution (Lean) (implicit in literature)

Caveats

The wiki's classifications are provisional and are not a benchmark. Many Erdős problems have never had a thorough literature review, so a result that looks new may later turn out to be known; some problems were also stated ambiguously or incorrectly. See the problem page for the full discussion.

∎