Euclid Numbers conjecture

Reference: Wikipedia

noncomputable def EuclidNumbers.Euclid (n : ℕ) : ℕ

The n-th Euclid number is the product of the first n prime numbers plus one.

Equations

• EuclidNumbers.Euclid n = 1 + ∏ i ∈ Finset.range n, Nat.nth Nat.Prime i

theorem EuclidNumbers.infinite_prime_euclid_numbers : {n : ℕ | Nat.Prime (Euclid n)}.Infinite ↔ sorry

It is not known whether there is an inifinite number of prime Euclid numbers.

theorem EuclidNumbers.euclid_numbers_are_square_free : (∀ (n : ℕ), Squarefree (Euclid n)) ↔ sorry

It is not known whether every Euclid number is a square-free number.