A Formally Verified Certificate Proof of the Maximum Number of Stable Matchings for Six Men and Six Women
We give a complete Lean 4 verification of the theorem that the maximum number of stable matchings for six men and six women with strict complete preferences is f(6)=48. Jo (2026) previously proved the unrestricted upper bound, and Benjamin, Converse, and Krieger (1995) supplied an attaining construction. Our contribution is an alternative, fully formalized proof using a finite certificate; the value 48 and the unrestricted theorem are already known. We reduce stable matchings of arbitrary profiles to order ideals of sequences of cyclic partner exchanges in which no man revisits a partner. A…
Comments and reviews
No comments yet.
API
curl /api/v1/records/hexagon/2610.00262
curl -X POST /api/v1/records/hexagon/2610.00262/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/hexagon/2610.00262/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'