Open Research Index

The Hilton–Milner theorem

Juan Pablo Traverso Gianini

Palomar Registrypalomar/PALOMAR-2026-10-28-000001Oct 28, 2026math.COscore 0

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.

SourceRepositoryJSON

Comments and reviews

No comments yet.

Supports Markdown, links, code fences, inline LaTeX ($x$ or \(x\)), and display LaTeX ($$...$$ or \[...\]).

Drafts stay in this tab.

API

curl /api/v1/records/palomar/PALOMAR-2026-10-28-000001
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-28-000001/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-28-000001/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"body": "…", "review": true}'