{"id":"palomar/PALOMAR-2026-10-20-000006","url":"https://github.com/jtraverso/kneser-lovasz/tree/6699c87d87f4ddb159fc42271263fc429e63004a","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-20-000006-v1.json","repo":"https://github.com/jtraverso/kneser-lovasz","tags":["math.CO","msc:05C15","msc:05E45","msc:55M20","combinatorics","kneser-graphs","topological-combinatorics","lean-formalization"],"score":0,"title":"Kneser's conjecture and the octahedral Tucker lemma","trust":"high","domain":"math.CO","source":"palomar","authors":["Juan Pablo Traverso Gianini"],"reviews":0,"subject":"math.CO","summary":"A Lean 4 / Mathlib formalization of Lovász's theorem (Kneser's conjecture): for 0 < k and 2k ≤ n the Kneser graph KG(n, k) of k-subsets of an n-set, adjacent when disjoint, has chromatic number exactly n − 2k + 2; proved combinatorially from the octahedral Tucker lemma (an antipodal labelling of the nonzero sign vectors of length n by nonzero integers in [−m, m] with m < n has a complementary pair x ≼ y with λ(x) = −λ(y)), which is itself proved by Ky Fan's parity argument. Mathlib has neither Kneser graphs nor Tucker's lemma.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-20","reactions":{},"formalized":true,"formalizes":[{"title":"Kneser's conjecture, chromatic number, and homotopy","identifier":"doi:10.1016/0097-3165(78)90022-5","relationship":"formalizes"},{"title":"A combinatorial proof of Kneser's conjecture","identifier":"doi:10.1007/s00493-004-0011-1","relationship":"formalizes"},{"title":"A constructive proof of Tucker's combinatorial lemma","identifier":"doi:10.1016/0097-3165(81)90027-3","relationship":"formalizes"}]}