therefore
Sign up
Open navigation
All open problems
Source labels openChecked July 26, 2026

MathOverflowField theory and polynomials

Mathoverflow 339137

Let P(x),Q(x)∈R[x]P(x), Q(x) ∈ ℝ[x] be two monic polynomials with non-negative coefficients. If R(x)=P(x)Q(x)R(x) = P(x)Q(x) is a 0,10,1 polynomial (coefficients only from {0,1}\{0,1\}), then P(x)P(x) and Q(x)Q(x) are also 0,10, 1 polynomials.

Field theory and polynomialsAMS 12

Mathematical statement

Let P(x),Q(x)∈R[x]P(x), Q(x) ∈ ℝ[x] be two monic polynomials with non-negative coefficients. If R(x)=P(x)Q(x)R(x) = P(x)Q(x) is a 0,10,1 polynomial (coefficients only from {0,1}\{0,1\}), then P(x)P(x) and Q(x)Q(x) are also 0,10, 1 polynomials.

Statement source: MathOverflow statement material

Statement terms: CC-BY-SA-4.0

Attributed source material. Reuse must follow the linked attribution and share-alike terms.

Statement artifacts, not proofs

These records expose exact Lean propositions and statement-only wrappers. Defining a proposition does not supply a proof of it. A placeholder-bearing target also contains no proof. Elaboration checks syntax and types; it does not certify that a formalization perfectly captures every nuance of the informal problem.

Pinned Lean formulation 1

mathoverflow_339137

Canonical source
Complete statement target, proof intentionally absentLean 4
theorem mathoverflow_339137 (P Q R : ℝ[X]) (hP: P.Monic) (hQ : Q.Monic)    (hp : ∀ c ∈ P.coeffs, 0 ≤ c) (hq : ∀ c ∈ Q.coeffs, 0 ≤ c)    (h : R = P * Q) (hR : IsZeroOne R) :    IsZeroOne P ∧ IsZeroOne Q := by  sorry
Statement source
Formal Conjectures
Lean version
v4.27.0
Placeholder
Present; no proof artifact
Source evidence
Pinned source index
Fidelity review
Community formulation

References

Pinned Formal Conjectures sourceformalizationmathoverflow/339137background*Sil*background