Erdős problem #19 — live-status audit, exact \(n=13\) reduction, and certificates

Access date: 2026-07-26 (UTC)

Claim labels used throughout:

• [a] elementary-rigorous — proved directly here or checkable by the standalone certificate checker.
• [b] rigorous-modulo-named-theorem — the deduction is rigorous assuming the cited published theorem.
• [c] plausible/structural-unverified — an inference, search miss, or cost forecast, not a theorem.
• [d] computational-only — a finite computation or an observation of live external state.

Outcome

[b+d] I did not solve the uniform Erdős–Faber–Lovász (EFL) conjecture. The sharp currently documented finite frontier at \(n=13\) is the 22 reduced buckets

where \(m\) is the number of lines/hyperedges in the dual 13-point linear space. This follows from Proposition 9, Corollary 10, and Theorem 14 of Kirchweger–Peitl–Szeider (SAT 2023), whose large computations I did not rerun.

[a] I produced a fully explicit, independently checkable reduced linear space in every one of those 22 buckets. Each has a selected reduction core containing every line of size at least three and having minimum line-intersection degree at least 13. Explicit optimal colorings give the exact chromatic indices of these 22 witnesses. Thus none of the 22 buckets is vacuous, even after the critical-core reduction.

[a] This does not prove that every member of any bucket is 13-colorable. It supplies a reproducible benchmark corpus and isolates the missing universal assertion exactly.

0. Mandatory live-page gate

[d] I fetched the live problem page, its LaTeX source, and the linked eight-comment discussion using a Bright Data cloud browser, not datacenter curl. The page was last edited 07 March 2026.

Verbatim current statement

[d] The exact LaTeX-source statement, copied verbatim, is:

If $G$ is an edge-disjoint union of $n$ copies of $K_n$ then is $\chi(G)=n$?

Gate fields

[d]

| Live field | Value |

|---|---|

| Status banner | DECIDABLE - $500 |

| Claimed proofs | 0 claimed proofs for this problem |

| Interested in collaborating | None |

| Currently working on this problem | None |

| Comments | 8 comments on this problem |

[d] The mandatory stop condition therefore did not fire: the live label was DECIDABLE, not solved/falsified; there was no claimed proof and no current worker.

Results and variants listed on the live page

[d] The page says the problem was conjectured by Erdős, Faber, and Lovász. It lists Kahn’s bound

\(\chi(G)\leq(1+o(1))n\), says Hindman proved the conjecture for \(n<10\), names special cases by Romero–Sánchez-Arroyo, Araujo-Pardo–Vázquez-Ávila, and Alesandroni, and says Kang–Kelly–Kühn–Methuku–Osthus proved the answer for all sufficiently large \(n\).

[d] The page also records:

• Erdős’s variant in which clique intersections need only be triangle-free or contain at most one edge;
• the Erdős–Füredi generalization for \(n\) copies of \(K_n\) with pairwise intersections of at most \(k\) vertices, conjecturing \(\chi(G)\leq kn\);
• the sufficiently-large-\(n\), \(k\)-independent result of Kang–Kelly–Kühn–Methuku–Osthus for that generalization;
• the displayed Horák–Tuza \(n^{3/2}\) bound and its \(k\geq\sqrt n\) consequence; and
• Erdős’s parameter \(m_k\), the least number of edge-disjoint \(K_n\)'s whose union can have chromatic number at least \(n+k\), with the original question phrased as \(m_1>n\).

All eight live comments

[d] These are transcriptions/summaries of user comments; the site itself warns that comments are not verified.

1. onetwothreefour, 20 Jul 2026: suggested correcting the page’s “Boulder, Colarado” wording; disclosed minor AI typo assistance.

2. Alfaiz, 02 Dec 2025: supplied the Hindman citation and noted the £50 / $100 prize statements in two 1976 Erdős sources.

3. Thomas Bloom, 06 Dec 2025: agreed the formulation was equivalent and added the references.

4. dykang, 25 Nov 2025: pointed to Theorem 1.2 of arXiv:2110.06181 for the bounded-intersection generalization and combined it with Horák–Tuza to leave finitely many \((k,n)\).

5. TerenceTao, 01 Sep 2025: observed that the original problem was technically not completely resolved, only reduced to finitely many cases.

6. zach hunter, 03 Sep 2025: viewed the asymptotic theorem as more solved than unsolved while acknowledging the finite residue.

7. TerenceTao, 04 Sep 2025: described the intended binary site status and the more nuanced community-database status decidable.

8. Thomas Bloom, 07 Sep 2025: explained his own preference for treating “all sufficiently large integers” as close to solved while retaining the nuanced status.

[d] The arXiv identifier in comment 4 exists and is the Kang–Kelly–Kühn–Methuku–Osthus paper “Solution to a problem of Erdős on the chromatic index of hypergraphs with bounded codegree”, submitted in 2021 and revised in 2024.

1. Primary-source audit

Results that matter for the finite frontier

[b] Kahn’s actual paper exists as JCTA 59 (1992), 31–39, DOI 10.1016/0097-3165(92)90096-D90096-D), and states the \(n+o(n)\) chromatic-index bound for nearly-disjoint hypergraphs.

[b] Hindman’s paper is N. Hindman, “On a conjecture of Erdős, Faber, and Lovász about \(n\)-colorings,” Canadian J. Math. 33 (1981), 563–570, DOI 10.4153/CJM-1981-046-9. Its final result is stronger than merely checking small \(n\): if the union of the hyperedges of size at least three has at most 10 vertices, the family is colorable. Taking the whole vertex set gives the EFL conjecture for \(n\leq10\). Thus the live page’s displayed \(n<10\) is weaker than the primary paper.

[d] Romero and Alonso-Pecina’s paper, “The Erdős–Faber–Lovász conjecture is true for \(n\leq12\),” Discrete Math. Algorithms Appl. 6 (2014), article 1450039, DOI 10.1142/S1793830914500396, reports exhaustive generation plus heuristic coloring of the 232,929 nonisomorphic 11-point and 28,872,973 nonisomorphic 12-point linear spaces. I verified that the paper and those claims exist; I did not regenerate those universes.

[b] Kang, Kelly, Kühn, Methuku, and Osthus proved that every sufficiently large \(n\)-vertex linear hypergraph has chromatic index at most \(n\): Annals of Mathematics 198 (2023), 537–618, DOI 10.4007/annals.2023.198.2.2.

[b] Their theorem does not publish a numerical cutoff. Section 3 defines \(a\ll b\) via an unspecified function and explicitly says that the functions will not be calculated. The final proof uses the hierarchy

Consequently the theorem proves that the residue is finite but does not hand us a finite numerical job list.

[d] Kirchweger, Peitl, and Szeider, “A SAT Solver’s Opinion on the Erdős–Faber–Lovász Conjecture”, SAT 2023, Article 13, give a proof-logging-capable SAT-modulo-symmetries workflow. Their Theorem 14 computationally verifies EFL' for:

I verified this statement in the official paper. I did not rerun its long SAT jobs or independently validate their DRAT output.

[c] A primary-source web search through 2026-07-26 found no later paper claiming a complete verification for \(n=13\) or an explicit \(n_0\). This is a search result, not proof that no such source exists.

2. Exact reduction

Duality

[a] Number the \(n\) cliques \(1,\dots,n\). For each vertex \(x\) of their union, form

Two distinct clique indices occur together in at most one \(S_x\), because two different shared vertices would give a common graph edge and violate edge-disjointness. Hence the sets \(S_x\) form a linear hypergraph on \(n\) points.

[a] Coloring the graph vertices is the same as edge-coloring the sets \(S_x\): two graph vertices are adjacent exactly when their corresponding sets share a clique index. Private graph vertices correspond to singleton hyperedges. Once all nonsingleton hyperedges have been properly colored with \(n\) colors, the singleton copies at each point receive the unused colors. Conversely, every loopless linear hypergraph on \(n\) points can be padded with private singleton copies because at a point its nonsingleton incident edges use disjoint other points and therefore number at most \(n-1\).

[a] Thus the live statement is equivalent to:

> Every loopless (all edges have size at least two) linear hypergraph on \(n\) vertices has chromatic index at most \(n\).

Linear-space and critical-core reductions

[a] Add a 2-edge for every uncovered pair of points. This preserves linearity and cannot turn a non-\(n\)-colorable hypergraph into an \(n\)-colorable one. A minimal search may therefore be restricted to linear spaces, where every point-pair lies in exactly one line.

[a] A 13-point linear space has at most

\(\binom{13}{2}=78\) lines, since every line contains at least one pair and distinct lines cover disjoint pairs.

[b] Proposition 9 and Corollary 10 of the SAT 2023 paper sharpen the completion step. If an EFL counterexample with \(n\) points exists, then an EFL' counterexample exists with at least as many lines and with a selected subgraph of the line-intersection graph that:

• contains every line of size at least three, and
• has minimum degree at least \(n-1\).

The paper calls the resulting space \((n-1)\)-reduced.

[a] For the counterexample search one may strengthen the core degree from \(n-1\) to \(n\). In the line-intersection graph of a non-\(n\)-colorable space, take a vertex-minimal non-\(n\)-colorable subgraph \(J\). For every \(v\in V(J)\), the graph \(J-v\) has an \(n\)-coloring; if \(d_J(v)\leq n-1\), one of the \(n\) colors is absent from its neighbors and extends to \(v\), a contradiction. Thus \(\delta(J)\geq n\). Delete every line of size at least three outside \(J\), and replace each deleted line by all of its constituent pairs. This preserves the pair partition, does not destroy \(J\), only increases the number of lines, and makes \(J\) contain every remaining line of size at least three. Hence a counterexample has a completed representative with the stronger degree-\(n\) core used by my certificates.

[b+d] For \(n=13\), Theorem 14 covers every \(m\in[13,78]\) except

Therefore ruling out non-13-colorability in these 22 buckets for spaces with a degree-13 core would prove the original EFL assertion for \(n=13\). This implication is exact; it does not say anything uniform yet about \(n\geq14\).

3. Explicit reduced witnesses in all 22 open \(n=13\) buckets

Seed

[a] On points \(0,\dots,12\), let \(\mathcal L_{33}\) contain the following 33 lines, in the displayed order within each size:

Here, for example, \(0\,2\,10\) denotes \(\{0,2,10\}\).

[a] The checker directly counts every one of the 78 point-pairs and finds it exactly once. Equivalently, the line-size profile satisfies

and the stronger pair-by-pair check rules out accidental repetitions or omissions.

Refinements

[a] Replacing a triple by its three pairs preserves the pair partition and increases the line count by two.

[a] Replacing the 4-line \(3\,9\,11\,12\) by

also preserves its six covered pairs and increases the line count by three.

[a] The following deterministic construction covers 21 buckets:

• for odd \(m=33+2a\), \(0\leq a\leq10\), split the first \(a\) triples in the displayed seed order;
• for even \(m=36+2a\), \(0\leq a\leq9\), first refine the 4-line as above and then split the first \(a\) original triples.

This gives every odd \(m=33,35,\dots,53\) and every even \(m=36,38,\dots,54\).

[a] For the missing bucket \(m=34\), take \(H_{13,10}\): one 10-line

\(B=\{0,\dots,9\}\), together with every pair not wholly contained in \(B\). There are

lines, and again every point-pair is covered exactly once.

Verified table

[a] In the block sizes column, \(s^t\) means \(t\) lines of size \(s\). core is the size of the supplied reduced core, every core has checked minimum intersection degree 13, max-rep is the largest number of lines through one point, and \(\chi'\) is the exact chromatic index of this particular witness.

| \(m\) | block sizes | core | \(\delta(\text{core})\) | max-rep | \(\chi'\) |

|---:|---:|---:|---:|---:|---:|

| 33 | \(2^{12}3^{20}4^1\) | 29 | 13 | 10 | 10 |

| 34 | \(2^{33}10^1\) | 31 | 13 | 12 | 13 |

| 35 | \(2^{15}3^{19}4^1\) | 31 | 13 | 11 | 11 |

| 36 | \(2^{15}3^{21}\) | 29 | 13 | 10 | 10 |

| 37 | \(2^{18}3^{18}4^1\) | 29 | 13 | 12 | 12 |

| 38 | \(2^{18}3^{20}\) | 31 | 13 | 11 | 11 |

| 39 | \(2^{21}3^{17}4^1\) | 32 | 13 | 12 | 12 |

| 40 | \(2^{21}3^{19}\) | 29 | 13 | 12 | 12 |

| 41 | \(2^{24}3^{16}4^1\) | 36 | 13 | 12 | 12 |

| 42 | \(2^{24}3^{18}\) | 37 | 13 | 12 | 12 |

| 43 | \(2^{27}3^{15}4^1\) | 38 | 13 | 12 | 12 |

| 44 | \(2^{27}3^{17}\) | 36 | 13 | 12 | 12 |

| 45 | \(2^{30}3^{14}4^1\) | 37 | 13 | 12 | 12 |

| 46 | \(2^{30}3^{16}\) | 38 | 13 | 12 | 12 |

| 47 | \(2^{33}3^{13}4^1\) | 37 | 13 | 12 | 12 |

| 48 | \(2^{33}3^{15}\) | 39 | 13 | 12 | 12 |

| 49 | \(2^{36}3^{12}4^1\) | 41 | 13 | 12 | 12 |

| 50 | \(2^{36}3^{14}\) | 38 | 13 | 12 | 12 |

| 51 | \(2^{39}3^{11}4^1\) | 42 | 13 | 12 | 12 |

| 52 | \(2^{39}3^{13}\) | 37 | 13 | 12 | 12 |

| 53 | \(2^{42}3^{10}4^1\) | 42 | 13 | 12 | 12 |

| 54 | \(2^{42}3^{12}\) | 39 | 13 | 12 | 12 |

Why the listed chromatic indices are exact

[a] For every row except \(m=34\), the standalone file contains and checks a coloring using exactly max-rep colors. All lines through a fixed point pairwise intersect, so they require max-rep distinct colors. The upper and lower bounds coincide.

[a] For \(m=34\), the checked certificate uses 13 colors. Twelve colors are impossible by a short parity/matching argument. Let \(\alpha\) be the color of the 10-line \(B\), and let \(O\) be the three outside points. Each point of \(O\) lies on 12 lines, so in a hypothetical 12-coloring it sees every color, including \(\alpha\). No \(B\)-to-\(O\) pair can have color \(\alpha\), because it meets \(B\). Therefore the \(\alpha\)-colored lines in \(O\) would have to form a matching of \(K_3\) covering all three vertices. A matching in \(K_3\) covers at most two vertices, a contradiction.

[a] These examples show an important limitation of the reduced-core condition: 21 of the 22 witnesses are already colorable with at most 12 colors, while the familiar \(H_{13,10}\) witness needs exactly 13. A minimum-degree-13 reduction core is available without loss of generality in the universal counterexample search, but by itself is far from forcing chromatic index 14.

[c] I do not claim the seed or the family as novel. The contribution of this run is the explicit all-bucket certificate corpus, its exact chromatic table, and the precise audit trail tying it to the live finite frontier.

4. Standalone re-verification

[a] The complete standard-library checker and all certificates are in

runs/erdos19_wave5f_verify.py. Run:

python -I runs/erdos19_wave5f_verify.py

[a] The checker uses only the Python standard library. It reconstructs every space rather than loading solver output, then independently checks:

1. exactly \(m\) distinct valid lines;

2. each of the 78 point-pairs occurs in exactly one line;

3. the core indices are valid, contain every line of size at least three, contain at least 14 lines, and have minimum intersection degree at least 13;

4. every explicit coloring is proper at every point;

5. the point-pencil lower bound matches the coloring, except at \(m=34\), where it checks the structural premises and finite \(K_3\)-matching obstruction above.

[d] Three negative mutation tests confirm that the checker rejects (i) a missing line, (ii) an improper color collision, and (iii) a core omitting a mandatory large line.

[d] Clean isolated execution on this VM produced:

elapsed=0.04 user=0.03 sys=0.00 maxrss_kb=12696
ALL CHECKS PASSED (22 buckets; 3 negative mutation tests)

[d] SHA-256 of the verified script:

d7da5abc672532663d0bfe5fc9e938af36c1b06e7cad4573286bee0172e6df09

[d] OR-Tools CP-SAT was used during exploration to find cores and colorings. It is not trusted at verification time: all retained outputs are explicit certificates checked by the standard-library script.

5. Exact wall and realistic next computation

[a+b+d] The next missing lemma for \(n=13\) is now exact:

> Every 13-point linear space with \(33\leq m\leq54\) that has a subgraph containing all lines of size at least three and minimum intersection degree at least 13 is 13-edge-colorable.

Proving this for all 22 buckets closes \(n=13\), modulo the published EFL/EFL' equivalence and the published computations outside the interval.

[a] Checking one witness per bucket cannot prove this universal statement. The quantifiers are adversarial: one must rule out the existence of a reduced linear space for which no 13-coloring exists. This is why ordinary “generate a candidate and color it” SAT is insufficient without enumeration, co-certificate learning, or a quantified encoding.

[d] The SAT 2023 implementation alternates a symmetry-aware hypergraph generator and a coloring solver. The paper allowed up to three CPU-days per \((n,m)\) case; its longest successful reported case took 63 hours 26 minutes. Those jobs are outside this run’s few-CPU-minute limit, so I did not launch an \(n=13,m=33\) universal SMS run.

[c] A same-cap sweep of 22 buckets is budgeted at

before proof-production reruns, checking, or overruns. At the current 2026 Hetzner Germany/Finland price of $0.1626/hour for a 4-dedicated-vCPU CCX23 instance, ideal full packing is about $64; six 72-hour instances are about $70, excluding VAT, IPv4, storage, and proof-log costs. This is an attempt budget, not a completion guarantee; the unresolved central buckets may exceed the old three-day cap.

[b] Even a complete \(n=13\) computation would not close the original uniform problem. A full finite resolution also needs an explicit usable \(n_0\) extracted from the Annals proof and certified treatment of every \(14\leq n

PARTIAL: reduced the documented \(n=13\) frontier exactly to \(m=33,\ldots,54\) and supplied independently verified reduced witnesses with exact chromatic index in all 22 nonvacuous buckets; the universal colorability of those buckets and the global effective cutoff remain open.