HackerPapers

arXiv:1707.04757cs.LO

Formalization of the fundamental group in untyped set theory using auto2

Bohua Zhan

Early discovery. Linked by one identifiable commenter. This paper is outside the main ranking; a mention is not an endorsement.

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.

arXiv comments
17 pages, accepted for ITP 2017
Journal reference
ITP 2017, LNCS 10499, pp. 514--530, 2017
DOI
doi:10.1007/978-3-319-66107-0_32
Subjects
cs.LOLogic in Computer Science

On Hacker News

Linked by 1 identifiable commenter in 1 comment across 1 thread, from Feb 2021 to Feb 2021.

Comments linking this paper, per year.

Discussed in comments1 thread

  1. Native Type Theory 1 comment

    • The issue is automation: At this point (Feb 2021), the support in interactive theorem provers is just much better for type-theory based mathematics in contrast to set-theory based maths. Whether that is due to technical advantages of type-theory over set theory, or a historical…

      GregarianChildView on HNParent context

Submitted to Hacker News

Connected through shared HN threads, not inferred similarity or a recommendation.