この記事の日本語版はまだありません。英語版を表示しています。

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

問題
Erdős problem #610 (graph theory); current status: proved (Lean)
貢献
Przemek Chojecki with Aristotle and GPT-5.4 Pro · AI working with humans
検証
Lean formalizationListed in Tao's wiki
経緯
First AI contribution 2026-04-21 · wiki data as of 2026-06-30
出典
Problem page (erdosproblems.com)Tao's AI-contributions wiki
部分的
結果
Per 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.

∎