Formalization of the fundamental group in untyped set theory using auto2

TL;DR

This paper introduces a new framework for formalizing the fundamental group within untyped set theory using the auto2 prover, enabling concise proofs from axioms to topological group definitions.

Contribution

It provides a novel approach to formalizing complex mathematical structures in untyped set theory with automated proof assistance.

Findings

Successful formalization of the fundamental group in Isabelle/FOL

Use of auto2 automation simplifies proof scripts

Complete development from set theory axioms to topological group definition

Abstract

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 topological space. The auto2 prover is used as the sole automation tool, and enables succinct proof scripts throughout the project.