The Banach lattice Lean library
David Muñoz-Lahoz
math.FA
Aug 7, 2026 · v1
TL;DR
A Lean 4 library formalizing the theory of Banach lattices, with three research-level formalizations built using it.
Abstract
We present a Lean 4 library for the theory of Banach lattices. Its purpose is to support the systematic formalization of contemporary research in Banach lattices and related areas. As evidence of this, we describe three research-level formalizations built using the library. Writing the library at scale was made possible by the use of LLMs with careful human supervision and planning. Unlike autoformalization, this approach allows for an actual understanding of the code. This, in turn, led to new mathematical insights that are also discussed. Judging by the interest expressed by other researchers, we expect the library to become a communal effort in the near future. For this reason, we also describe several parts of the theory that could be added next.
Problem
Contemporary research in Banach lattices and related functional analysis lacks formalized foundations to support systematic verification and further formalization.
Approach
A Lean 4 library for the theory of Banach lattices is developed to support systematic formalization of research-level results. The library was written at scale using LLMs under careful human supervision and planning, distinguished from autoformalization by aiming for genuine understanding of the code. Three research-level formalizations were built on top of the library.
Results
Three research-level formalizations were completed using the library, and the formalization effort yielded new mathematical insights. The authors report interest from other researchers and outline parts of the theory to be added next.
