{"id":"palomar/PALOMAR-2026-08-31-000003","url":"https://github.com/sneed-and-feed/lean-theorems-1/tree/a3047d6bc04685572164ac141822aea8d3ad60e4","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-08-31-000003-v1.json","repo":"https://github.com/sneed-and-feed/lean-theorems-1","tags":["math.CO","msc:05D05","msc:11B75","msc:15A03","combinatorics","extremal-set-theory","lean-formalization"],"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 Frankl–Wilson theorem (1981) for modulo-p intersecting set families. Uses the polynomial linear algebra method over ZMod p to prove both the general non-uniform bound |F| <= sum_{i=0}^s choose(n, i) and the uniform cardinality bound |F| <= choose(n, s). To the maintainers' knowledge, the theorem was not found in an exact declaration name, 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-31","reactions":{},"formalized":true,"formalizes":[{"title":"Intersection theorems with geometric consequences","identifier":"","relationship":"formalizes"}]}