{"id":"palomar/PALOMAR-2026-10-22-000017","url":"https://github.com/jtraverso/counting-steiner-triple-systems/tree/52fda83038df7442c576e17edffba591db703cb8","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-22-000017-v2.json","repo":"https://github.com/jtraverso/counting-steiner-triple-systems","tags":["math.CO","msc:05B07","msc:05B15","msc:05A16","combinatorial-designs","steiner-triple-systems","latin-squares","lean"],"score":0,"title":"Counting Steiner triple systems: Wilson (1974) and Linial–Luria (2013)","trust":"high","domain":"math.CO","source":"palomar","authors":["Juan Pablo Traverso Gianini"],"reviews":0,"subject":"math.CO","summary":"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…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-22","reactions":{},"formalized":true,"formalizes":[{"title":"Nonisomorphic Steiner triple systems","identifier":"doi:10.1007/BF01215371","relationship":"formalizes"},{"title":"An upper bound on the number of Steiner triple systems","identifier":"doi:10.1002/rsa.20487","relationship":"formalizes"},{"title":"On Leonid Gurvits's proof for permanents","identifier":"doi:10.4169/000298910X523380","relationship":"formalizes"}]}