Optimization is used extensively in engineering, industry, and finance, and various methods are used to transform problems to the point where they are amenable to solution by numerical methods. We describe progress towards developing a framework, based on the Lean interactive proof assistant, for designing and applying such reductions in reliable and flexible ways.

翻译：优化在工程、工业和金融领域广泛使用,并采用各种方法将问题转化为以数字方法解决的问题,我们描述在开发一个框架方面取得的进展,该框架以利恩互动验证助理为基础,以可靠和灵活的方式设计和应用这种削减。