Formalization of Line Search Methods by Lean
This paper presents a formalization of line search methods in the Lean 4 theorem prover. Our goal is to advance machine verification of nonlinear optimization theory by translating standard textbook definitions and convergence arguments into rigorous Lean code. We formalize fundamental notions related to gradient descent and descent directions, adaptive step-size selection via backtracking line search, and several classical line search criteria, including the Armijo, Goldstein, and Wolfe conditions, as well as nonmonotone variants. We further formalize a key convergence result, namely the…
Comments and reviews
No comments yet.
API
curl /api/v1/records/arxiv/2606.25412
curl -X POST /api/v1/records/arxiv/2606.25412/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/arxiv/2606.25412/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'