{"id":"palomar/PALOMAR-2026-08-22-000007","url":"https://github.com/ashebson/kinin-lean/tree/d8ca202e6ccd655bd9c49dad5b9ee724cd3c2f54","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-08-22-000007-v1.json","repo":"https://github.com/ashebson/kinin-lean","tags":["math.CO","msc:05A17","msc:90C27","mishnah","combinatorics","lean-formalization"],"score":0,"title":"ashebson/kinin-lean","trust":"high","domain":"math.CO","source":"palomar","authors":["Aryeh Shebson"],"reviews":0,"subject":"math.CO","summary":"A Lean 4 formalization of all sixteen units of Mishnah Kinnim, with a machine-checked physical optimization theorem for the Koppel--Reiss reading of Kinnim 3:2. For any list of pair counts grouped by owner, the priest has already acted on exactly half of the mixed birds above and half below. A physical world records one action level for every individual bird of every owner. Lean proves that every such world is compatible, by permutation, with the fixed half-split action list. Counting valid birds directly from each owner's closed-pair quota, the theorem proves that the exact minimum over all…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-08-22","reactions":{},"formalized":true,"formalizes":[{"title":"Seder Kinnim: A Mathematical Commentary on Tractate Kinnim","identifier":"","relationship":"formalizes"},{"title":"A Mathematical Proof of Kinnim 3:2","identifier":"doi:10.2307/40914641","relationship":"formalizes"}]}