Prime patterns and conjectures

Twin primes and Brun's constant, Hardy–Littlewood tuples, Goldbach/Lemoine-type statements, primes represented by polynomials (Friedlander–Iwaniec).

TheoremClement's criterion for twin primes#✓fully proved

For every natural number \(p \ge 2\), the numbers \(p\) and \(p + 2\) are both prime if and only if

\[4\bigl((p-1)! + 1\bigr) + p \equiv 0 \pmod{p(p+2)}.\]

The hypothesis \(p \ge 2\) is needed: the unqualified restatement in the Journal of Integer Sequences is false at \(p = 1\).

Sources: * JIS restatement: https://cs.uwaterloo.ca/journals/JIS/VOL13/Schmidt/multifact.tex, lines 3295-3306. * Corrected domain: M. Chaves, Twin Primes and a Primality Test by Indivisibility, arXiv:math/0211034v3, source lines 110-121, citing P. A. Clement, Congruences for Sets of Primes, Amer. Math. Monthly 56 (1949), 23.

theorem clement_twin_prime_criterion :
    ∀ (p : ℕ), 2 ≤ p →
      (Nat.Prime p ∧ Nat.Prime (p + 2) ↔
        Nat.ModEq (p * (p + 2)) (4 * (Nat.factorial (p - 1) + 1) + p) 0)

TheoremFriedlander–Iwaniec theorem#●ready to prove

There are infinitely many primes \(p\) of the form \(p = a^2 + b^4\) with \(a\) and \(b\) natural numbers.

public theorem_wanted friedlander_iwaniec : {p : ℕ | p.Prime ∧ ∃ a b, p = a ^ 2 + b ^ 4}.Infinite
Sources
  • Friedlander, John, and Henryk Iwaniec. “The Polynomial X² + Y⁴ Captures Its Primes.” Annals of Mathematics, vol. 148, no. 3, 1998, pp. 945–1040. JSTOR, https://doi.org/10.2307/121034. Problem friedlander_iwaniec of the lean-eval benchmark.

TheoremLemoine's conjecture up to \(10^{13}\)#●ready to prove

Every odd natural number \(n\) with \(5 < n \le 10^{13}\) can be written as \(n = p + 2q\) with \(p\) and \(q\) prime.

public theorem_wanted lemoine_of_le_ten_pow_thirteen (n : ℕ) (hn : Odd n) (h5 : 5 < n)
    (hle : n ≤ 10 ^ 13) : ∃ p q : ℕ, p.Prime ∧ q.Prime ∧ n = p + 2 * q
Sources
  • Zsófia Juhász, Máté Bartalos, Péter Magyar, and Gábor Farkas, Empirical Verification of a Generalization of Goldbach's Conjecture, Journal of Integer Sequences 27 (2024), Article 24.4.3, abstract (jis-2024-24.4.3-abstract-main).
1 fully proved2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.