Summary of "The Banach lattice Lean library"

Summary (Overview)

• Comprehensive Lean 4 library: The paper presents § banlat, a Lean 4 library for the theory of Banach lattices, designed to support systematic formalization of contemporary research in the field.
• Three research-level formalizations: The library enabled formalization of (1) the free Banach lattice generated by a Banach space, (2) a solution to Wickstead's open problem on positive projections, and (3) a counterexample showing σ-Lebesgue property is not preserved under completion.
• Semiautoformalization approach: The library was written using LLMs with careful human supervision, striking a balance between scale (via AI assistance) and mathematical understanding (via human oversight).
• New mathematical insights: The process yielded novel results, including an elementary proof that lattice-linear expressions vanishing on ℝ vanish on all vector lattices, and a clarification of the solid interior of convex sets.
• Community expectation: The author anticipates the library becoming a communal effort, with several researchers already expressing interest in contributing.

---

Introduction and Theoretical Foundation

Motivation

The paper addresses the growing need for formal verification in mathematics, particularly in Banach lattice theory. With the volume of published research being "costly and difficult to check," formalization offers a path toward systematic verification. The author positions this work within the spectrum of formalization approaches:

"In the levels of quality of formalization introduced by T. Tao, this project would lie somewhere between levels 2 (Publication-level formalization) and 3 (Prototype-level formalization)."

The Semiautoformalization Philosophy

The author distinguishes three approaches:

• Manual formalization (as in mathlib): highest quality, most readable, but slow
• Semiautoformalization (this project): LLM-written code with human steering
• Autoformalization: fully automated, but often lacks mathematical understanding

The key trade-off is scale vs. code quality: proofs are generally not checked by humans, but the speed allows formalization of research-level results in reasonable time.

Why Banach Lattices?

Banach lattices sit at the intersection of:

• Analysis: as Banach spaces with additional structure
• Order theory: as vector lattices with a complete lattice norm

The order-theoretic approach proved ideal for formalization because it starts close to existing mathlib content, while the field has a "cohesive and supportive community" willing to contribute.

---

Methodology

Semiautoformalization Workflow

The author describes a careful, human-supervised process:

1. Careful planning of library organization
2. Keeping LLM tasks close and within reach to prevent design decisions by the AI
3. Correcting unnatural approaches proposed by LLMs for transparency
4. Human expertise required in both Banach lattices and Lean

Library Structure

The library is organized into several modules:

---

Empirical Validation / Results

2.1 Free Banach Lattice Generated by a Banach Space

The free Banach lattice FBL[E] is constructed via the free norm:

$$\|f\|_{\mathrm{FBL}[E]} = \sup\left\{\sum_{k=1}^{n} |f(x_k^*)|: n \in \mathbb{N}, x_1^*, \dots, x_n^* \in B_{E^*}, \sup_{x \in B_E} \sum_{k=1}^{n} |x_k^*(x)| \leq 1\right\}$$

The space is defined as:

$$C_0 = \left\{f \in C(B_{E^*}): \|f\|_{\mathrm{FBL}[E]} < \infty\right\}$$

FBL[E] is the closed sublattice generated by $\{\delta_x : x \in E\}$ where $\delta_x(x^*) = x^*(x)$. The universal property (Theorem 2.3) states: for every Banach lattice X and bounded operator $T: E \to X$, there exists a unique lattice homomorphism $\hat{T}: \mathrm{FBL}[E] \to X$ with $\|\hat{T}\| = \|T\|$ satisfying $\hat{T}\delta = T$.

2.2 Wickstead's Problem on Positive Projections

Theorem 2.4 (main_CK): Let K be a non-empty compact Hausdorff space, $P: C(K) \to C(K)$ a positive projection with $P\mathbb{1}_K = \mathbb{1}_K$. If there exists $\alpha \geq 0$ satisfying:

• (i) $\alpha \, \mathrm{id}_{C(K)} \leq P$
• (ii) if $0 \leq M_f \leq P$, then $\|f\|_\infty \leq \alpha$

Then either $\alpha = 0$ or $\alpha = 1/n$ for some $n \in \mathbb{N}$.

Corollary 2.5 (main): For a non-zero Dedekind complete vector lattice X with positive projection P having constant diagonal α, either $\alpha = 0$ or $\alpha = 1/n$.

This solves an open problem and yields non-representable Banach lattice algebras (Proposition 2.6).

2.3 σ-Lebesgue Completion Counterexample

Proposition 2.7: There exists a σ-Lebesgue Hausdorff locally convex-solid vector lattice whose completion is not σ-Lebesgue — answering Open Problem 8.1 in [1] negatively.

3.1 Vanishing Lattice-Linear Expressions

Theorem 3.4: A lattice-linear expression that vanishes on ℝ must also vanish on every vector lattice.

The proof uses a novel elementary approach discovered by the LLM, avoiding the axiom of choice. Key ingredients:

Lemma 3.5: If for all $(\lambda_1, \dots, \lambda_n) \in \mathbb{R}^n$:

$$\sum_{j=1}^{n} \lambda_j p_j \leq \bigvee_{i=1}^{m} \sum_{j=1}^{n} \lambda_j a_{ij}$$

then $\mathbf{p} \in \mathrm{conv}(\mathbf{a}_1, \dots, \mathbf{a}_m)$.

Normal Form Theorem (3.10): Every lattice-linear expression is equivalent to one of the form:

$$\Phi[t_1, \dots, t_n] = \bigvee_{i=1}^{m} \sum_{k=1}^{n} a_{ik} t_k - \bigvee_{j=1}^{l} \sum_{k=1}^{n} b_{jk} t_k$$

This led to the llarith tactic for closing non-strict inequalities in vector lattices.

3.2 Archimedean Property Subtlety

The paper highlights a discrepancy between mathlib's definition and the vector lattice convention:

• mathlib (3.11): For $x, y \in R$ with $0 < y$, there exists $n \in \mathbb{N}$ with $x \leq ny$
• Vector lattices (3.12): If $ny \leq x$ for all $n \in \mathbb{N}$, then $y \leq 0$

These differ in general (e.g., $\mathbb{R}^2$ with pointwise order satisfies 3.12 but not 3.11).

3.3 Locally Convex-Solid Topologies

The paper clarifies that a locally convex-solid topology admits a neighbourhood basis at 0 formed by sets that are both convex and solid — a fact assumed without proof in [2].

Proposition 3.15: The solid interior of a convex set is convex, where:

$$\operatorname{SolInt}(S) = \{x \in S: [-|x|, |x|] \subseteq S\}$$

---

Theoretical and Practical Implications

For Formal Verification

• Scale is achievable: Research-level results can be formalized in reasonable time using semiautoformalization
• Verification pipeline: Systematic formalization could make paper checking easier — "to check the correctness of a paper we would only need to check the correctness of the formalization"
• Library as trusted foundation: A shared library avoids re-checking the definition tree back to mathlib

For Mathematics

• New proofs discovered: The elementary proof of Theorem 3.4 (vanishing of lattice-linear expressions) is novel, avoiding the axiom of choice and working for all vector lattices
• Subtle gaps identified: The solid-interior convexity result (Proposition 3.15) fills a gap in the standard monograph [2]
• Definitional discrepancies: The paper highlights how formalization exposes inconsistencies between conventions (Archimedean property, order completeness terminology)

For AI-Assisted Research

• LLMs as collaborators: The LLM "taught us how to approach certain results" — a genuine two-way interaction
• Efficiency considerations: Keeping LLM tasks small and well-specified keeps token usage efficient
• Alignment with Tau Ceti: The philosophy aligns with the Lean FRO's new "repository of formal mathematics, directed by human-written roadmaps"

---

Conclusion

The paper presents a significant milestone in the formalization of Banach lattice theory. The § banlat library demonstrates that:

1. Semiautoformalization works: With careful human supervision, LLMs can produce research-level formalizations at scale
2. Formalization yields mathematical insights: The process uncovered new proofs and clarified subtle points
3. Community building is underway: The library is positioned to become a communal effort

Future Directions

The author lists several extension directions:

• Locally solid topologies: Extending Meyer-Nieberg and Andô theorems
• Order continuous operators: Proving Ogasawara's theorem
• Orthomorphisms and f-algebras: Including universal completions
• Nakano theory: Carriers and null ideals
• Free Banach lattices: Further properties
• Atomic and order continuous Banach lattices
• Enriched examples: Ideals, bands in C(K) and L$_p$(μ)
• Positively homogeneous function calculus
• Convex/concave Banach lattices

In the long term, the author hopes to "distill from the library the contents that could be welcome in mathlib, rewrite them to have the appropriate code quality, and contribute them" — giving back to the communal effort that mathlib represents.