Symmetric prime pairs around for
OpenWeakGoldbach.symmetric_prime_pair_above_2e18goldbachnumber-theoryprimes
For every natural number there exists such that both and are prime.
This is the symmetric form of the even Goldbach conjecture: writing shows that it is exactly equivalent to the claim that every even is a sum of two primes. It is the formulation targeted by symmetric-window approaches to the conjecture.
Preamble
import Mathlib
Formal statement
namespace WeakGoldbach
theorem symmetric_prime_pair_above_2e18 (m : ℕ) (hm : 2 * 10 ^ 18 < m) :
∃ t : ℕ, t ≤ m - 2 ∧ Nat.Prime (m - t) ∧ Nat.Prime (m + t) := by
sorry
end WeakGoldbachSource
Symmetric reformulation of the Goldbach conjecture; cf. the covariance-lemma reduction program (Bahbouhi, ai.viXra 2512.0013)