Mechanizing set theory. Cardinal arithmetic and the axiom of choice (Q5961491)

The authors use a proof assistant, the Isabelle Logical Framework, to establish some fairly deep results of Zermelo-Fraenkel set theory. The results, which are formally proven, concern cardinal arithmetic and the axiom of choice. The proofs require results from theories of orders, order-isomorphisms, order types, ordinal arithmetic, cardinals, etc., which covers most of the first chapter of Kunen's set theory book. Overall, the paper is a valuable contribution to the growing corpus of machine checked mathematics.