Papers With

← All papers
First page of Banach lattices and phase retrieval: A case study for the use of AI in mathematics

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

math.FA Aug 7, 2026 · v1
formalization analysis theorem-proving-ml
Read PDF arXiv abstract Code
TL;DR
Banach lattice results including Kakutani's C(K)-representation theorem were formalized and verified in Lean alongside LLM-assisted research in phase retrieval.
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.
Problem

Large language models can assist mathematical research but their outputs are unreliable. A group in Banach lattice theory and phase retrieval sought to incorporate LLMs into their workflow while ensuring correctness.

Approach

The team coupled LLM-assisted discovery with Lean verification of results. They built a Lean library of Banach lattice facts, revisiting the classical theory and its dependency structure. Kakutani's C(K)-representation theorem was formalized in Lean over roughly one month. Students and senior members contributed under strict disclosure and quality standards.

Results

Kakutani's C(K)-representation theorem was formalized in Lean (publicly available). The process led to a deeper understanding of the field's geometry, a more united community, and new plans for courses, conferences, and Lean libraries on analysis formalization.