{"id":"palomar/PALOMAR-2026-08-26-000009","url":"https://github.com/sneed-and-feed/lean-theorems-1/tree/158e3dbad77b780e4e21c89072bc3b863104edd1","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-08-26-000009-v1.json","repo":"https://github.com/sneed-and-feed/lean-theorems-1","tags":["math.CO","msc:05D05","msc:05A05","extremal-combinatorics","intersecting-families","lean","formal-verification"],"score":0,"title":"sneed-and-feed/lean-theorems-1","trust":"high","domain":"math.CO","source":"palomar","authors":["Sneed & Feed Formalization Team"],"reviews":0,"subject":"math.CO","summary":"A complete machine-checked Lean 4 formalization of the Erdős–Ko–Rado theorem (1961) on intersecting families of finite sets using Katona's circle method (1972), along with the construction of the classical Hilton–Milner (1967) extremal non-star intersecting family. To the maintainers' knowledge, the theorem was not found in an exact declaration, docstring, and type signature search of the pinned Mathlib revision (Mathlib v4.34.0-rc1).","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-08-26","reactions":{},"formalized":true,"formalizes":[{"title":"Intersection theorems for systems of finite sets","identifier":"","relationship":"formalizes"},{"title":"A simple proof of the Erdös-Chao Ko-Rado theorem","identifier":"","relationship":"adapts"},{"title":"Some intersection theorems for systems of finite sets","identifier":"","relationship":"adapts"}]}