Prime values of polynomials

DefinitionBunyakovsky condition#✓fully proved

An integer polynomial \(f \in \mathbb{Z}[x]\) satisfies the Bunyakovsky condition when it has degree at least \(1\), is irreducible in \(\mathbb{Z}[x]\), and has positive leading coefficient.

Unlike the hypothesis of Bunyakovsky's conjecture, this condition does not require the values of \(f\) to have no common prime divisor.

def BunyakovskyCondition (f : ℤ[X]) : Prop :=
  1 ≤ f.degree ∧ Irreducible f ∧ 0 < f.leadingCoeff
Used by 1
Used bySchinzel's Hypothesis H gives numbers that are primary \(5\)- and \((-11)\)-Carmichael

DefinitionSchinzel condition#✓fully proved

A finite set \(F\) of integer polynomials satisfies the Schinzel condition when it has no fixed prime divisor: for every prime \(p\) there is a natural number \(n\) such that \(p\) divides none of the values \(f(n)\) for \(f \in F\).

def SchinzelCondition (fs : Finset ℤ[X]) : Prop :=
  ∀ p : ℕ, p.Prime → ∃ n : ℕ, ∀ f ∈ fs, ¬(p : ℤ) ∣ f.eval (n : ℤ)
Used by 1
Used bySchinzel's Hypothesis H gives numbers that are primary \(5\)- and \((-11)\)-Carmichael

TheoremInfinitely many primes of the form \(4k^2 + 2k + 1\)#●ready to prove

There are infinitely many natural numbers \(k\) such that \(4k^2 + 2k + 1\) is prime.

The source derives this from its Conjecture A (Bunyakovsky's conjecture). Only this polynomial is stated here, not the full Bunyakovsky conjecture nor the companion polynomial \(9k^2 + 6k + 2\).

theorem_wanted conjectureA_prime_values_four_square :
    Set.Infinite {k : ℕ | Nat.Prime (4 * k ^ 2 + 2 * k + 1)}
Sources
2 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.