TY - RPRT TI - Formalization of Line Search Methods by Lean AU - Yiyang Zhang AU - Kenneth W. Shum PY - 2026 UR - https://arxiv.org/abs/2606.25412 ID - 2606.25412 ER -