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

Jaume de Dios Pont, Lukas Liehr, David Muñoz-Lahoz, Mitchell A. Taylor, Pedro Tradacete

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.

Disclosure

“a single finite case. Another substantial group of contributions concerned free products and push-outs of vector lattices, Archimedean vector lattices, and Banach lattices. In an ongoing project by G. Martı́nez- Fernández and PT, the LLM helped formulate and prove several results about preservation of injectivity in categorical constructions. For example, in a push-out square of vector lattices S1”
PDF page 12

Classification: Substantial mathematical content or result generation
Multiplier: 10
Verified: 2026-08-23T05:00:13.859946Z

Structural counts

Pages 17 pdf

Theorems 0 source

Lemmas 0 source

Propositions 0 source

Corollaries 0 source

Definitions 0 source

Displayed equations 9 source

Bibliography entries 77 source

Appendix pages 0 estimated

Count notes

Source counts use the expanded primary TeX file main.tex.
Appendix pages include the first PDF page with an explicit Appendix heading through the final page.