The Reinhardt Conjecture and Formal Foundations of Optimal Control

Join Zoom Meeting


Meeting ID: 919 7037 2380

Passcode: 259598

Tuesday, November 17, 2020 - 14:00


Speaker Information
Koundinya Vajjha

Abstract or Additional Information

I shall describe a reformulation (following Hales (2017)) of a 1934 conjecture of Reinhardt on pessimal packings of convex domains in the plane as a problem in optimal control theory. General solutions to the associated control problem and a compactification result are presented. I shall argue that this leads to a program for exhaustive computer search for critical points of the full optimal control problem. 

Finally, I will describe a formal proof of convergence (in the proof assistant Coq) of value and policy iteration algorithms in the theory of Markov Decision Processes, which constitute the first results in a program to formalize the basics of optimal control theory.

All are welcome to attend! Please reach out to for questions.