Advancing Mathematical Research via Human-AI Interactive Theorem Proving

TL;DR

This paper presents a human-AI collaborative workflow for mathematical theorem proving that leverages large language models to enhance research efficiency while ensuring mathematical rigor.

Contribution

It introduces a novel human-in-the-loop approach integrating LLMs into theorem proving and scientific computing workflows, demonstrated through a case study on quantum algorithms.

Findings

LLMs assist in proof search and theorem discovery.

The workflow accelerates exploration of mathematical structures.

Framework maintains transparency and rigor in AI-assisted research.

Abstract

We investigate how large language models can be used as research tools in scientific computing while preserving mathematical rigor. We propose a human-in-the-loop workflow for interactive theorem proving and discovery with LLMs. Human experts retain control over problem formulation and admissible assumptions, while the model searches for proofs or contradictions, proposes candidate properties and theorems, and helps construct structures and parameters that satisfy explicit constraints, supported by numerical experiments and simple verification checks. Experts treat these outputs as raw material, further refine them, and organize the results into precise statements and rigorous proofs. We instantiate this workflow in a case study on the connection between manifold optimization and Grover's quantum search algorithm, where the pipeline helps identify invariant subspaces, explore Grover-compatible retractions, and obtain convergence guarantees for the retraction-based gradient method. The framework provides a practical template for integrating large language models into frontier mathematical research, enabling faster exploration of proof space and algorithm design while maintaining transparent reasoning responsibilities. Although illustrated on manifold optimization problems in quantum computing, the principles extend to other core areas of scientific computing.