Verified reductions for optimization

TL;DR

This paper introduces a formal framework using the Lean proof assistant to design and verify problem reductions in optimization, enhancing reliability and robustness in engineering, industry, and finance applications.

Contribution

It presents a novel approach to formally verify optimization problem reductions using Lean, improving trustworthiness and reproducibility of the reduction process.

Findings

Framework successfully verifies optimization reductions.

Enhanced reliability through formal proof verification.

Provides a robust environment for constructing and reasoning about reductions.

Abstract

Numerical and symbolic methods for optimization are used extensively in engineering, industry, and finance. Various methods are used to reduce problems of interest to ones that are amenable to solution by such software. We develop a framework for designing and applying such reductions, using the Lean programming language and interactive proof assistant. Formal verification makes the process more reliable, and the availability of an interactive framework and ambient mathematical library provides a robust environment for constructing the reductions and reasoning about them.