# Mathematical Discovery in the Wild: AI-Guided Proofs in Banach Space Theory

arXiv: https://arxiv.org/abs/2607.17388 · HTML: https://mlsanity.com/paper/2607.17388/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 18 of its 75 references that are in the map.
- First posted on arXiv 19 Jul 2026.

## Builds on (most cited first, 18 of 18)

- [The AI Scientist: Towards Fully Automated Open-Ended Scientific Discovery](https://mlsanity.com/paper/2408.06292/) (2024)
- [AlphaEvolve: A coding agent for scientific and algorithmic discovery](https://mlsanity.com/paper/2506.13131/) (2025)
- [The AI Scientist-v2: Workshop-Level Automated Scientific Discovery via Agentic Tree Search](https://mlsanity.com/paper/2504.08066/) (2025)
- [FrontierMath: A Benchmark for Evaluating Advanced Mathematical Reasoning in AI](https://mlsanity.com/paper/2411.04872/) (2024)
- [Kosmos: An AI Scientist for Autonomous Discovery](https://mlsanity.com/paper/2511.02824/) (2025)
- [Mathematical exploration and discovery at scale](https://mlsanity.com/paper/2511.02864/) (2025)
- [Aristotle: IMO-level Automated Theorem Proving](https://mlsanity.com/paper/2510.01346/) (2025)
- [Towards Autonomous Mathematics Research](https://mlsanity.com/paper/2602.10177/) (2026)
- [First Proof](https://mlsanity.com/paper/2602.05192/) (2026)
- [Automated Conjecture Resolution with Formal Verification](https://mlsanity.com/paper/2604.03789/) (2026)
- [Toward Generalist Autonomous Research via Hypothesis-Tree Refinement](https://mlsanity.com/paper/2606.11926/) (2026)
- [AI co-mathematician: Accelerating mathematicians with agentic AI](https://mlsanity.com/paper/2605.06651/) (2026)
- [IMProofBench: Benchmarking AI on Research-Level Mathematical Proof Generation](https://mlsanity.com/paper/2509.26076/) (2025)
- [Generative Modeling for Mathematical Discovery](https://mlsanity.com/paper/2503.11061/) (2025)
- [LemmaBench: A Live, Research-Level Benchmark to Evaluate LLM Capabilities in Mathematics](https://mlsanity.com/paper/2602.24173/) (2026)
- [Aletheia tackles FirstProof autonomously](https://mlsanity.com/paper/2602.21201/) (2026)
- [First Proof Second Batch](https://mlsanity.com/paper/2606.18119/) (2026)
- [Iteris: Agentic Research Loops for Computational Mathematics](https://mlsanity.com/paper/2606.02484/) (2026)

## Abstract (arXiv)

We investigate the capacity of current language models to contribute to mathematical research. In Banach space theory, AI systems generated key ideas and proofs for five new results, which were then verified and refined by humans. We also developed an automated system that searches the literature for open problems and attempts solutions at scale. Our results show both the potential of language models for mathematical discovery and the continuing importance of expert verification.