polynomial_goldbach_conjecture
Provedalgebragraph-theorynumber-theorypolynomials
Polynomial Goldbach analogue: Can every polynomial of degree ≥ 2 with integer coefficients be written as a sum of two irreducible polynomials? Analogue of Goldbach's conjecture in the polynomial ring ℤ[x]. Open for integer polynomials; proved over finite fields for most cases.
Preamble
import Mathlib
Formal statement
import Mathlib
theorem polynomial_goldbach_conjecture (p : Polynomial ℤ)
(hdeg : 2 ≤ p.natDegree)
(hirr : Irreducible p)
(hlc : 0 < p.leadingCoeff) :
∃ (q r : Polynomial ℤ),
Irreducible q ∧ Irreducible r ∧ p = q + r := by
sorrySource