  Fairly deep results of Zermelo-Frenkel (ZF) set theory have been mechanized
using the proof assistant Isabelle. The results concern cardinal arithmetic and
the Axiom of Choice (AC). A key result about cardinal multiplication is K*K =
K, where K is any infinite cardinal. Proving this result required developing
theories of orders, order-isomorphisms, order types, ordinal arithmetic,
cardinals, etc.; this covers most of Kunen, Set Theory, Chapter I. Furthermore,
we have proved the equivalence of 7 formulations of the Well-ordering Theorem
and 20 formulations of AC; this covers the first two chapters of Rubin and
Rubin, Equivalents of the Axiom of Choice, and involves highly technical
material. The definitions used in the proofs are largely faithful in style to
the original mathematics.
