def Goldbach.even_conjecture (H : ℕ) : Prop

theorem Goldbach.even_conjecture_mono (H H' : ℕ) (h : even_conjecture H) (hh : H' ≤ H) : even_conjecture H'

theorem Goldbach.even_goldbach_test : even_conjecture 30

def Goldbach.odd_conjecture (H : ℕ) : Prop

theorem Goldbach.odd_conjecture_mono (H H' : ℕ) (h : odd_conjecture H) (hh : H' ≤ H) : odd_conjecture H'

theorem Goldbach.even_to_odd_goldbach_triv (H : ℕ) (h : even_conjecture H) : odd_conjecture (H + 3)

theorem Goldbach.odd_goldbach_test : odd_conjecture 33

theorem Goldbach.even_to_odd_goldbach (x₀ H Δ : ℕ) (hprime : ∀ x ≥ x₀, HasPrimeInInterval (↑x * (1 - 1 / ↑Δ)) (↑x / ↑Δ)) (heven : even_conjecture H) (hodd : odd_conjecture (x₀ + 4)) : odd_conjecture ((H - 4) * Δ + 4)

theorem Goldbach.richstein_goldbach : even_conjecture (4 * 10 ^ 14)

theorem Goldbach.ramare_saouter_odd_goldbach : odd_conjecture 11325599999999886744004

theorem Goldbach.e_silva_herzog_piranian_goldbach : even_conjecture (4 * 10 ^ 18)

theorem Goldbach.helfgott_odd_goldbach_finite : odd_conjecture (11325 * 10 ^ 22)

theorem Goldbach.e_silva_herzog_piranian_goldbach_ext : even_conjecture (4 * 10 ^ 18 + 4)

theorem Goldbach.kadiri_lumley_odd_goldbach_finite : odd_conjecture (1966196911 * 4 * 10 ^ 18)