Documentation

FormalConjectures.ErdosProblems.«141»

Erdős Problem 141 #

References:

source
def Erdos141.Set.IsPrimeProgressionOfLength (s : Set ℕ) (l : ℕ∞) :
Prop

The predicate that a set s consists of l consecutive primes (possibly infinite). This predicate does not assert a specific value for the first term.

Equations
Instances For
    source
    theorem Erdos141.first_three_odd_primes :
    Set.IsPrimeProgressionOfLength {3, 5, 7} 3

    The first three odd primes are an example of three consecutive primes.

    source
    def Erdos141.Set.IsAPAndPrimeProgressionOfLength (s : Set ℕ) (l : ℕ) :
    Prop

    The predicate that a set s is both an arithmetic progression of length l and a progression of l consecutive primes.

    Equations
    Instances For
      source
      theorem Erdos141.exists_three_consecutive_primes_in_ap :
      ∃ (s : Set ℕ), Set.IsAPAndPrimeProgressionOfLength s 3

      There are 3 consecutive primes in arithmetic progression.

      source
      theorem Erdos141.erdos_141 :
      (∀ k ≥ 3, ∃ (s : Set ℕ), Set.IsAPAndPrimeProgressionOfLength s k) ↔ sorry

      Let $k≥3$. Are there $k$ consecutive primes in arithmetic progression?

      source
      theorem Erdos141.erdos_141.variant.first_cases (k : ℕ) :
      k ≥ 3 → k ≤ 10 → ∃ (s : Set ℕ), Set.IsAPAndPrimeProgressionOfLength s k

      The existence of such progressions has been verified for $k≤10$.

      source
      theorem Erdos141.erdos_141.variant.eleven :
      (∃ (s : Set ℕ), Set.IsAPAndPrimeProgressionOfLength s 11) ↔ sorry

      Are there $11$ consecutive primes in arithmetic progression?

      source
      def Erdos141.consecutivePrimeArithmeticProgressions (k : ℕ) :
      Set (Set ℕ)

      The set of arithmetic progressions of consecutive primes of length $k$.

      Equations
      Instances For
        source
        theorem Erdos141.erdos_141.variant.infinite_three :
        (consecutivePrimeArithmeticProgressions 3).Infinite ↔ sorry

        It is open, even for $k=3$, whether there are infinitely many such progressions.

        source
        theorem Erdos141.erdos_141.variant.infinite_general_case (k : ℕ) (hk : k ≥ 3) :
        (consecutivePrimeArithmeticProgressions k).Infinite ↔ sorry

        Fix a $k \geq 3$. Is it true that there are infinitely many arithmetic prime progressions of length $k$?