Banach lattices and phase retrieval: A case study for the use of AI in mathematics

David Mu\~noz-Lahoz; Jaume de Dios Pont; Lukas Liehr; Mitchell A. Taylor; Pedro Tradacete

REVIEW 3 major objections 5 minor 29 references

Banach lattices and phase retrieval: A case study for the use of AI in mathematics

T0 review · 3 major / 5 minor · reviewed 2026-08-15 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read This case study reports that pairing LLM-generated proof drafts with Lean verification let a group of analysts produce verified research results, including a 72-hour verified solution to the L2-stability problem for STFT phase retrieval…

desk verdict A candid, readable field report on LLM+Lean in analysis—honest about failures, but the central verification claims are self-reported and not auditable from the text. read the letter →

arxiv 2608.07396 v1 pith:PD25NNY5 submitted 2026-08-07 math.FA

Jaume de Dios Pont , Lukas Liehr , David Muñoz-Lahoz , Mitchell A. Taylor , Pedro Tradacete This is my paper · ORCID

classification math.FA MSC 46B4246A4068V20

keywords interactivetheoremprovingLeanlargelanguagemodelsphaseretrievalBanachlatticesformalverificationautoformalizationSTFT

verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

This paper reports on five months in which a group of researchers in Banach lattice theory and phase retrieval made large language models and the Lean proof checker part of their daily mathematical workflow. The authors' central claim is that the combination of LLM-generated proof ideas with Lean verification produced genuine research progress: a Lean-verified solution to the $L^2$-stability problem for short-time Fourier transform phase retrieval, obtained within 72 hours of an LLM suggesting a strategy, plus fully verified papers and a growing shared library of formalized Banach lattice theory. The aim is not to claim that LLMs replace mathematicians, but that they work as high-speed proof assistants when every output is checked line-by-line or in Lean. The case matters because it sketches a division of labour—models propose, humans judge and generalize, computers check—that could make formal verification a normal part of research-level analysis.

What carries the argument

The central mechanism is the verification loop: an LLM proposes proof strategies and even code, a human mathematician judges, repairs, and generalizes the ideas, and the Lean theorem prover checks the final formal argument. Lean is an interactive theorem prover based on dependent type theory, in which propositions are types, proofs are terms, and the kernel verifies the typing of every term; a theorem is certified when the kernel accepts the term. Within this loop the load-bearing object is the formal statement and its definitions, because Lean certifies only that the statement follows from the axioms, not that the statement means what the mathematician intends; the paper therefore treats statement-writing and definition-review as the highest-risk part of the process, and builds shared, human-audited libraries to keep that risk under control.

What would settle it

Find a Lean-verified theorem from this project whose formal statement has a model that mathematicians would reject as not satisfying the intended result—for instance, a function that satisfies the formal $L^2$-stability inequality but violates the phase-retrieval inequality as physically meant; exhibiting such a mismatch for the STFT stability theorem would falsify the claim that Lean verification closes the reliability gap.

Watch

Extended reading notes

Core claim

The paper's central claim is that a workflow combining large language models and Lean verification can carry research-level mathematics in analysis, and that it did so in this group's recent work. The flagship episode is the $L^2$-stability problem for short-time Fourier transform phase retrieval: an LLM gave a largely incorrect execution of a strategy for the key lemma, the authors saw that the strategy itself was sound, completed the proof, and then obtained a Lean verification of the solution in less than 72 hours. The paper further reports that autoformalizing their first paper produced a new elementary proof; that formalizing a counterexample about regular Gabor frames forced a cleaner, more general statement; that a colleague with almost no prior Lean experience verified a result on Cantor measures with almost no guidance; and that a semiautoformalized Banach lattice library reached a scale that supported three research-level formalizations in two months. The conclusion offered is that LLM exploration plus Lean certification plus human judgment gives trustworthy, sometimes faster mathematics, and that the process itself deepened the community's understanding of its field.

Load-bearing premise

The load-bearing premise is that the Lean statements faithfully encode the authors' intended theorems, since Lean can verify a formal statement but cannot guarantee that the statement expresses the intended mathematics.

Editorial extensions

If this is right

The $L^2$-stability result for STFT phase retrieval is now Lean-verified, so its proof is checked at the level of the formal statement; the authors also report generalizing the argument to all Hermite windows, all finite spans of the canonical basis, and all dimensions.
Autoformalization can improve a proof even when the theorem statement stays fixed: in their first formalized paper it produced a new, more elementary proof alongside the original concentration-compactness argument.
The Banach lattice library, built in about two months of part-time work, made possible the formalization of three research-level results, including a very recent solution to an open question; this suggests reusable libraries are decisive for scaling up the workflow.
Researchers with almost no prior Lean experience can verify results with limited guidance, so the workflow is not limited to formalization experts.
Formal verification catches subtle LLM errors that could easily be missed by human reading alone, which is the authors' stated reason for adopting the workflow.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

If this division of labour becomes common, the scarce human skill shifts from constructing proofs to writing trustworthy formal statements; the paper already implies this by making definitions the most carefully reviewed part of the code.
A testable consequence of the paper's account is that 'right strategy, wrong execution' LLM outputs will be disproportionately valuable on problems close to a research group's expertise, because the humans can recognize and repair the strategy; that could be benchmarked on collections of open problems.
The success of the Banach lattice library suggests that formalization quality and research speed trade off, but the real bottleneck is definitional trust; a community that invests early in audited definitions may reap faster verified results later.
If models are later trained on formal corpora as well as informal text, the rate of correct-but-misstated theorems may rise, making a 'specification gap' review layer—human-readable statements attached to formal ones—a permanent fixture of the workflow.

Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Desk Editor's Note

read the letter

Colleague—

You should know up front: this is not a research paper in mathematics. It's a five-month field report from a group that added LLMs and Lean to their workflow in Banach lattices and phase retrieval. The actual theorems live in external preprints ([1], [4], [14], [15]); this note is about the process and the community.

What's genuinely good: the candor. They document far more failures than successes, name specific failure modes (models using false axioms close to true ones, omitting hypotheses, hiding gaps behind plausible citations), and they explicitly discuss the specification gap—Lean verifies a formal statement, but does not guarantee that statement matches the intended math. That is the central caveat of the whole enterprise, and they put it in print. The account of building a small Banach lattice library, with statements reviewed separately from proofs, is useful practical detail. The community-building angle is refreshing.

The soft spots are the flip side of the genre. The key anecdote—a Lean-verified solution to the L2-stability problem in under 72 hours—is unverifiable from this text. No Lean file, no formal statement, no diff against the informal theorem appears here. The external repositories are cited, not audited. The authors are upfront that only statements and definitions were intensively reviewed, and that even five independent agent checks can certify a completely wrong proof. Given that, the reader has to take the central verification claim on faith. That is not a fatal flaw for a case study, but it means this paper's evidence is testimony, not artifact. Some of the Section 3.8 successes are work in progress, so those are also promises rather than proofs.

Overall: the paper is honest, well-written, and useful for anyone thinking about how AI and formalization fit into research practice. It deserves a serious referee if submitted to a venue on mathematical practice, AI4Math, or a journal like Notices. It should not be treated as a source of new mathematical results. A referee should ask the authors to include or point to at least one concrete, human-readable rendering of a formally verified statement, and to make explicit what exactly "Lean verification of the solution" means for [4]. Without that, the central exhibit is an anecdote.

Referee Report

3 major / 5 minor

Summary. This manuscript is an experiential case study rather than a mathematical research paper. It reports on the authors' roughly five-month effort to use large language models and the Lean theorem prover in their research in Banach lattice theory and phase retrieval. Section 2 sketches the mathematical background; Section 3 recounts early Lean formalization of Kakutani's theorem, an early LLM-assisted hot-spots computation, the autoformalization of [1] and [4], the construction of a Banach lattice library [19], and a series of student projects (Section 3.8), many of which involve LLM-generated proofs that were corrected or abandoned. Sections 4 and 5 discuss community-building and future plans. The paper's stated conclusion is that combining LLM-generated proof ideas with Lean verification has led to verified mathematical results, including an alleged Lean-verified solution to the L2-stability problem for STFT phase retrieval 'in less than 72 hours,' and to a deeper understanding and more unified community.

Significance. If true, the reported workflow is a meaningful methodological development: it would demonstrate that autoformalization can be done at research scale with LLM assistance, that formalization can force simpler proofs, and that Lean can catch subtle errors in LLM output. The authors are candid about failures, including false statements, omitted hypotheses, and the five-independent-agents counterexample, and they explicitly identify the specification gap between informal and formal statements. These features make the paper a useful community document. However, the central evidential claim is not independently checkable as written: the Lean files and formal statements are not included, and the paper's own caveats in Sections 3.5 and 3.7 leave open the possibility that the formal statements do not faithfully express the intended mathematics. The paper is not a contribution to Banach lattice theory or phase retrieval per se.

major comments (3)

[Abstract; §3.3] The claim that the authors 'were able to obtain a Lean verification of the solution in less than 72 hours' is load-bearing and is not checkable from the manuscript. No Lean code, no formal theorem statement, no repository commit hash, and no comparison between the formal statement and the informal theorem in [4] is supplied; the repositories are only cited externally. Please include the exact formal statements and definitions for [1], [4], [14], and [15] in an appendix (or a stable, versioned repository), and for each state which informal theorem it is intended to encode and who performed the encoding review.
[§3.7; §3.5] The paper correctly acknowledges that 'Lean can formally verify the correctness of a statement but it cannot guarantee that the statement faithfully expresses the intended mathematical theorem.' This is exactly the point on which the paper's central inference depends. §3.5 reports that only statements and definitions were intensively reviewed and that these reviews were decoupled from the proofs, while §3.8 documents LLM-generated definitions that were subtly wrong. The manuscript does not describe a protocol that closes this gap for the results it advertises. Please supply the review protocol and, for each verified theorem, a line-by-line mapping from the informal statement to the Lean statement, including the hypotheses that are implicit in the informal version.
[§3.3] The paper never states precisely what mathematical theorem was allegedly verified: the reader is told that the target was 'local stability' at the constant function in one dimension for the Gaussian window, and later that the proof generalizes to 'all Hermite windows' in 'all dimensions,' but no precise theorem statements, stability constants, or function spaces are given. Without these, the claim of a verified solution to an L2-stability problem cannot be assessed even informally. Please state the informal theorem(s) explicitly in the text.

minor comments (5)

[§3.8] Section 3.8 asks the reader to ignore all undefined terms, but several of the terms discussed are central to assessing the claims; please add a short glossary or defer technical statements to an appendix.
[References; §3.5] Reference [19] is cited as 'The Banach lattice Lean library. 2026' with no URL or repository identifier; since it is central to Section 3.5, provide a stable link and version.
[§1.3] The sentence in Section 1.3 listing private companies and initiatives is unverified and not cited; consider removing it or attributing each item to a source.
[§3.4] In Section 3.4, the claim that the proof in [15] was 'correctly Lean verified' should identify which version of the Lean statement and which Mathlib version were used, as the specification gap is especially relevant for a topological counterexample.
[§3.3] The phrase 'less than 72 hours' should specify whether this was wall-clock time, total person-hours, or token-hours, so that the claim can be interpreted accurately.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity: the paper is an experience report, not a derivation, and its central verification claims rest on machine-checked Lean artifacts; the acknowledged specification gap is a correctness limitation, not a circular reduction.

full rationale

This paper is an experience report rather than a mathematical derivation, so the standard circularity failure modes do not directly apply: there is no fitted parameter later called a prediction, no theorem defined in terms of its own conclusion, and no uniqueness theorem imported from the authors' prior work to force a choice. The central claim—that LLM-generated proof strategies combined with Lean verification produced a verified solution to the L2-stability problem for STFT phase retrieval—is supported by self-cited preprints [1], [4], [14], [15] and the library [19]. Although those references overlap heavily with the present authors, the key verification claims are machine-checked in Lean, and under the review rules a machine-checked citation counts as independent support rather than circular self-citation. The paper explicitly acknowledges the main limitation in Section 3.7: 'Lean can formally verify the correctness of a statement but it cannot guarantee that the statement faithfully expresses the intended mathematical theorem,' and Section 3.5 states that only the statement and definitions were intensively reviewed, decoupled from the proof. That is a genuine verification and specification concern, but it is not a circular reduction of the paper's claims to their own inputs. No equation or derivation in this paper is shown to be equivalent to its own premise by construction, and no self-citation chain is used to preclude alternative explanations. The self-referential nature of the evidence and the subjective claims about community and understanding are real epistemic limitations, but they belong under correctness or evidentiary risk, not circularity. Score 0.

Assumptions & free parameters 0 free parameters · 3 assumptions · 0 invented entities

No mathematical derivation is performed, so free parameters and invented entities are absent. The relevant assumptions concern trust in formalization infrastructure and the accuracy of self-reported experiences.

assumptions (3)

domain assumption The Lean kernel and Mathlib provide a sound foundation for the formal proofs.
The paper's trust in its verified results rests on the correctness of the Lean kernel and the Mathlib library, discussed in Section 3.6.
ad hoc to paper The formal statements in the cited repositories correspond to the intended mathematical theorems.
The authors acknowledge the specification gap in Section 3.7 and provide no independent mechanism to ensure correspondence beyond their own review.
ad hoc to paper The reported experiences and verification times are accurately described.
The case study consists of self-reported anecdotes; no logs, certificates, or independent observers are provided.

how reviews work

0 comments

Cite this review

Pith. "Pith review of Banach lattices and phase retrieval: A case study for the use of AI in mathematics." pith.science (2026). https://pith.science/paper/PD25NNY5

@misc{pith2026260807396,
  author       = {Pith},
  title        = {Pith review of: Banach lattices and phase retrieval: A case study for the use of AI in mathematics},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/PD25NNY5}},
  note         = {Machine review of arXiv:2608.07396}
}

read the original abstract

The ability of large language models to assist professional mathematicians has been progressing rapidly. Earlier this year, a group of researchers in Banach lattice theory and phase retrieval began incorporating this technology into their research workflows. Facing challenges about the reliability of these models, they also decided to couple the discovery process with Lean verification. Here, we present a case study of how this has led to a more united community and a deeper understanding of our field.

Review history (2 revisions) →

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

29 extracted references · 22 canonical work pages

[1]

Pedro Abdalla, Jaume de Dios Pont, Jo˜ ao P. G. Ramos, and Mitchell A. Taylor. Stable Phase Retrieval for Spans of Independent Random Variables.arXiv preprint arXiv:2607.06693, 2026

work page Pith review arXiv 2026
[4]

Taylor, and Jo˜ ao P

Susanna Bertolini, Jaume de Dios Pont, Ben Pineau, Mitchell A. Taylor, and Jo˜ ao P. G. Ramos.L 2-Stability for STFT phase retrieval.arXiv preprint arXiv:2605.20527, 2026

arXiv 2026
[14]

Lukas Liehr, Jaume de Dios Pont, and Mitchell A. Taylor. Cantor measures with odd base do not admit Fourier frames.arXiv preprint arXiv:2607.08656, 2026

work page Pith review arXiv 2026
[15]

Lukas Liehr, Jaume de Dios Pont, and Mitchell A. Taylor. On the existence problem of regular Gabor frames. arXiv preprint arXiv:2606.26052, 2026

arXiv 2026
[19]

The Banach lattice Lean library

David Mu˜ noz-Lahoz. The Banach lattice Lean library. 2026

work page 2026
[2]

Mathematicians in the Age of AI.arXiv preprint arXiv:2603.03684, 2026

Jeremy Avigad. Mathematicians in the Age of AI.arXiv preprint arXiv:2603.03684, 2026

arXiv 2026
[3]

Amalgamation and injectivity in Banach lattices.Int

Antonio Avil´ es and Pedro Tradacete. Amalgamation and injectivity in Banach lattices.Int. Math. Res. Not., 2023(2):956–997, 2023

work page 2023
[5]

Bilokopytov, A

E. Bilokopytov, A. Salguero-Alarc´ on, P. Tradacete, and N. Trejo-Arroyo. Splitting and extension properties in Banach lattices. Work in progress

work page

Show all 29 references

[6]

Formalising perfectoid spaces

Kevin Buzzard, Johan Commelin, and Patrick Massot. Formalising perfectoid spaces. InProceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, pages 299–312, 2020

2020
[7]

Advancing mathematics by guiding human intuition with ai.Nature, 600(7887):70–74, 2021

Alex Davies, Petar Veliˇ ckovi´ c, Lars Buesing, Sam Blackwell, Daniel Zheng, Nenad Tomaˇ sev, Richard Tanburn, Peter Battaglia, Charles Blundell, Andr´ as Juh´ asz, et al. Advancing mathematics by guiding human intuition with ai.Nature, 600(7887):70–74, 2021

2021
[8]

The Lean 4 Theorem Prover and Programming Language

Leonardo de Moura and Sebastian Ullrich. The Lean 4 Theorem Prover and Programming Language. InAu- tomated Deduction – CADE 28: 28th International Conference on Automated Deduction, Virtual Event, July 12–15, 2021, Proceedings, page 625–635, Berlin, Heidelberg, 2021. Springer-Verlag

2021
[9]

Garc´ ıa-S´ anchez and P

E. Garc´ ıa-S´ anchez and P. Tradacete. Free dual spaces and free Banach lattices.J. Math. Anal. Appl., 532(2):22,
[10]

Sorries Are Not the Hard Part: An Expert-Review Case Study of a Semi- Autonomous Formalization.arXiv preprint arXiv:2606.13925, 2026

Vasily Ilin and Brian Nugent. Sorries Are Not the Hard Part: An Expert-Review Case Study of a Semi- Autonomous Formalization.arXiv preprint arXiv:2606.13925, 2026

2026
[11]

hot spots

David Jerison and Nikolai Nadirashvili. The “hot spots” conjecture for domains with two axes of symmetry. Journal of the American Mathematical Society, 13(4):741–772, 2000

2000
[12]

Taylor, Justin Baker, Rushil Raghavan, Junyi Zhang, Ying Nian Wu, Andrea L

Eric Jiang, Xiao Liang, Yikai Zhang, Yingjia Wan, Mengting Li, Haikang Deng, Alexander K. Taylor, Justin Baker, Rushil Raghavan, Junyi Zhang, Ying Nian Wu, Andrea L. Bertozzi, Kai-Wei Chang, Raghu Meka, Matthew Sottile, Nanyun Peng, Amit Sahai, Terence Tao, and Wei Wang. From ...

2026 arXiv
[13]

Mathematical methods and human thought in the age of AI.arXiv preprint arXiv:2603.26524, 2026

Tanya Klowden and Terence Tao. Mathematical methods and human thought in the age of AI.arXiv preprint arXiv:2603.26524, 2026

2026
[16]

Improved upper bounds for the Hot Spots constant of Lipschitz domains.Potential Analysis, 59(2):771–787, 2023

Phanuel Mariano, Hugo Panzo, and Jing Wang. Improved upper bounds for the Hot Spots constant of Lipschitz domains.Potential Analysis, 59(2):771–787, 2023

2023
[17]

Free Products of Banach Lattices.arXiv preprint arXiv:2605.28988, 2026

Gonzalo Mart´ ınez-Fern´ andez and Pedro Tradacete. Free Products of Banach Lattices.arXiv preprint arXiv:2605.28988, 2026

2026 arXiv
[18]

Autoformalize your math.https://lean.functionalanalysismadrid.com/

David Mu˜ noz-Lahoz. Autoformalize your math.https://lean.functionalanalysismadrid.com/
[20]

Taylor, Pedro Tradacete, and Vladimir G

Timur Oikhberg, Mitchell A. Taylor, Pedro Tradacete, and Vladimir G. Troitsky. Free Banach lattices.J. Eur. Math. Soc. (JEMS), 28(10):4387–4514, 2026

2026
[21]

Sharp bounds on the failure of the hot spots conjecture.arXiv preprint arXiv:2508.16321, 2025

Jaume de Dios Pont, Alexander W Hsu, and Mitchell A Taylor. Sharp bounds on the failure of the hot spots conjecture.arXiv preprint arXiv:2508.16321, 2025

2025 arXiv
[22]

Formalizing mathematics at scale.arXiv preprint arXiv:2605.29955, 2026

Ahmad Rammal, Niket Patel, Fabian Gloeckle, Amaury Hayat, Julia Kempe, Remi Munos, Charles Arnal, and Vivien Cabannes. Formalizing mathematics at scale.arXiv preprint arXiv:2605.29955, 2026

2026 arXiv
[23]

Liquid tensor experiment.Experimental Mathematics, 31(2):349–354, 2022

Peter Scholze. Liquid tensor experiment.Experimental Mathematics, 31(2):349–354, 2022

2022
[24]

An upper bound on the hot spots constant.Revista Mathematica Iberoamericana, 39(4), 2023

Stefan Steinerberger. An upper bound on the hot spots constant.Revista Mathematica Iberoamericana, 39(4), 2023

2023
[25]

Machine-assisted proof.Notices of the American Mathematical Society, 72(1):6–13, 2025

Terence Tao. Machine-assisted proof.Notices of the American Mathematical Society, 72(1):6–13, 2025

2025
[26]

The integrated explicit analytic number theory network : a progress report

Terence Tao. The integrated explicit analytic number theory network : a progress report. Conference talk at Techniques and Tools for the Formalization of Analysis, Institute for Computational and Experimental Research in Mathematics (ICERM), 2026

2026
[27]

The Lean Mathematical Library

The mathlib Community. The Lean Mathematical Library. InProceedings of the 9th ACM SIGPLAN Interna- tional Conference on Certified Programs and Proofs, CPP 2020, New Orleans, LA, USA, January 2020. ACM

2020
[28]

On proof and progress in mathematics

William P Thurston. On proof and progress in mathematics. In18 Unconventional essays on the nature of mathematics, pages 37–55. Springer, 2006. Center for Data Science, New York University, New York, New York 10011, USA Email address:jdedios@nyu.edu Department of Mathematics, ...

2006
[2024]

BANACH LATTICES AND PHASE RETRIEV AL: A CASE STUDY FOR THE USE OF AI IN MATHEMATICS 17

Id/No 127931. BANACH LATTICES AND PHASE RETRIEV AL: A CASE STUDY FOR THE USE OF AI IN MATHEMATICS 17

Pith tools

Reviewed August 15, 2026 · model on record in the stance chip above.

[1] [1]

Pedro Abdalla, Jaume de Dios Pont, Jo˜ ao P. G. Ramos, and Mitchell A. Taylor. Stable Phase Retrieval for Spans of Independent Random Variables.arXiv preprint arXiv:2607.06693, 2026

work page Pith review arXiv 2026

[2] [4]

Taylor, and Jo˜ ao P

Susanna Bertolini, Jaume de Dios Pont, Ben Pineau, Mitchell A. Taylor, and Jo˜ ao P. G. Ramos.L 2-Stability for STFT phase retrieval.arXiv preprint arXiv:2605.20527, 2026

arXiv 2026

[3] [14]

Lukas Liehr, Jaume de Dios Pont, and Mitchell A. Taylor. Cantor measures with odd base do not admit Fourier frames.arXiv preprint arXiv:2607.08656, 2026

work page Pith review arXiv 2026

[4] [15]

Lukas Liehr, Jaume de Dios Pont, and Mitchell A. Taylor. On the existence problem of regular Gabor frames. arXiv preprint arXiv:2606.26052, 2026

arXiv 2026

[5] [19]

The Banach lattice Lean library

David Mu˜ noz-Lahoz. The Banach lattice Lean library. 2026

work page 2026

[6] [2]

Mathematicians in the Age of AI.arXiv preprint arXiv:2603.03684, 2026

Jeremy Avigad. Mathematicians in the Age of AI.arXiv preprint arXiv:2603.03684, 2026

arXiv 2026

[7] [3]

Amalgamation and injectivity in Banach lattices.Int

Antonio Avil´ es and Pedro Tradacete. Amalgamation and injectivity in Banach lattices.Int. Math. Res. Not., 2023(2):956–997, 2023

work page 2023

[8] [5]

Bilokopytov, A

E. Bilokopytov, A. Salguero-Alarc´ on, P. Tradacete, and N. Trejo-Arroyo. Splitting and extension properties in Banach lattices. Work in progress

work page