Source indexedtheorem · leanprover/lean4:v4.32.0

Goldbach.e_silva_herzog_piranian_goldbach_ext

PrimeNumberTheoremAnd.IEANTN.Goldbach · PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:206 to 223

Source documentation

The arguments in \cite[Appendix C]{helfgott-goldbach-arxiv} push the bound further than this, but require unpublished estimates of Ramare. However, similar arguments were established in \cite{kadiri-lumley}, and we present them here.

Exact Lean statement

@[blueprint
  "e-silva-herzog-piranian-even-goldbach-ext"
  (title := "e Silva--Herzog--Piranian verification of even Goldbach (extended)")
  (statement := /-- \cite{eSHP}
  The even Goldbach conjecture is verified up to $4 \times 10^{18} + 4$. -/)
  (proof := /-- If $N = 4 \times 10^{18}$, use the fact that $211, 313, N-209, N-309$
  are all prime. -/)
  (latexEnv := "proposition")]
theorem e_silva_herzog_piranian_goldbach_ext : even_conjecture (4 * 10 ^ 18 + 4)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

@[blueprint  "e-silva-herzog-piranian-even-goldbach-ext"  (title := "e Silva--Herzog--Piranian verification of even Goldbach (extended)")  (statement := /-- \cite{eSHP}  The even Goldbach conjecture is verified up to $4 \times 10^{18} + 4$. -/)  (proof := /-- If $N = 4 \times 10^{18}$, use the fact that $211, 313, N-209, N-309$  are all prime. -/)  (latexEnv := "proposition")]theorem e_silva_herzog_piranian_goldbach_ext : even_conjecture (4 * 10 ^ 18 + 4) := by  intro n hn he  simp only [Finset.mem_Icc] at hn  by_cases! h1 : n ≤ 4 * 10 ^ 18  · exact e_silva_herzog_piranian_goldbach n (Finset.mem_Icc.mpr ⟨hn.1, h1⟩) he  · obtain ⟨k, hk⟩ := he    have : n = 4000000000000000002 ∨ n = 4000000000000000004 := by omega    rcases this with rfl | rfl    · exact ⟨211, 3999999999999999791, prime_211, prime_3999999999999999791, by norm_num⟩    · exact ⟨313, 3999999999999999691, prime_313, prime_3999999999999999691, by norm_num⟩