{"id":"arxiv/2602.17064","url":"https://arxiv.org/abs/2602.17064","tags":["math.OC"],"score":0,"title":"Formalization of Two Fixed-Point Algorithms in Hilbert Spaces","domain":"math.OC","source":"arxiv","authors":["Yifan Bai","Yantao Li","Jian Yu","Jingwei Liang"],"reviews":0,"subject":"math.OC","summary":"Iterative algorithms are fundamental tools for approximating fixed-points of nonexpansive operators in real Hilbert spaces. Among them, Krasnosel'skiĭ--Mann iteration and Halpern iteration are two widely used schemes. In this work, we formalize the convergence of these two fixed-point algorithms in the interactive theorem prover Lean4 based on type dependent theory. To this end, weak convergence and topological properties in the infinite-dimensional real Hilbert space are formalized. Definition and properties of nonexpansive operators are also provided. As a useful tool in convex analysis,…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"discussed":0,"published":"2026-02-19","reactions":{}}