Conic Linear Optimization for Computer-assisted Proofs

Abstract

Conic (linear) optimization is the problem of minimizing a linear functional over the intersection of a convex cone with an affine subspace of a topological vector space. Examples of conic linear optimization problems include semidefinite programming in the finite-dimensional case, and the generalised problem of moments in the infinite-dimensional case. Here, the underlying cones are the cone of positive semidefinite matrices, and the cone of positive Borel measures (with given support), respectively.

Since the 1980s, efficient algorithms have been developed for (certain) conic optimization problems. The use of computers makes it possible to prove inequalities with (near-) optimal constants or (near-) optimal weights which otherwise would be completely out of reach with classical pen and paper reasoning. Also the field of conic optimization has a powerful duality theory. This duality theory makes it relatively easy to verify rigorously the obtained numerical computer-assisted proofs without for instance using extensive case by case checking.

Thus there has been a flood of new proofs using conic optimization in discrete geometry, (extremal) graph theory, numerical analysis, and other fields, the most famous example perhaps being the proof of the Kepler Conjecture.

The aim of this workshop was to bring researchers from these diverse fields together to work towards expanding the current scope of conic optimization as a method of generating proofs, and to identify problems and challenges to work on together.

This workshop was a follow-up on the (half) workshop in 2022 of the same name (Oberwolfach Workshop 2215b).