AI 中文总结
本文介绍用于巴拿赫格理论的Lean 4库，借助带人工监督的LLMs构建，可支持相关研究的形式化，已完成三项研究级形式化，有望成为集体成果。
AI 中文摘要
我们推出了用于巴拿赫格理论的Lean 4库，其目的是支持巴拿赫格及相关领域当代研究的系统形式化。作为例证，我们描述了使用该库构建的三项研究级形式化工作。通过在人工监督与规划下使用大型语言模型（LLMs），才得以大规模编写该库。与自动形式化不同，此方法能实现对代码的实际理解，进而获得了新的数学见解，本文也对此进行了讨论。从其他研究人员表现出的兴趣来看，我们预计该库将在不久的将来成为一项集体工作，因此我们还描述了理论中接下来可添加的几个部分。
英文摘要
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.
