Email Gateway (Aug 01 2025 at 10:58): Email Gateway (Aug 01 2025 at 10:58):From: Lawrence Paulson <lp15@cam.ac.uk>
I am happy to announce a new entry, Unconstrained Optimization, by Dustin Bryant.
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:
• minimizers, strict and isolated local minimizers;
• first- and second-order optimality conditions for scalar real-valued functions;
• first-order optimality conditions for vector-valued functions; and
• a worked example.
The new session provides sound, reusable foundations for future proof-checking tools and mechanized research in optimization, analysis, and algorithmic correctness.
https://www.isa-afp.org/entries/Unconstrained_Optimization.html
Larry Paulson
Last updated: Aug 20 2025 at 20:23 UTC