Formalization of Line Search Methods by Lean

DOI10.48550/arXiv.2606.25412MaRDI QIDQ7270083arXivFDO

Authors Yiyang Zhang, Kenneth W. Shum

Publication date 24 June 2026

Published in arXiv

Tldr We formalize standard textbook line search methods using Lean 4. This paper provides a comprehensive formalization of fundamental notions and convergence arguments for gradient descent and descent directions, backtracking line search, classical and nonmonotone line search criteria, and the Zoutendijk theorem, advancing machine verification of nonlinear optimization theory.

Full work available at URL https://doi.org/10.48550/arXiv.2606.25412

arXiv classification

cs.MSmath.NAmath.OC

This page was built for publication: Formalization of Line Search Methods by Lean

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q7270083)