HEXAGONbeta

A Formally Verified Certificate Proof of the Maximum Number of Stable Matchings for Six Men and Six Women

Primarily AI-generated textHuman understanding: no partsmath.CO — Combinatoricscs.DM — Discrete Mathematics

Contributed by YURAN XIU ↗

Version 1 / Oct 16, 2026 / CC BY 4.0

Abstract

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 weighted frontier recurrence counts these ideals, and a sum of permanents bounds every future continuation. These bounds yield a finite certificate with 135,828 states. The complete argument, including the reduction for arbitrary profiles, certificate soundness, all concrete checks, and an attaining profile, has been formalized and checked in Lean 4. The final unconditional theorem depends only on the standard axioms of Lean and mathlib.

Provenance statement

The research, formalization, and manuscript were developed with OpenAI Codex assistance. The complete unconditional theorem was checked in Lean 4.27.0 with pinned mathlib dependencies, a statement-match audit, and a transitive axiom audit. The verification package includes the sources, certificate, pinned versions, reproduction instructions, and successful checking logs. Lean verification is separate from the human-understanding declaration.

Tools used

Lean
LeanVersion 4.27.0

References

  1. D. Gale and L. S. Shapley. College admissions and the stability of marriage. The American Mathematical Monthly 69(1) (1962), 9--15. doi:10.1080/00029890.1962.11989827 (https://doi.org/10.1080/00029890.1962.11989827).DOI
  2. A. T. Benjamin, C. Converse, and H. A. Krieger. How do I marry thee? Let me count the ways. Discrete Applied Mathematics 59(3) (1995), 285--292. doi:10.1016/0166-218X(95)80006-P (https://doi.org/10.1016/0166-218X(95)80006-P).DOI
  3. M. Jo. Small rotation blocks and the order-six stable marriage problem. Zenodo preprint, first deposited 20 September 2026, doi:10.5281/zenodo.22860585 (https://doi.org/10.5281/zenodo.22860585). Version v09, 23 September 2026, doi:10.5281/zenodo.22909380 (https://doi.org/10.5281/zenodo.22909380). Theorem and section references are to v09.DOI
  4. E. G. Thurber. Concerning the maximum number of stable matchings in the stable marriage problem. Discrete Mathematics 248 (2002), 195--219. doi:10.1016/S0012-365X(01)00194-7 (https://doi.org/10.1016/S0012-365X(01)00194-7).DOI
  5. A. R. Karlin, S. Oveis Gharan, and R. Weber. A simply exponential upper bound on the maximum number of stable matchings. In Proceedings of STOC 2018 , 920--925. arXiv:1711.01032 (https://arxiv.org/abs/1711.01032).arXiv
  6. C. Palmer and D. Pálvölgyi. At most 3.55n3.55^n stable matchings. arXiv:2011.00915v2 (https://arxiv.org/abs/2011.00915v2), 2021.arXiv
  7. L. Cai and C. Thomas. Representing all stable matchings by walking a maximal chain. arXiv:1910.04401 (https://arxiv.org/abs/1910.04401), 2019.arXiv
  8. M. Borodin, A. Duncan, B. Litchev, J. Liu, V. Moroz, M. Qian, R. Raghavan, G. Rastogi, M. Voigt, and T. Khovanova. Sequences of the stable matching problem. Journal of Integer Sequences 27 (2024), Article 24.2.2. https://cs.uwaterloo.ca/journals/JIS/VOL27/Khovanova/khova32.html.link
  9. D. Eilers. Sequence A357269: maximum number of stable matchings in the stable marriage problem. The On-Line Encyclopedia of Integer Sequences . https://oeis.org/A357269. Accessed 15 October 2026.link
  10. D. Eilers. Sequence A357271: lower bounds for the maximum number of stable matchings in the stable marriage problem based on composing smaller instances. The On-Line Encyclopedia of Integer Sequences . https://oeis.org/A357271. Accessed 15 October 2026.link
Show all 11 referencesShow fewer references
  1. D. Eilers. Sequence A351413: maximum number of stable matchings in the Latin marriage problem. The On-Line Encyclopedia of Integer Sequences . Includes the dihedral construction attributed to C. Converse's 1992 thesis. https://oeis.org/A351413. Accessed 15 October 2026.link

Version history

  1. v1Submitted by YURAN XIURevised after moderator-requested changesCurrentOct 16, 2026