Counting Steiner triple systems: Wilson (1974) and Linial–Luria (2013)
A complete Lean 4 / Mathlib formalization of R. M. Wilson's "Nonisomorphic Steiner triple systems" (inequality (2.1), Theorems 1–4, Lemmas 3–5, including the exact numbers of Latin squares of orders 6, 7 and 8 and the bounds N(19) ≥ 2450, N(21) ≥ 2160980, N(25) ≥ 163929929318400) and of N. Linial and Z. Luria's "An upper bound on the number of Steiner triple systems" (Theorems 1.1 and 1.2 with explicit error terms). Version 2 adds a proof of the van der Waerden permanent theorem (Egorychev, Falikman), following Gurvits's proof as simplified by Laurent and Schrijver. The parts of Wilson's…
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-10-22-000017
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-22-000017/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-22-000017/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'