Formalization of Two Fixed-Point Algorithms in Hilbert Spaces
Yifan Bai, Yantao Li, Jian Yu, Jingwei Liang
math.OC
Feb 19, 2026 · v1
TL;DR
Formalizes convergence of Krasnoselskii-Mann and Halpern fixed-point iterations for nonexpansive operators in real Hilbert spaces in Lean 4.
Abstract
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, we then formalize the Fejér monotone sequence. Building on these foundations, we verify the convergence of both the iteration schemes. Our formalization provides reusable components for machine-checked convergence analysis of fixed-point iterations and theories of convex analysis in real Hilbert spaces. Our code is available at
https://github.com/TTony2019/fixed-point-iterations-in-lean.
Problem
Krasnoselskii-Mann iteration and Halpern iteration are fundamental fixed-point algorithms for nonexpansive operators in Hilbert spaces, but their convergence properties have not been formally verified in a proof assistant.
Approach
The authors formalize in Lean 4 the convergence of both Krasnoselskii-Mann iteration (weak convergence) and Halpern iteration (strong convergence) for nonexpansive operators. They first develop the weak topology and topological properties in infinite-dimensional real Hilbert spaces, then formalize nonexpansive operators and Fejer monotone sequences as foundational tools. The formalization builds on Mathlib's type-dependent theory.
Results
The formalization provides reusable Lean 4 components for machine-checked convergence analysis of fixed-point iterations and convex analysis in real Hilbert spaces, addressing gaps in Mathlib's coverage of weak topology. The code is publicly available.
