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.

翻译：数值与符号优化方法广泛应用于工程、工业及金融领域。研究者常采用多种方法将待求解问题转换为便于现有软件处理的约简形式。本文基于Lean编程语言与交互式定理证明器，构建了用于设计及应用此类约简方法的框架。形式化验证提升了流程的可靠性，而交互式框架与环境数学库的可用性，则为约简构造及其推理提供了稳健环境。