Proof Pearl: The Marriage Theorem

  • Dongchen Jiang
  • Tobias Nipkow
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 7086)


We describe two formal proofs of the finite version of Hall’s Marriage Theorem performed with the proof assistant Isabelle/HOL, one by Halmos and Vaughan and one by Rado. The distinctive feature of our formalisation is that instead of sequences (often found in statements of this theorem) we employ indexed families, thus avoiding tedious reindexing of sequences.


Induction Hypothesis Theorem Prover Formal Proof Proof Assistant Marriage Problem 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Aigner, M., Ziegler, G.M.: Proofs from the Book. Springer, Heidelberg (2001)CrossRefzbMATHGoogle Scholar
  2. 2.
    Easterfield, T.E.: A combinatorial algorithm. Journal London Mathematical Society 21, 219–226 (1946)MathSciNetCrossRefzbMATHGoogle Scholar
  3. 3.
    Everett, C.J., Whaples, G.: Represetations of sequences of sets. American Journal of Mathematics 71, 287–293 (1949)MathSciNetCrossRefzbMATHGoogle Scholar
  4. 4.
    Hall, P.: On representatives of subsets. Journal London Mathematical Society 10, 26–30 (1935)zbMATHGoogle Scholar
  5. 5.
    Halmos, P.R., Vaughan, H.E.: The marriage problem. American Journal of Mathematics 72, 214–215 (1950)MathSciNetCrossRefzbMATHGoogle Scholar
  6. 6.
    Jiang, D., Nipkow, T.: Hall’s marriage theorem. In: Klein, G., Nipkow, T., Paulson, L. (eds.) The Archive of Formal Proofs (December 2010),; formal proof development
  7. 7.
    Nipkow, T., Paulson, L.C., Wenzel, M.T.: Isabelle/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002)zbMATHGoogle Scholar
  8. 8.
    Rado, R.: Note on the transfinite case of Hall’s Theorem on representatives. Journal London Mathematical Society 42, 321–324 (1967)MathSciNetCrossRefzbMATHGoogle Scholar
  9. 9.
    Romanowicz, E., Grabowski, A.: The Hall marriage theorem. Formalized Mathematics 12(3), 315–320 (2004)Google Scholar
  10. 10.
    Wikipedia: Hall’s marriage theorem — wikipedia, the free encyclopedia (2011), (accessed September 8, 2011]

Copyright information

© Springer-Verlag Berlin Heidelberg 2011

Authors and Affiliations

  • Dongchen Jiang
    • 1
    • 2
  • Tobias Nipkow
    • 2
  1. 1.State Key Laboratory of Software Development EnvironmentBeihang UniversityChina
  2. 2.Institut für InformatikTechnische Universität MünchenGermany

Personalised recommendations