Wiki
Wiki

Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.

Updated

Problem 1022

../

claims/: The 2 claim pages of Problem 1022, one per claimant's result; the problem's standing derives from them.


Statement. Is there a constant ctc_t, where ct→∞c_t\to \infty as t→∞t\to \infty, such that if F\mathcal{F} is a finite family of finite sets, all of size at least tt, and for every set XX there are <ct∣X∣<c_t\lvert X\rvert many A∈FA\in \mathcal{F} with A⊆XA\subseteq X, then F\mathcal{F} has chromatic number 22 (in other words, has property B)?

Statement (corrected). Is there a constant ctc_t, where ct→∞c_t\to \infty as t→∞t\to \infty, such that if F\mathcal{F} is a finite family of finite sets, all of size at least tt, and for every nonempty set XX there are <ct∣X∣<c_t\lvert X\rvert many A∈FA\in \mathcal{F} with A⊆XA\subseteq X, then F\mathcal{F} has chromatic number 22 (in other words, has property B)?

Notes. The site's wording quantifies over every set XX, the empty set included; at X=∅X=\varnothing its hypothesis reads 0<00<0, which never holds, so no family meets it and the question as printed is answered yes for every choice of ctc_t, for want of an instance. The defect is Erdős's: [Er71] Problem 17 (p. 105) takes the count "for every S1⊂SS_1\subset S", and the site's curator, Thomas Bloom, quoted that sentence in the problem's thread on 4 December 2025 and called the site's statement an accurate rephrasing of it. Bloom reads the question with XX nonempty. The site's commentary (page last edited 25 January 2026) calls the statement false and names Wood's construction [Wo13b] and KoishiChan's as counterexamples, which refute it only once XX is nonempty; the Lean statement that Boris Alexeev posted in the thread on 22 January 2026, whose hypothesis is X.Nonempty, is the one Terence Tao recorded as the formalization of KoishiChan's solution and the one the label's (LEAN) mark refers to; and on 23 January 2026 Bloom wrote of marking the problem solved by KoishiChan "since this answers the question as I understand it". The corrected Statement inserts "nonempty" before "set XX" and changes nothing else; the formal-conjectures statement requires XX nonempty as well. Under the printed wording the answer is yes, vacuously; under Bloom's reading it is no: Wood's theorem gives ct<2c_t<2 and KoishiChan's construction ct≤2c_t\le2 for every tt, and Lovász's theorem with [KN99] gives the exact value 11 (Known Results). No result about the printed wording exists beyond the vacuity check recorded here. The site's label PROVED (LEAN) has the polarity of a positive answer; it contradicts the site's own commentary and the Lean proof of the negation, and the page follows the commentary (Status).

Status. PROVED (LEAN) on erdosproblems.com (page last edited 25 January 2026); the site's own commentary says the statement is false, names Wood's construction [Wo13b] as the counterexample with ct<2c_t<2 for every tt, and credits KoishiChan with an independent counterexample in the comments; the label's Lean mark refers to the Lean proof listed under Formalization, which proves the negation of the corrected Statement. The page therefore departs from the site's label: the corrected Statement is disproved.

Source. erdosproblems.com/1022, accessed 2026-09-05. Cite as: T. F. Bloom, Erdős Problem #1022, https://www.erdosproblems.com/1022.

References.

Formalization.

  • The formal-conjectures statement, pinned to its revision of 4 September 2026, defines the positive existential proposition and records that the answer is false. Its theorem body is a sorry whose proof metadata points to the separate solution.
  • The Lean solution in Boris Alexeev's repository lean-proofs, linked at its pinned commit from the claim page KoishiChan 2025, formalizes KoishiChan's direct construction and proves the negation. Its header credits Aristotle and Boris Alexeev as formal authors. This corpus has not built it, so the formalization is a link and not formalized evidence.

Current assessment

The site labels the problem PROVED (LEAN). That label has the wrong polarity: the same page says the assertion is false, Wood's theorem gives counterexamples, and the linked Lean development proves the negation of the existential statement with XX nonempty, the corrected Statement.

Two accepted claim pages settle the problem in the negative, each by a different hypergraph: KoishiChan 2025, the direct two-level construction posted in the site's thread, reviewed there by Terence Tao, with the bound corrected to ct≤2c_t\le2 by ChatGPT Pro, which Tao ran on the argument, and credited by the site's curator; and Wood 2013, the earlier 22-degenerate construction that the curator's commentary names as the counterexample, which gives ct<2c_t<2. Neither is refereed, and the corpus has not built the third-party Lean proof of KoishiChan's construction. The sharper obstruction ct≤1c_t\le1 from [KN99], recorded under Known Results, is the corpus's reading of a paper Wood cites as a strengthening, not a claim anyone made about the problem, so it has no claim page.

The page links the complete Lovász and [KN99] proofs, Wood's full inductive construction, and KoishiChan's rewritten direct counterexample. It records the public acceptance of KoishiChan's argument; the local checks of Lovász's proof and of the other routes are author-recorded, and no independent review report of them is retained in this repository. The site's page and its forum thread list no other claim.

Progress

The original formulation on p. 105 of [Er71] requires ∣A∣>t|A|>t, while the site uses size at least tt. This indexing difference does not affect the negative answer: use Wood's (t+1)(t+1)-uniform example for the original wording and Wood's tt-uniform example for the site's wording.

On p. 105 of [Er71], Erdős reports that Lovász proved the t=2t=2, c=1c=1 case, and says that the Fano plane shows the constant is best possible. No reference is attached to that sentence in the paper. The site's commentary says [Lo68] does not contain this result. The full proof, recorded on its library result page, appears instead as Theorem 5 of [Lo68b], a different 1968 paper. Theorem 3 of [Lo73] restates the result in its union-of-edges form and explicitly cites [Lo68b] as reference [2]. This supplies published provenance for Lovász's theorem without identifying the site's [Lo68] as its source.

In December 2025, KoishiChan posted a direct two-level construction with a two-to-one assignment of edges to vertices. Terence Tao judged the argument essentially correct; ChatGPT Pro, which Tao ran on it, corrected the claimed ct<2c_t<2 to ct≤2c_t\leq2 for that construction, and Thomas Bloom later marked the problem solved. The [[../library/set_systems/koishichan_2025_counterexample_erdos_1022/counterexample|rewritten proof]] records the construction and its acceptance provenance.

In January 2026, KoishiChan also pointed out that Wood's earlier Theorem 3 gives a stronger counterexample. Bloom corrected the comment's claimed equivalence: degeneracy implies the problem's counting condition, while the converse need not hold. This one-way implication is all that the disproof needs.

Wood's paper in turn points to [KN99] as a strengthening. Property 7 there constructs 3-chromatic uniform hypergraphs whose maximum subhypergraph density is arbitrarily close to 11. Its complete proof gives the stronger upper obstruction ct≤1c_t\leq1 below.

[KN99] also reports that Burstein, Lovász, Seymour, and Woodall independently proved that every 3-chromatic hypergraph has density at least 11. The Lovász proof is Theorem 5 of [Lo68b], reached through [Lo73]'s explicit pointer; its local check is author-recorded, and no independent review report is retained in this repository. In the terminology of [Lo68b], the strict c=1c=1 condition makes the family a forest, and Theorem 5 two-colors it.

Known Results

The largest valid constant is exactly 11 for every t≥2t\geq2. To prove the positive direction, suppose first that F\mathcal F is nonempty and satisfies the problem's hypothesis with c=1c=1. For every nonempty subfamily K⊆F\mathcal K\subseteq\mathcal F, take X=⋃KX=\bigcup\mathcal K. Then

∣K∣≤∣{A∈F:A⊆X}∣<∣X∣,|\mathcal K| \leq |\{A\in\mathcal F:A\subseteq X\}| <|X|,

so ∣X∣≥∣K∣+1|X|\geq|\mathcal K|+1. A subsystem with no edges and a nonempty vertex set satisfies the same inequality automatically. Thus the family is a forest in the sense of [Lo68b]. Lovász's Theorem 5 gives a two-coloring, and the empty family is immediate. See the complete inductive proof. The equivalent union-of-kk-edges formulation and its exact self-citation appear as Theorem 3 of [Lo73].

For all integers g≥3g\geq3, r≥2r\geq2, and m≥1m\geq1, [KN99] constructs a 3-chromatic rr-uniform hypergraph GG of girth at least gg with

den⁡(G)=max⁡∅≠H⊆G∣E(H)∣∣V(H)∣<1+1m.\operatorname{den}(G) =\max_{\varnothing\ne H\subseteq G}\frac{|E(H)|}{|V(H)|} <1+\frac1m.

Fix t≥2t\geq2 and c>1c>1, take r=tr=t, and choose mm with 1+1/m<c1+1/m<c. Every nonempty induced subhypergraph G[X]G[X] then has fewer than c∣X∣c|X| edges, but GG has no property B. Consequently every constant for which the problem's implication could hold must satisfy c≤1c\leq1. Together with Lovász's positive result, this proves the exact value above. See the complete Property 7 proof and its replacement-construction dependencies.

For every t≥2t\geq2, Wood constructs a triangle-free, 22-degenerate, tt-uniform hypergraph of chromatic number 33. Degeneracy gives strictly fewer than 2∣X∣2|X| edges inside every nonempty XX. Therefore every constant for which the problem's implication holds must be <2<2, ruling out ct→∞c_t\to\infty. See [[../library/set_systems/wood_2013_hypergraph_colouring_degeneracy/theorem_3|Theorem 3 and its application]] and the full [[../library/set_systems/wood_2013_hypergraph_colouring_degeneracy/lemma_4|inductive construction]].

KoishiChan's materially different direct construction gives, for every t≥2t\geq2, a non-two-colorable (t+1)(t+1)-uniform hypergraph with at most 2∣X∣2|X| edges inside each vertex set XX. It excludes every c>2c>2 and by itself already disproves the proposed sequence. See the [[../library/set_systems/koishichan_2025_counterexample_erdos_1022/counterexample|direct counterexample]].

Linked library material

These entries are derived from explicit links on library pages. They are navigation only and do not by themselves record mathematical progress.