Source indexedtheorem · leanprover/lean4:v4.32.0

Goldbach.helfgott_odd_goldbach_finite

PrimeNumberTheoremAnd.IEANTN.Goldbach · PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:184 to 200

Mathematical statement

Exact Lean statement

@[blueprint
  "helfgott-odd-goldbach-finite"
  (title := "Helfgott's verification of odd Goldbach for small $n$")
  (statement := /-- \cite[Appendix C]{helfgott-goldbach-arxiv}
  The odd Goldbach conjecture is verified up to $1.1325 \times 10^{26}$. -/)
  (proof := /-- Combine Proposition \ref{e-silva-herzog-piranian-even-goldbach},
  Proposition \ref{even-to-odd-goldbach-triv}, and Theorem \ref{thm:ramare-saouter2003}. -/)
  (latexEnv := "proposition")
  (discussion := 969)]
theorem helfgott_odd_goldbach_finite : odd_conjecture (11325 * 10 ^ 22)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

@[blueprint  "helfgott-odd-goldbach-finite"  (title := "Helfgott's verification of odd Goldbach for small $n$")  (statement := /-- \cite[Appendix C]{helfgott-goldbach-arxiv}  The odd Goldbach conjecture is verified up to $1.1325 \times 10^{26}$. -/)  (proof := /-- Combine Proposition \ref{e-silva-herzog-piranian-even-goldbach},  Proposition \ref{even-to-odd-goldbach-triv}, and Theorem \ref{thm:ramare-saouter2003}. -/)  (latexEnv := "proposition")  (discussion := 969)]theorem helfgott_odd_goldbach_finite : odd_conjecture (11325 * 10 ^ 22) := by  have h1 := even_to_odd_goldbach 10726905042 (4 * 10 ^ 18) 28314000    (fun x hx => RamareSaouter2003.has_prime_in_interval x (by norm_cast : (x : ℝ) > 10726905041))    e_silva_herzog_piranian_goldbach  have h2 := odd_conjecture_mono (4 * 10 ^ 18 + 3) 10726905046    (even_to_odd_goldbach_triv _ e_silva_herzog_piranian_goldbach)  norm_num at *  exact odd_conjecture_mono _ _ (h1 h2) (by grind)