Formalization of the Fundamental Group in Untyped Set Theory Using Auto2

摘要

We present a new framework for formalizing mathematics in untyped set theory using auto2. Using this framework, we formalize in Isabelle/FOL the entire chain of development from the axioms of set theory to the definition of the fundamental group for an arbitrary topo-logical space. The auto2 prover is used as the sole automation tool, and enables succinct proof scripts throughout the project.