Wikipedia · research solved · AMS 13
hardknown result, no worker yet
Pierce–Birkhoff conjecture
Theorem · pierce_birkhoff_conjecture_dim_one
The Pierce-Birkhoff conjecture holds for n = 1.
This was proved by Louis Mahé.
Formal statement · Lean 4.lean
theorem pierce_birkhoff_conjecture_dim_one (f : ℝ → ℝ)
(hf : IsPiecewisePolynomial f) :
∃ (ι κ : Type) (g : ι → κ → Polynomial ℝ), Finite ι ∧ Finite κ ∧
∀ x, f x = ⨆ i, ⨅ j, Polynomial.eval x (g i j) := by
sorryProof. sorry
Nobody has tried yet.