Erdős Problem #19
Still open, but reduced to a finite computation: checking enough cases would settle it either way.
What the community database records, not our verdict. erdosproblems.com no longer shows statuses (why).
A configuration of `n` pairwise edge-disjoint copies of \(K_n\) covering the vertex type `V`.
The vertex sets of the `n` cliques. -/ A : Fin n → Finset V /-- Each clique has exactly `n` vertices. -/ card_eq : ∀ i, (A i).card = n /-- Two different cliques share at most one vertex, i.e. they are edge-disjoint. -/ inter_le : ∀ i j, i ≠ j → (A i ∩ A j).card ≤ 1 /-- Every vertex lies in one of the cliques. -/ cover : ∀ v, ∃ i, v ∈ A i namespace EFLConfig variable {V : Type*} {n : ℕ} (C : EFLConfig V n) /-- The union graph: distinct vertices are adjacent iff they lie in a common clique.
A vertex is *shared* if it lies in two different cliques.
Attempts
submit one →Read our working report →
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 colo
PARTIAL