Conic Linear Optimization for Computer-Assisted Proofs

Abstract

From a mathematical perspective, optimization is the science of proving inequalities. In this sense, computational optimization is a method for computer-assisted proofs.

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. For many cones this problem is computationally tractable, and as a result there is a growing number of computer-assisted 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.