Topological proofs of the infinitude of primes

DefinitionPositive integers coprime to a given integer#✓fully proved

For a positive integer \(n\), \(\Omega_n\) is the set of positive integers \(m\) with \(\gcd(n, m) = 1\).

def coprimeSet (n : ℕ+) : Set ℕ+ :=
  {m | Nat.Coprime (n : ℕ) (m : ℕ)}

Used by 1

Used byMacías's coprime basis

DefinitionMacías's coprime basis#✓fully proved

For a positive integer \(n\) let \(\Omega_n\) be the set of positive integers coprime to \(n\). Macías's coprime basis is the family \(\beta = \{\Omega_n : n \ge 1\}\) of subsets of the positive integers.

def maciasBasis : Set (Set ℕ+) :=
  Set.range coprimeSet

Uses 1 · Used by 2

Statement usesPositive integers coprime to a given integer

Used byMacías's coprime sets form a basis · Macías's coprime topology

DefinitionMacías's coprime topology#✓fully proved

For a positive integer \(n\) let \(\Omega_n\) be the set of positive integers coprime to \(n\). Macías's coprime topology \(\tau\) is the topology on the positive integers generated by the sets \(\Omega_n\), \(n \ge 1\), that is, the coarsest topology in which every \(\Omega_n\) is open.

@[instance_reducible] def maciasTopology : TopologicalSpace ℕ+ :=
  TopologicalSpace.generateFrom maciasBasis

Uses 1 · Used by 7

Statement usesMacías's coprime basis

Used byClosure of a prime in Macías's coprime topology · Coprime arithmetic progressions are dense in the comaximal space · Density of the primes passes from the subspace without 1 · A nonempty set of primes is dense in the comaximal space iff it is infinite · Infinitude of the primes as density · Macías's coprime sets form a basis · Macías's coprime topology without 1

DefinitionMacías's coprime topology without 1#✓fully proved

The topology \(\tau_1\) on the set of positive integers different from \(1\) is the subspace topology induced by Macías's coprime topology \(\tau\) on the positive integers.

@[instance_reducible] def maciasTopology₁ : TopologicalSpace {x : ℕ+ // (x : ℕ) ≠ 1} :=
  TopologicalSpace.induced Subtype.val maciasTopology

Uses 1 · Used by 2

Statement usesMacías's coprime topology

Used byThe primes are dense in the coprime topology without 1 · Density of the primes passes from the subspace without 1

DefinitionPrimes among the positive integers#✓fully proved

The set of positive integers that are prime numbers.

def primeSet : Set ℕ+ :=
  {p | Nat.Prime (p : ℕ)}

Used by 2

Used byDensity of the primes passes from the subspace without 1 · Infinitude of the primes as density

DefinitionPrimes among the positive integers different from 1#✓fully proved

Within the set of positive integers different from \(1\), this is the subset consisting of the prime numbers.

def primeSet₁ : Set {x : ℕ+ // (x : ℕ) ≠ 1} :=
  {x | Nat.Prime ((x : ℕ+) : ℕ)}

Used by 2

Used byThe primes are dense in the coprime topology without 1 · Density of the primes passes from the subspace without 1

TheoremMacías's coprime sets form a basis#●ready to prove

For a positive integer \(n\) let \(\Omega_n\) be the set of positive integers coprime to \(n\). The family \(\beta = \{\Omega_n : n \ge 1\}\) is a basis of the topology on the positive integers that it generates (Macías's coprime topology).

theorem_wanted maciasBasis_isTopologicalBasis :
    @TopologicalSpace.IsTopologicalBasis ℕ+ maciasTopology
      maciasBasis

Sources

• Jhixon Macías, "Another Topological Proof of the Infinitude of Prime Numbers", Theorem 1.

Uses 2

Statement usesMacías's coprime basis · Macías's coprime topology

TheoremClosure of a prime in Macías's coprime topology#●ready to prove

If \(p\) is a prime number, then the closure of \(\{p\}\) in the positive integers with Macías's coprime topology is the set of positive integers divisible by \(p\).

theorem_wanted closure_singleton_prime_eq_multiples
    (p : ℕ+) (hp : Nat.Prime (p : ℕ)) :
    @closure ℕ+ maciasTopology {p} = {x : ℕ+ | (p : ℕ) ∣ (x : ℕ)}

Sources

• Jhixon Macías, "Another Topological Proof of the Infinitude of Prime Numbers", Lemma 1.

Uses 1

Statement usesMacías's coprime topology

TheoremInfinitude of the primes as density#●ready to prove

There are infinitely many prime numbers if and only if the set of prime numbers is dense in the positive integers with Macías's coprime topology.

theorem_wanted infinite_primes_iff_dense_primeSet :
    Set.Infinite {p : ℕ | Nat.Prime p} ↔
      @Dense ℕ+ maciasTopology primeSet

Sources

• Jhixon Macías, "Another Topological Proof of the Infinitude of Prime Numbers", Theorem 2.

Uses 2

Statement usesMacías's coprime topology · Primes among the positive integers

TheoremDensity of the primes passes from the subspace without 1#●ready to prove

Let \(X\) be the positive integers with Macías's coprime topology and \(X_1\) the subspace of positive integers different from \(1\). If the set of prime numbers is dense in \(X_1\), then it is dense in \(X\).

theorem_wanted dense_primeSet_of_dense_primeSet₁ :
    @Dense {x : ℕ+ // (x : ℕ) ≠ 1} maciasTopology₁ primeSet₁ →
      @Dense ℕ+ maciasTopology primeSet

Sources

• Jhixon Macías, "Another Topological Proof of the Infinitude of Prime Numbers", Lemma 2.

Uses 4

Statement usesMacías's coprime topology · Macías's coprime topology without 1 · Primes among the positive integers · Primes among the positive integers different from 1

TheoremThe primes are dense in the coprime topology without 1#●ready to prove

The set of prime numbers is dense in the set of positive integers different from \(1\), with the subspace topology induced by Macías's coprime topology on the positive integers.

theorem_wanted dense_primeSet₁ :
    @Dense {x : ℕ+ // (x : ℕ) ≠ 1} maciasTopology₁ primeSet₁

Sources

• Jhixon Macías, "Another Topological Proof of the Infinitude of Prime Numbers", Theorem 3.

Uses 2

Statement usesMacías's coprime topology without 1 · Primes among the positive integers different from 1

TheoremA nonempty set of primes is dense in the comaximal space iff it is infinite#●ready to prove

Equip the positive integers with the comaximal topology, the topology generated by the sets \(\{m : \gcd(n, m) = 1\}\) for positive integers \(n\). A nonempty set \(A\) of primes is infinite if and only if it is dense in this topology.

public theorem_wanted infinite_iff_dense_maciasTopology_of_subset_primes (A : Set ℕ+)
    (hA : A.Nonempty) (hAp : ∀ p ∈ A, Nat.Prime (p : ℕ)) :
    A.Infinite ↔ @Dense ℕ+ maciasTopology A

Sources

• Jhixon Macías, A Topological Proof of the Infinitude of Prime Numbers in Certain Arithmetic Progressions, INTEGERS 26 (2026), Article A39, Lemma 1 (quoting Macías, INTEGERS 24 (2024), Article A47).

Uses 1

Statement usesMacías's coprime topology

TheoremCoprime arithmetic progressions are dense in the comaximal space#●ready to prove

Equip the positive integers with the comaximal topology, the topology generated by the sets \(\{m : \gcd(n, m) = 1\}\) for positive integers \(n\). If \(a\) and \(b\) are coprime positive integers, then the arithmetic progression \(\{ak + b : k \in \mathbb{N}\} = \{b, a + b, 2a + b, \dots\}\), with \(k\) ranging over the natural numbers including \(0\), is dense in this topology.

public theorem_wanted dense_maciasTopology_arithmeticProgression (a b : ℕ+)
    (hab : Nat.Coprime a b) :
    @Dense ℕ+ maciasTopology {m : ℕ+ | ∃ k : ℕ, (m : ℕ) = a * k + b}

Sources

• Jhixon Macías, A Topological Proof of the Infinitude of Prime Numbers in Certain Arithmetic Progressions, INTEGERS 26 (2026), Article A39, Lemma 2.

Uses 1

Statement usesMacías's coprime topology

6 fully proved7 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.