Combinatorics

Date added 6 Nov 2026

Erdős problem 19

G

is an edge-disjoint union of

n

copies of

K_n

, then is

\chi(G) = n

$1,036 bounty

Solve it

Nobody has attempted this. A complete proof or refutation takes the whole bounty.

Submit a proof

Where this lives

conjectures-tasks

The pinned statement, the Lean challenge file and the exact bundle you build against.

versions/fc-v2-erdos19-erdos-19-f60a2df3f33a72302b701b22-formalized →

Formal statement

Proof target

import Mathlib
import FormalConjectures.ErdosProblems.«19»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos19.erdos_19" := by
  sorry

end Bounty

Open this target’s Challenge.lean Task bundle on GitHub

Original conjecture (Lean type)

∀ (V : Type) (n : ℕ) (C : Erdos19.EFLConfig V n), C.graph.chromaticNumber = ↑n

Original conjecture source: FormalConjectures/ErdosProblems/19.lean

The audit patch changes this file, so the upstream version can differ from the statement above.

Source type SHA-256: sha256:4a449a6315ce1e5d6d611dbeab77103d73cfdf32486221e1062a9a396e81be78
Task id: fc-v2-erdos19-erdos-19-f60a2df3f33a72302b701b22-formalized
Task commitment: sha256:9ce9d79b123431ba3e3f1e3c97918e36698c6f3c9944bc4ad488e2a8f998b0eb

References

erdosproblems.com/19

[Hi81] Hindman, N., *On a conjecture of Erdős, Faber, and Lovász about $n$ -colorings*. Canad. J. Math. (1981).
[Ka92] Kahn, J., *Coloring nearly-disjoint hypergraphs with $n + o(n)$ colors*. J. Combin. Theory Ser. A (1992).
[KKKMO21] Kang, D. Y., Kelly, T., Kühn, D., Methuku, A. and Osthus, D., A proof of the Erdős–Faber–Lovász conjecture. Ann. of Math. (2023). arXiv:2101.04698

Something wrong with this formalization?

A statement that does not faithfully capture the original conjecture is the one real risk here, so we would rather hear about it early - before someone spends weeks on it.

Our channel is in the Bittensor Discord server. Join the server first, then open the channel to send your report.

Bittensor Discord