### Abstract

This article gives a formal version of Furstenberg's topological proof of the infinitude of primes. He defines a topology on the integers based on arithmetic progressions (or, equivalently, residue classes). Using some fairly obvious properties of this topology, the infinitude of primes is then easily obtained.

Apart from this, this topology is also fairly ‘nice’ in general: it is second countable, metrizable, and perfect. All of these (well-known) facts are formally proven, including an explicit metric for the topology given by Zulfeqarr.

### License

BSD License

### Topics

- Mathematics/Number theory

### Session Furstenberg_Topology

- Furstenberg_Topology

## Cite

×

Furstenberg_Topology-AFP

    @article{Furstenberg_Topology-AFP,
      author  = {Manuel Eberl},
      title   = {Furstenberg's topology and his proof of the infinitude of primes},
      journal = {Archive of Formal Proofs},
      month   = {March},
      year    = {2020},
      note    = {\url{https://isa-afp.org/entries/Furstenberg_Topology.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 18, 2020 : Isabelle2020
- Mar 27, 2020 : Isabelle2019