2 papers
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…
math.CV2026
Formalizing Extended Complex Numbers, Mobius Transformations, and Cross Ratio in Lean 4
Fubin Yan, Kenneth W. Shum
The extended complex plane is a fundamental object in complex analysis, hyperbolic geometry, and mathematical physics. Its geometry is governed by Möbius transformations, with the…