The Banach lattice Lean library
David Muñoz-Lahoz
math.FA
Aug 7, 2026 · v2
TL;DR
Develops a Lean 4 library for Banach lattice theory, built with LLM assistance under human supervision, and uses it for three research-level formalizations.
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 on Banach lattices lacks infrastructure for systematic formalization in Lean. A dedicated library is needed so research-level results in this area can be machine-checked.
Approach
The authors build a Lean 4 library covering the theory of Banach lattices. They write it at scale with large language models under careful human planning and supervision, as opposed to autoformalization. This keeps the resulting code understandable to its authors. They then use the library to carry out three research-level formalizations.
Results
The library supports three research-level formalizations. Working on it led to new mathematical insights, which the paper discusses. The authors also outline parts of the theory that could be added next as a community effort.
