Open Research Index

Kirkman's theorem on Steiner triple systems

Juan Pablo Traverso Gianini

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

A Lean 4 / Mathlib formalization of Kirkman's 1847 theorem: for v ≥ 1, a Steiner triple system on v points (a family of 3-subsets covering every pair of distinct points exactly once) exists if and only if v ≡ 1 or 3 (mod 6). Sufficiency is proved by Bose's and Skolem's constructions from Steiner quasigroups. Mathlib does not contain Steiner triple systems.

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-000003
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-28-000003/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-000003/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"body": "…", "review": true}'