collaborators

1 paper

math.OC2026

Formalization of Line Search Methods by Lean

Yiyang Zhang, Kenneth W. Shum

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…