Formalization of Line Search Methods by Lean (Q7270083)
From MaRDI portal
!
This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use the normal view instead:
No description defined
| Language | Label | Description | Also known as |
|---|---|---|---|
| default for all languages | No label defined |
||
| English | Formalization of Line Search Methods by Lean |
No description defined |
Statements
Formalization of Line Search Methods by Lean (English)
0 references
24 June 2026
0 references
math.OC
0 references
cs.MS
0 references
math.NA
0 references
Yiyang Zhang
0 references
Kenneth W. Shum
0 references
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.
0 references
Formalization
0 references
Line Search
0 references
Lean 4
0 references
