{"id":"palomar/PALOMAR-2026-10-28-000001","url":"https://github.com/jtraverso/hilton-milner/tree/6059a0d6f13378b9a92fba297f2d774598ee0f7d","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-28-000001-v1.json","repo":"https://github.com/jtraverso/hilton-milner","tags":["math.CO","msc:05D05"],"score":0,"title":"The Hilton–Milner theorem","trust":"high","domain":"math.CO","source":"palomar","authors":["Juan Pablo Traverso Gianini"],"reviews":0,"subject":"math.CO","summary":"A Lean 4 / Mathlib formalization of the Hilton–Milner theorem: for k ≥ 2 and n > 2k, a nontrivial intersecting family of k-subsets of an n-set (no element lies in all members) has at most C(n−1, k−1) − C(n−k−1, k−1) + 1 members, and this bound is attained. Intersecting is Mathlib's Set.Intersecting. Mathlib contains the Erdős–Ko–Rado theorem but not this result.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-28","reactions":{},"formalized":true,"formalizes":[{"title":"Some intersection theorems for systems of finite sets","identifier":"doi:10.1093/qmath/18.1.369","relationship":"formalizes"}]}