We gratefully acknowledge support from
the Simons Foundation and member institutions.
Full-text links:


Current browse context:


Change to browse by:

References & Citations

DBLP - CS Bibliography


(what is this?)
CiteULike logo BibSonomy logo Mendeley logo del.icio.us logo Digg logo Reddit logo ScienceWISE logo

Computer Science > Logic in Computer Science

Title: Verified reductions for optimization

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.
Subjects: Logic in Computer Science (cs.LO); Optimization and Control (math.OC)
MSC classes: 90C25, 68V15
Cite as: arXiv:2301.09347 [cs.LO]
  (or arXiv:2301.09347v3 [cs.LO] for this version)

Submission history

From: Alexander Bentkamp [view email]
[v1] Mon, 23 Jan 2023 10:25:48 GMT (52kb,D)
[v2] Tue, 24 Jan 2023 16:38:03 GMT (52kb,D)
[v3] Wed, 22 Feb 2023 15:37:56 GMT (52kb,D)

Link back to: arXiv, form interface, contact.