The Banach lattice Lean library

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.

Disclosure

“(funded by Universidad Autónoma de Madrid), by grants PID2024-162214NB-I00 and CEX2023-001347-S (funded by MCIN/AEI/10.13039/501100011033), and by the CSIC cooperation grant COOPB25033 under the i-COOP program. AI disclosure GPT-5.5 and Claude Opus 4.6 were used to write the code in § banlat. In the process of writing the paper, GPT-5.5 was only used to search for typos and other obvious errors in final versions of the text, and to generate the list of files with their docstrings (wh”

PDF page 25

Classification

Code generation, completion, or debugging

Multiplier

2

Verified

2026-08-23T05:00:01.054614Z

Structural counts