Convex Functions in ACL2(r)
This work is incremental, advancing formal verification in theorem proving for convex optimization, primarily benefiting researchers in formal methods and mathematical analysis.
The paper formalizes convex functions in ACL2(r) by proving a set of theorems, including Nesterov's theorem on convex functions with Lipschitz continuous gradients, which to the authors' knowledge has not been fully published before.
This paper builds upon our prior formalisation of R^n in ACL2(r) by presenting a set of theorems for reasoning about convex functions. This is a demonstration of the higher-dimensional analytical reasoning possible in our metric space formalisation of R^n. Among the introduced theorems is a set of equivalent conditions for convex functions with Lipschitz continuous gradients from Yurii Nesterov's classic text on convex optimisation. To the best of our knowledge a full proof of the theorem has yet to be published in a single piece of literature. We also explore "proof engineering" issues, such as how to state Nesterov's theorem in a manner that is both clear and useful.