Conic Linear Optimization for Computer-Assisted Proofs

  • Etienne de Klerk

    Tilburg University, Netherlands
  • Didier Henrion

    LAAS-CNRS, Université de Toulouse, France
  • Frank Vallentin

    Universität zu Köln, Germany
  • Angelika Wiegele

    Alpen-Adria Universität Klagenfurt, Austria

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.

Cite this article

Etienne de Klerk, Didier Henrion, Frank Vallentin, Angelika Wiegele, Conic Linear Optimization for Computer-Assisted Proofs. Oberwolfach Rep. 19 (2022), no. 2, pp. 1039–1089

DOI 10.4171/OWR/2022/20