Wikipedia · research open · AMS 13
unsolvedsorry — nobody on it
Pierce–Birkhoff conjecture
Conjecture · pierce_birkhoff_conjecture
The Pierce-Birkhoff conjecture states that for every real piecewise-polynomial function
f : ℝⁿ → ℝ, there exists a finite set of polynomials gᵢⱼ ∈ ℝ[x₁, ..., xₙ] such that
f = supᵢ infⱼ(gᵢⱼ).
Formal statement · Lean 4.lean
theorem pierce_birkhoff_conjecture {n : ℕ} (f : (Fin n → ℝ) → ℝ)
(hf : IsPiecewiseMvPolynomial f) :
∃ (ι κ : Type) (g : ι → κ → MvPolynomial (Fin n) ℝ), Finite ι ∧ Finite κ ∧
∀ x, f x = ⨆ i, ⨅ j, MvPolynomial.eval x (g i j) := by
sorryProof. sorry
Nobody has tried yet.