Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: First-Order Methods for Smooth...

Email Gateway (Aug 13 2026 at 06:06):

From: Tobias Nipkow <nipkow@in.tum.de>
Subject: [isabelle] New in the AFP: First-Order Methods for Smooth Convex Optimization in Isabelle/HOL

First-Order Methods for Smooth Convex Optimization in Isabelle/HOL
Feier Lyu

This entry develops reusable Isabelle/HOL infrastructure for first-order methods
in smooth convex optimization. The central application is projected-gradient
descent, but the development is organized around general-purpose interfaces for
gradients, first-order convexity certificates, smooth quadratic upper bounds,
descent and telescoping arguments, projection geometry, projected-gradient
mappings, residual certificates, strong convexity, and linear convergence rates.
The main purpose of the entry is not only to formalize a single convergence
proof, but to separate the analytic, geometric, and algorithmic components of
first-order convergence arguments into reusable Isabelle/HOL layers. The
resulting library can be used as a basis for future formalizations of
constrained first-order optimization methods.

https://isa-afp.org/entries/Projected_Gradient_Descent.html

Enjoy!

smime.p7s

Last updated: Sep 02 2026 at 16:10 UTC