  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.
