Unconstrained Optimization

Dustin Bryant 📧

July 16, 2025

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

Abstract

As formal methods gain traction in machine learning and numerical analysis, the community needs computer-checked proofs of core optimization results. Existing Isabelle libraries still lack a foundational framework for unconstrained optimization. We close this gap with a comprehensive Isabelle/HOL development that formalizes:

  1. minimizers, strict and isolated local minimizers;
  2. first- and second-order optimality conditions for scalar functions \( f : \mathbb{R} \to \mathbb{R} \);
  3. first-order optimality conditions for vector functions \( g : \mathbb{R}^{n} \to \mathbb{R} \); and
  4. a worked example showing that the continuous function \[ h(x) = \begin{cases} x^{4} \left( \cos(1/x) + 2 \right), & \text{if } x \neq 0, \\[4pt] 0, & \text{if } x = 0 \end{cases} \] has a strict but non-isolated local minimizer at \( x = 0 \).

The new session Unconstrained_Optimization provides sound, reusable foundations for future proof-checking tools and mechanized research in optimization, analysis, and algorithmic correctness.

License

BSD License

Topics

Session Unconstrained_Optimization