Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: Furstenberg's topology and his...


view this post on Zulip Email Gateway (Aug 23 2022 at 08:34):

From: "Thiemann, René" <Rene.Thiemann@uibk.ac.at>
Dear all,

I’m happy to announce a new AFP entry by Manuel Eberl.

Furstenberg's topology and his proof of the infinitude of primes

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.

More details at: https://www.isa-afp.org/entries/Furstenberg_Topology.html

Enjoy and stay healthy,
René


Last updated: Apr 25 2024 at 20:15 UTC