Unconstrained Optimization

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.