Experimental formalization and algorithmic investigation of the Belgian Chocolate threshold, including computability-oriented constructions and endpoint analysis. Not a complete solution of the original Belgian Chocolate Problem.
theorem-proving threshold formal-verification control-theory robust-control mathlib computer-assisted-proof computability lean4 certified-computation belgian-chocolate-problem simultaneous-stabilization
-
Updated
Sep 15, 2026 - Lean