2021/11/12 by Alexander Bentkamp, Bentkamp, Alexander, Jeremy Avigad +1
Computer Science · #Logic, programming, and type systems #Formal Methods in Verification #Spreadsheets and End-User Computing
paper · pdf · doi:10.48550/arxiv.2111.06807
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.