# Advancing Mathematical Research via Human-AI Interactive Theorem Proving
**Authors**: Chenyi Li, Zhijian Lai, Dong An, Jiang Hu, Zaiwen Wen
> Beijing International Center for Mathematical Research, Peking University, Beijing, 100871, People’s Republic of China
> Yau Mathematical Sciences Center, Tsinghua University, Beijing, 100190, People’s Republic of China
> Corresponding author. Beijing International Center for Mathematical Research, Peking University, Beijing, 100871, People’s Republic of China
## 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.
## 1 Introduction
Recent advances in artificial intelligence, especially large language models, show strong capabilities in analyzing long text [zhang2020pegasus], consolidating domain knowledge [lewis2019bart], and supporting literature grounded querying through retrieval augmented pipelines [lewis2020retrieval]. They also achieve steady gains in stepwise mathematical reasoning [lewkowycz2022solving, wei2022chain]. At the same time, mathematical research remains a demanding enterprise that requires sustained abstraction, long horizon coherence, and verifiable correctness [thurston2006proof, tao2007good]. In practice, the process is conducted by human experts and often iterative. Human experts pose questions, build candidate structures, test them on examples or with tools, and keep what survives as statements with reusable arguments [lakatos2015proofs, polya1957solve]. Guided by these trends, we take a forward looking view and study how LLMs can advance research level theorem proving by centering human expertise and building interaction workflows that accelerate the research cycle. We emphasize clear prompts and task decomposition, generation of examples and counterexamples and iterative refinement of sketches under human critique. The goal is to show assistance from AI that helps experts frame sharper topics, surface promising conjectures, and develop proofs more quickly while maintaining standards of correctness and clarity.
A growing body of work utilizes machine learning to assist mathematical research and to tackle difficult problems across algebra, geometry, and related areas. In algebra, collaborations between mathematicians and AI reveal useful relations in representation theory and guide the formulation and proof of new results [davies2021advancing]. Recent studies use data driven methods to rediscover classical algebraic inequalities [dong2024machine]. In algebraic combinatorics, curated datasets focus on the conjecturing process and support machine assisted exploration of patterns that lead to precise and testable statements [chau2025machine]. As for geometry, AI systems produce human readable proofs for challenging Euclidean problems and have good performance on Olympiad style benchmarks by combining search, deduction, and verification [trinh2024solving, chervonyi2025gold]. Data driven analyzes of Calabi Yau spaces reveal structural regularities and motivate new conjectures that can be vetted by experts [he2024distinguishing] for algebraic geometry. Beyond individual domains, Ramanujan Machine procedures generate candidate identities for fundamental constants and invite human validation and proof [raayoni2021generating]. Symbolic regression and equation discovery pipelines recover concise laws from data and suggest invariants and lemmas for further study [udrescu2020ai, brunton2016discovering]. These works promote automatic workflows for theorem discovery and proving, in which models propose, rank, and test candidate statements, while human researchers shape definitions, control scope, and turn promising leads into theorems.
A separate line of work targets solutions to competition level mathematics, especially IMO problems. Domain specialized models such as DeepSeekMath-V2 achieve gold medal level performance on IMO tasks via purely natural language proofs with heavy test time compute and dedicated self-verification [shao2025deepseekmathv2]. In parallel, frontier general purpose reasoning models from Google reach comparable scores on IMO 2025 style problems. Building on these backbones, Huang and Yang design a model agnostic verification and refinement pipeline that attains gold medal level at IMO 2025 by systematically generating, checking, and refining candidate solutions [huang2025gemini]. Complementing this natural language line, DeepMind’s AlphaProof system, combines reinforcement learning with formal proof search in Lean and achieves silver medal performance on IMO 2024 problems under fully formal verification [hubert2025olympiad]. These advances suggest that natural language and formal pipelines can both approach top human performance on Olympiad benchmarks.
Beyond theorem proving, many recent efforts use AI to assist scientific research, with most systems targeting application driven areas such as biomedical [huang2025biomni], nature sciences [yang2023ai] and machine learning [li2024mlr]. Deep research systems [huang2025deep, xu2025comprehensive] go further by producing end-to-end reports and maintaining long horizon plans. However, without sustained human supervision, their conclusions often remain limited in strength. A parallel line builds agentic systems for automating parts of the research workflow, ranging from specific agents to AI scientist frameworks and research copilots, showing feasibility in structured settings [lu2024ai, gandhi2025researchcodeagent]. Auto survey methods can conduct a comprehensive survey of the relevant background literature [wang2024autosurvey, liang2025surveyx]. For methodology implementation, recent systems pursue auto code generation for research, including project level context refinement with compiler feedback [bi2024iterative]. In parallel, auto academic writing tools target reference handling, citation integrity, and drafting support [sun2024metawriter, fuad2024llm]. Finally, auto review systems focus on argumentation quality and fairness, but are not sufficient to guarantee mathematical rigor [liu2023reviewergpt, wang2020reviewrobot, idahl2024openreviewer].
<details>
<summary>x1.png Details</summary>
### Visual Description
## Diagram: AI-Assisted Research Workflow
### Overview
The image is a technical flowchart illustrating a three-stage, human-in-the-loop workflow for AI-assisted mathematical or scientific research. The process is divided into three interconnected modules: **AI-assisted Topic Conceptualization**, **AI-assisted Theorem Proving**, and **AI-assisted Theorem Discovery**. The diagram uses color-coded boxes and directional arrows to show the flow of ideas, tasks, and feedback between human researchers and AI systems.
### Components/Axes
The diagram is structured into three main rectangular containers, each with a title.
**1. AI-assisted Topic Conceptualization (Top-Left Container)**
* **Components (in approximate flow order):**
* `Initial Idea` (Green box, top-left)
* `Literature Review` (White box with OpenAI logo, below Initial Idea)
* `Candidate Domain` (Blue box, center)
* `Human Supervision` (Red box, above Candidate Domain)
* `Novelty Inspiration` (White box with OpenAI logo, right of Candidate Domain)
* `Validated Plan` (Blue box, top-right)
* **Flow:** Arrows connect `Initial Idea` -> `Literature Review` -> `Candidate Domain`. `Human Supervision` and `Novelty Inspiration` both feed into `Candidate Domain`. An arrow leads from `Candidate Domain` to `Validated Plan`.
**2. AI-assisted Theorem Proving (Bottom-Left Container)**
* **Components:**
* `Target Theorem` (Green box, center)
* `Direct Proofs` (Blue box, bottom-left)
* `Clear Target Unknown Truth` (Blue box, bottom-right)
* `"Aha" Discovery` (White box, top-right)
* `Human Check` (Red box, right side)
* **Flow:** Arrows flow from `Target Theorem` to both `Direct Proofs` and `Clear Target Unknown Truth`. Both of these boxes have OpenAI logos next to their incoming arrows. An arrow leads from `Clear Target Unknown Truth` to `Human Check`, which then points to `"Aha" Discovery`. Finally, an arrow loops from `"Aha" Discovery` back to `Target Theorem`.
**3. AI-assisted Theorem Discovery (Right Container)**
* **Components:**
* `Human Organization` (Red box, top-left)
* `Target Theorem` (Green box, top-center)
* `Final Output` (White box, top-right)
* `Numerical Experiments with AI` (White box with OpenAI and Python logos, center)
* `Propose Candidate Conclusions` (Blue box, below experiments)
* `Synthesis under Constraints` (Blue box, right of propose conclusions)
* `Theorem Proving with AI` (White box with OpenAI logo, below synthesis)
* `Result Refinement` (White box, bottom-left)
* `Candidate Complete Proof` (Green box, bottom-right)
* **Flow:** The main flow starts from the `Validated Plan` (from the Conceptualization module) pointing to `Human Organization`. From there: `Human Organization` -> `Target Theorem` -> `Final Output`. A secondary, exploratory path branches from `Target Theorem` downwards: `Numerical Experiments with AI` -> `Propose Candidate Conclusions` & `Synthesis under Constraints` -> `Theorem Proving with AI` -> `Result Refinement` -> `Candidate Complete Proof`. An arrow from `Candidate Complete Proof` loops back up to `Human Organization`.
**Inter-Module Connections:**
* An arrow connects `Validated Plan` (Conceptualization) to `Human Organization` (Discovery).
* An arrow connects `Human Organization` (Discovery) to `Target Theorem` (Proving).
### Detailed Analysis
The diagram meticulously maps the roles of human and AI agents:
* **Human Roles (Red Boxes):** `Human Supervision`, `Human Check`, `Human Organization`. These represent oversight, validation, and high-level structuring.
* **AI Roles (White Boxes with Logos):** Tasks like `Literature Review`, `Novelty Inspiration`, `Numerical Experiments`, and `Theorem Proving` are explicitly marked with the OpenAI logo, indicating AI execution. The `Numerical Experiments` box also includes a Python logo, suggesting the use of Python-based computational tools.
* **Process States (Green Boxes):** Represent key milestones or objects of focus: `Initial Idea`, `Target Theorem` (appears in two modules), `Candidate Complete Proof`.
* **Process Outputs/Actions (Blue Boxes):** Represent derived domains, plans, proof types, or synthesis actions: `Candidate Domain`, `Validated Plan`, `Direct Proofs`, `Clear Target Unknown Truth`, `Propose Candidate Conclusions`, `Synthesis under Constraints`.
The workflow is highly iterative, especially in the Theorem Proving module, which features a feedback loop from `"Aha" Discovery` back to the `Target Theorem`. The Theorem Discovery module also shows a refinement loop from `Candidate Complete Proof` back to `Human Organization`.
### Key Observations
1. **Central Role of the "Target Theorem":** This concept is the focal point of both the Proving and Discovery modules, indicating it is the core research object.
2. **Human as Organizer and Validator:** Humans are not shown doing the computational heavy lifting (literature review, proving, experimenting) but are crucial for supervision, checks, and organization.
3. **AI as Executor and Inspirer:** AI is tasked with concrete, often computational, sub-tasks and is also credited with providing "Novelty Inspiration" and facilitating `"Aha" Discovery` moments.
4. **Non-Linear Pathways:** The process is not a simple linear sequence. It includes parallel paths (e.g., `Direct Proofs` vs. `Clear Target Unknown Truth`), branching exploration (`Numerical Experiments`), and multiple feedback loops.
5. **Color-Coded Semantics:** The consistent use of color (Green=State, Blue=Action/Output, Red=Human, White=AI Task) provides an immediate visual grammar for understanding the type of each component.
### Interpretation
This diagram presents a conceptual model for a collaborative, AI-augmented research pipeline, likely in mathematics or formal sciences. It argues that breakthrough discovery (`"Aha" Discovery`, `Candidate Complete Proof`) emerges from a structured interplay where:
* **AI handles scalable, data-intensive, or formal tasks:** Sifting through literature, running numerical experiments, executing proof steps.
* **Humans provide direction, judgment, and synthesis:** Setting goals (`Human Organization`), validating intermediate results (`Human Check`), and supervising the overall domain (`Human Supervision`).
The separation into three modules suggests a phased approach: first defining a promising research area (Conceptualization), then working on specific proof techniques (Proving), and finally integrating everything into a novel discovery (Discovery). The presence of loops underscores that research is an iterative, self-correcting process. The model emphasizes that AI does not replace the human researcher but acts as a powerful tool that extends their capabilities, particularly in exploration and formal verification, while the human retains control over the creative and evaluative aspects.
</details>
Figure 1: Human-AI interactive theorem proving pipeline.
These observations motivate our interactive workflow, which inserts human oversight at intermediate stages and utilizes machine verifiable evidence to substantiate the conclusions. We present a practical workflow that couples human judgment with AI generation to prove, transfer, and discover mathematical results. The proposed workflow serves as a template for leveraging LLM assistance in mathematical research, helping to turn interaction with language models into verifiable definitions, lemmas, and proofs, thereby improving research efficiency while preserving rigor.
Our AI-human workflow centers on three stages: conceptualizing research topics, theorem proving for fixed targets, and theorem discovery when the conclusion is not yet determined. As an illustrative case study, we apply this workflow to our recent research that combines Grover’s algorithm from quantum computing with Riemannian optimization, and we explicitly present the prompts that instantiate the workflow in this setting. The human-AI interactive proving pipeline is shown in Figure 1. Our main contributions are listed as follows.
1. Topic conceptualization with AI. We design an AI-assisted routine for early stage problem formulation. Starting from preliminary human ideas about research topics, the LLM proposes candidate objects, assumptions, and questions with brief notes on novelty and feasibility. Researchers, guided by both their own expertise and the model’s feedback, test these candidates on minimal examples. The survivors are turned into precise statements, and an initial paper outline.
1. Goal-guided proving. For clearly specified proof targets, researchers communicate their preliminary proof ideas and directions to the model via carefully designed prompts. The LLM suggests reductions, proof sketches, and possible counterexamples along these directions. Under human checks, we extract full clear theorem statements, theorem proofs, and auxiliary lemmas and consolidate them into rigorous, human readable theorems.
1. Open-ended theorem discovery. When target conclusions are not fixed in advance, we use the LLM to propose candidate statements with lightweight evidence, such as numerical experiments and mathematical reasoning. Human experts filter and refine these candidates into theorem templates and reusable proof schemas for related problems. When suitable constructions are unknown, a property constrained generator to tester loop searches for simple candidates that satisfy the desired conditions and admit clean proofs.
1. Pipeline validated by case study. We apply the end-to-end workflow to a nontrivial problem in quantum inspired Riemannian optimization. This case study yields machine checkable definitions, lemmas, and proofs, together with reusable prompts. It highlights that the pipeline above supports rigorous and reusable mathematical outcomes.
Our examples are drawn from our present work on quantum computing and Riemannian optimization. We organize the paper according to different modes of AI-assisted mathematical practice. Hence, some example theorems do not follow the natural order of the underlying mathematics. For a detailed explanation of quantum algorithms and development of the mathematical results themselves, we refer readers to the companion mathematics paper [lai2025grover].
The remainder of the paper is organized as follows. We briefly review elements of mathematical research in Section 2. Topic conceptualization with AI support is discussed in Section 3. We present AI-assisted theorem proving for fixed targets and document the associated machine checkable artifacts in Section 4. AI-assisted theorem discovery, including proposal, numerical test, and proof, together with transfer to similar settings, is explored in Section 5. We clarify the respective roles of human experts and AI systems in Section 6. Finally, the paper is concluded with Section 7.
## 2 Preliminaries: elements and mechanics of mathematical research
In practice, mathematicians often view research as passing through five connected phases: topic conceptualization, conjecturing, validation, proof development, and writing. Each phase has its own goals, typical outputs, and methods. We briefly review the role of each phase and indicate how new advances can be categorized.
Topic conceptualization. The first task is topic conceptualization. Good topics balance depth, tractability, and potential for broader impact [tao2007good]. The conceptualization process specifies the scope, modeling decisions, and targets for correctness and clarity. Researchers begin by specifying three components: the object, the assumptions, and the claim. This choice determines the scope, modeling decisions, and targets for correctness and clarity. The object identifies the mathematical structure under study, such as a class of functions, graphs, or manifolds. The assumptions collect the standing hypotheses, for example, the regularity conditions, dimensional regimes, or model constraints. The claim formulates the intended conclusion in precise terms, including but not limited to, an error bound, a convergence rate, or a stability guarantee. In practice, this stage consists of surveying prior work, including both results and methods and also known limitations and choosing the working setting, such as toy models for quick feedback and general frameworks for the final version of the theorem.
Conjecturing. Once the main topic is relatively fixed, human experts study the related literature and learn the relevant concepts. They ask what existing results already cover, where the assumptions are too strong, which regimes or examples are missing, and how known methods might be modified. They also look for ideas from neighboring areas that could be imported into the current setting. From this perspective, conjectures often come from extending an existing theorem to a new regime, weakening assumptions while trying to keep the same type of conclusion, or combining mechanisms that have been used separately [polya1957solve].
Innovation types in conjecturing. We now distinguish several common innovation routes at the conjecturing stage and, for each route, explain how conjectures arise and provide representative examples.
1. Fix bug: make existing methods verifiable or stable under realistic assumptions. Typical examples include robustness to nonsmooth terms and convergence proofs under perturbations, such as proximal steps and operator splitting for nonsmooth objectives.
1. Weaken assumptions: replace strong regularity or noise free models with weaker, more realistic conditions while preserving guarantees. For instance, establish convergence or rates under weak convexity, stochastic perturbations, or inexact oracles.
1. Combination fusion: merge complementary mechanisms to improve performance. For example, combine acceleration with variance reduction to obtain provable improvements over either component alone.
1. Cross domain lifts: recast the problem in a different domain, then use the new viewpoint to propose related questions. Typical cases include passing from discrete to continuous models, from Euclidean setting to manifold ones.
1. Unifying viewpoints: place several related methods in a single framework to explain their similarities and differences. For example, viewing first-order methods through a parameterized ODE can unify different acceleration schemes, which can then be analyzed within a Lyapunov framework.
1. Boundary and negative results: identify the limits of what is achievable under a given set of assumptions. Common goals include proving lower bounds, and giving sharp counterexamples that show the corner cases under certain settings.
Validation. Before investing effort in proofs, human experts test candidate conjectures in straightforward ways. They may compare them with known results and basic intuition, and examine their behavior on both simple examples and complicated cases. Feedback from these checks is then used to revise the statement, adjust the assumptions, and decide which directions are worth pursuing.
In practice, human experts combine careful manual calculations with small numerical experiments. Examples that cover boundary cases and important special situations may also be explored. It is often helpful to keep a record of each conjecture, which contains the tests it has passed or failed, and the exact assumptions under which it seems to hold. The goal is to discard weak ideas early, focus on a clear and robust formulation, and formulate early proof ideas.
Proof development. When the statement is stable, human experts try to figure out a proof plan. Several basic proof approaches are useful in many parts of mathematics. First, human experts use plain step-by-step reasoning: write down the definitions, expand them carefully, and follow the logical implications until the claim is reached. Second, they adapt standard methods from previous work or neighboring areas. Typical transfers take techniques developed in other domains and apply them in the current setting. Decomposing the current problem into simpler subproblems can reveal structures that also appear in related work. Third, they look for innovative structure or ideas that can guide the proof. This may involve defining a quantity with carefully chosen properties. At this stage, new proof techniques may also be developed to handle more sophisticated problems.
Writing. In the final stage, human experts organize the statements, standardize the notation, and polish the proofs. Results are arranged into a coherent hierarchy of definitions, lemmas, and theorems, and symbols are introduced explicitly and used consistently. Proofs are streamlined where possible, with the main idea stated before technical details. The final writeup gathers the work from conjecturing, testing, and proving into a presentation that is clear, checkable, and easy to build on.
## 3 Conceptualizing research topics with AI
### 3.1 Early stage exploration: domain sketch and candidate questions
Early exploration moves from broad themes to specific mathematical targets. We begin by using AI to map the structure of the domain. This includes identifying the main objects under study, including core algorithms, key operators, and typical function classes. We also identify the assumptions that usually govern behavior, namely properties of functions, or curvature conditions, and the standard objectives like rates, bounds, stability, and existence results. By aligning terminology across different areas and highlighting analogies, AI helps construct a coherent picture of the field and locate promising candidate problems. A typical example is transferring properties established in Euclidean space to their counterparts on manifolds.
With this guidance, we encourage AI to propose concrete research questions along principled axes of variation. These include weakening or strengthening hypotheses, transferring known results to new regimes, seeking converses, or isolating thresholds. Each proposal is paired with three elements: a precise claim sketch with minimal hypotheses, the nearest classical results with their gaps, and a plausible method class. To avoid vacuous or ill-posed targets, we run quick feasibility checks. AI is asked to generate instances, and to perform scaling and invariance sanity checks. These steps reveal hidden necessary conditions or point to underlying patterns. Proposals that survive are ranked by novelty and tractability, with preference given to those promising a unifying principle rather than an isolated trick. The output of this stage is a compact domain sketch and a curated set of viable questions ready to be sharpened.
Example. Building on the perspective of [suzuki2025grover], which analyzes classical quantum algorithms through imaginary time evolution, we begin with an initial idea of combining quantum algorithms with manifold optimization. We phrase this idea as a concrete prompt, given in Appendix A.1. The model returns a concise conclusion that lists candidate directions and prerequisite concepts on both sides, such as algorithmic primitives, target objectives, and possible correspondences between them, together with preliminary feasibility explanations. We treat this response as a rough map. It guides our literature reading and internal discussion, and helps us prune ideas that are ill-posed or unlikely to admit clean analysis. After several rounds of interaction with language models, our main idea converges on two anchors: Grover’s search and Riemannian gradient methods.
### 3.2 Concrete idea phase: sharpened claims and validation plan
Once the topic and basic directions are in place, the next step is to turn promising ideas into precise and checkable statements. Human experts usually begin by fixing notation and writing down assumptions as explicit structural properties of the objects under study. This forces clarity on what is concerned and what is merely background. At the same time, AI can be asked to suggest propose decompose ways, and point out where known techniques are likely to apply. The goal is to expose the core difficulty of the problem and to identify a small number of central conjectures and theorems that capture it.
With candidate statements in hand, we organize the reasoning into a hierarchy of proof tasks. This hierarchy includes main theorems, key reductions, comparison steps, and delicate lemmas where constants, parameter ranges, or limiting regimes matter most. For each task, AI can list possible proof strategies and propose simple numerical tests. These tests help diagnose which parts are routine and which are genuine bottlenecks. On this basis, we design a validation plan. It separates the claims we aim to prove completely from conjectures that are strongly suggested by the structure but still require further ideas.
Finally, we start to shape the final paper around this structure. The definitions and notations are organized in the way which is most convenient for the arguments that follow. Intermediate claims are grouped into coherent subsections. Prospective figures and tables are tied directly to specific arguments or comparisons. By the end of this phase, a vague direction has been converted into a disciplined roadmap containing relatively clear claims with explicit scope, identified proof avenues, and a theoretical validation plan.
Example. Continuing the example from the previous subsection, suppose we have fixed the topic at the intersection of Riemannian optimization and Grover’s algorithm. The guiding theme is to interpret Grover’s procedure from a manifold optimization viewpoint. With this topic in place, we ask the model for a theoretical framing. It produces a structured note that lists the relevant objects on both sides. These include the manifold of quantum states and the standard Riemannian gradient updates. It also recalls the basic properties of Grover iterations, namely their symmetry and complexity guarantees. It suggests natural submanifolds to restrict to, and propose possible connections between gradient like dynamics and Grover’s iterations appear to align. The prompts used in this example are given in Appendix A.2.
We then further request a more explicit manifold optimization treatment. The model proposes viewing the state evolution as gradient style updates on a suitable manifold of quantum states and outlines checks that distinguish genuine geometric structure from artifacts of a particular parameterization. It suggests candidate statements that aim to recover the classical complexity of Grover’s algorithm within this manifold gradient framework. On the human side, we refine these suggestions into precise assumptions and theorem statements. We decide which claims must be proved rigorously in the first version of the paper and which remain uncertain.
## 4 AI-assisted theorem proving
Contemporary AI systems already possess substantial theorem proving capabilities. When a target statement falls within a familiar formal framework, they can often produce correct, easy but nontrivial arguments with limited guidance. In this section, we therefore concentrate on AI-assisted theorem proving under a fixed objective and structure the discussion around three usage scenarios. In all cases, human experts specify the goal, choose search strategies, examine intermediate proposals, and shape the final argument. AI is used to enlarge the search space and shorten the iteration cycle, while human experts maintain academic standards of clarity, appropriate scope, and sufficient evidence.
Throughout, human experts and AI work under a clear division of responsibilities. Key mathematical ideas and decisions remain under human authorship, while the model mainly supplies candidate lemmas, alternative approaches, and computational support. Human experts then refine promising suggestions into proofs that are clear, robust, and easy to reuse.
### 4.1 Direct proofs when the statements are trusted
The easiest case begins with a statement human experts believe to be correct and a concrete proof plan. The simplest way to use an AI prover in this setting is to ask it directly for a proof of the target statement, then query the model for standard reductions and a stepwise derivation. The model, however, remains error prone. It may skip justifications, misapply lemmas, or mishandle quantifiers and constants. To mitigate this, human experts use targeted prompts. For example, they explicitly state assumptions and variable domains, require line-by-line reasoning, and ask for citations, adversarial checks, and quick numerical spot tests. Nevertheless, human experts must still verify every claim produced by the AI, checking edge cases and reproducing key calculations.
This setup typically arises when human experts already have a deep understanding of what needs to be proved and only some local details remain to be filled in. After reviewing the draft, they identify gaps, remove redundancy, and reorganize the argument so that the key steps are transparent. In this way, the AI accelerates routine proof work and broadens the search space, while human experts provide validation, judgment, and final integration into a clear and fully rigorous proof.
Example. We illustrate our human-AI workflow with the following claim, which ties stationarity to global optimality on the unitary manifold. Let $H=H^†=H^2$ be an orthogonal projector on a Hilbert space. $U∈U(N)$ denotes the quantum circuit we want to design. Our cost function is $f(U)=(HUψ_0U^†)$ , where $≤ft|ψ_0\right⟩$ is the initial state. Intuitively, the skew-Hermitian component of the Riemannian gradient $\widetilde{}f(U)=[H,ψ_U]$ shows that stationarity is equivalent to the output state $ψ_U$ commuting with $H$ . In this case $ψ_U$ is an eigenstate of $H$ , and since the spectrum of $H$ is $\{0,1\}$ , the expectation $f(U)=(Hψ_U)$ is forced to take an extremal value $0$ or $1$ . This intuition gives the following theorem on global optimality.
**Theorem 4.1 (Global optimality)**
*Let $f(U)=(HUψ_0U^†)$ on the unitary group $U(N)$ , and write $ψ_U:=Uψ_0U^†$ for the output state of the circuit $U$ . The skew-Hermitian part of the Riemannian gradient of $f$ on $U(N)$ is
$$
\widetilde{}f(U)=[H,ψ_U].
$$
Moreover, $\widetilde{}f(U)=0$ if and only if $U$ is a global optimizer of $f$ over $U(N)$ ; in that case $f(U)∈\{0,1\}$ , corresponding respectively to the global minimum $0$ and global maximum $1$ .*
To turn the above intuition into a rigorous argument within our human-AI workflow, we do not simply ask the model to prove the theorem. Instead, we issue a structured prompt with explicit instructions tailored to this setting. The model is asked to restate all assumptions, notation, and variable domains, and to produce a numbered, step-by-step LaTeX proof in which every nontrivial inference is justified. It is further required to rely only on standard, named results rather than informal or unsupported statements. These requirements are chosen by the human experts based on their understanding of the current problem, and can be adapted on a case-by-case basis. When experts have a clear proof strategy in mind, they can encode it directly into the prompt. Under these constraints, the model returns a detailed derivation, which the human experts then verify line by line, reproduce key calculations, examine boundary cases, and streamline into the final proof. The prompts used in this example are listed in Appendix A.3.
### 4.2 Clear target, uncertain truth
In many cases, human experts do not know in advance whether a proposed theorem is true as stated, hence situations of uncertainty are common. Faced with this uncertainty, we adopt a systematic prove or disprove protocol. We delegate to AI along two coordinated branches: one explores plausible avenues toward a proof, and the other actively searches for failure. Both outcomes are informative: a successful argument consolidates the scope of the claim, while a counterexample clarifies its limits and may suggest a revised, more accurate formulation.
On the proof side, the AI proposes feasible directions, candidate lemmas, decomposition strategies, and intermediate claims, around which the human expert can organize a coherent argument. On the disproof side, the AI generates tentative constructions, stress tests, and diagnostic patterns that focus the search for counterexamples on promising regions of the space. By jointly assessing the evidence produced by both branches, the human expert avoids one-sided or wishful reasoning and moves more efficiently from an initial conjecture to a stable, well justified conclusion.
Example. We illustrate the prove or disprove workflow on a basic structural question from matrix theory related to the retraction on the Riemannian manifold. Consider the following proposition about commutators of Hermitian matrices and the Lie algebra $\mathfrak{su}(n)$ . It is straightforward to check that any commutator $[A,B]$ with $A^†=A$ and $B^†=B$ is skew-Hermitian. However, it is much less obvious whether every skew-Hermitian matrix with zero trace arises in this way. This makes the statement a natural candidate for a two branch search: the proof branch looks for a constructive representation of arbitrary elements of $\mathfrak{su}(n)$ as commutators, while the disproof branch asks the model to propose potential counterexamples or structural obstructions.
**Proposition 4.2**
*The set of commutators of Hermitian matrices
$$
C=\{[A,B]:A^†=A,B^†=B\}
$$
equals $\{X∈ M_n(ℂ):X^†=-X,trX=0\}=\mathfrak{su}(n).$*
To analyze this proposition with AI assistance, we do not simply ask whether it is true or false. Instead, we issue a structured prove or disprove prompt that forces the model to work along two explicit branches. Concrete prompts can be found in Appendix A.4. First, the model must restate all assumptions, notation, and ambient spaces, and then develop a proof branch that attempts to represent arbitrary elements of $\mathfrak{su}(n)$ as commutators $[A,B]$ via concrete constructions, basis expansions, or dimension arguments. In parallel, a disproof branch searches for obstructions or counterexamples by analyzing the subspace spanned by such commutators, checking invariants, and probing whether some traceless skew-Hermitian matrices might lie outside $C$ . Within each branch, the model is required to give line-by-line reasoning with explicit justification of every nontrivial step and to rely only on standard, named results. Finally, it must return a clear verdict, proof or counterexample, together with a short list of adversarial checks a human reader could perform. This protocol yields a structured record of both successful and failed lines of attack, which human experts can then inspect, test, and refine into a stable conclusion.
### 4.3 Rich proofs and the “Aha” moment
When human experts ask a model to prove a theorem, the model typically generates a “rich trace”, which contains not merely a linear line of argument, but a spectrum of unranked byproducts, including auxiliary lemmas, equivalent formulations, invariants, and candidate inequalities. These outputs are treated as products to be mined rather than noise. Human experts deliberately scan these artifacts, assessing their utility for tightening bounds, exposing mechanisms, or simplifying decisive steps. Promising items are subjected to targeted validation, such as scope checks, numerical probes, or lightweight strict verification. We name these results as “aha” observations. Validated insights are subsequently organized to named results, prompting a restructuring of the surrounding argument to reflect their significance.
Crucially, many of these “aha” observations are results the which experts did not initially set out to prove. While the model’s breadth surfaces these possibilities, it lacks the capacity to assign importance. This role belongs to the human expert, who remains critically skeptical until sufficient evidence has accumulated. By applying explicit acceptance criteria, generality, simplicity, and interoperability with subsequent sections, the expert determines what enters the formal record. This curation process elevates a merely correct derivation into an insightful analysis, converting incidental outputs into durable, reusable building blocks.
Example. In proving the synthesis statement in Section 5.1, the model generated a comprehensive proof accompanied by a note on secondary conclusions regarding the update properties. Among these byproducts, one observation proved pivotal. It transformed the manifold viewpoint of the Grover’s algorithm into an implementable algorithm on a two dimensional subspace. Specifically, after a one shot preprocessing step on classical hardware to fix coordinates, the subsequent evolution admits closed form scalar recurrences. Although this property was not the primary focus during the initial research phase, practical implementation constraints on quantum hardware necessitated a modification of the iterative update. Consequently, we formulate the following theorem regarding the initially determinable parameters:
**Theorem 4.3**
*Let the iterates $V_k$ be finite products of terms $e^iθ H$ and $e^iθψ_0$ . Define $U_k+1:=V_kU_k$ (with $U_0=I$ ) and $ψ_k:=U_kψ_0U_k^†$ . Then there exists an explicit, classically computable process
$$
F:(x_k,y_k,q_k;t_k)↦(x_k+1,y_k+1,q_k+1) \tag{1}
$$
which ensures all iterates remain within $U(N)$ , preserves the Grover plane $S$ , and admits closed-form scalar recursions.*
The concrete form of the function $F$ is omitted here for brevity. The reply from the model is given in Appendix A.5. However, we need to highlight the distinction between generation and presentation. While the language model successfully identified the recursive structure and provided the raw derivation, the transition from raw output to the structured clarity of Theorem 4.3 required significant human intervention. We invest substantial effort in synthesizing the model’s dispersed findings into a coherent narrative, standardizing notation, and rigorizing the proof steps. This final curation, organizing the logical flow and formatting the results to meet academic standards, remains an essential human contribution to the collaborative workflow.
## 5 AI-assisted theorem discovery
Theorem discovery is generally harder than theorem proving and, in practice, it is also the more common task. In many projects, human experts do not yet know what the final statement should be. Traditionally, they make progress by talking with colleagues, reading the literature, and trying constructions based on their experience until a promising conjecture appears. AI can strengthen this stage. It can suggest candidate statements and variants, highlight patterns and invariants, propose convenient normal forms, and quickly test ideas by searching for counterexamples or checking boundary cases. Human experts still control the goals and the evidence. They fix the assumptions, judge what the model returns, and decide what enters the written report. Along the way, the AI often produces useful byproducts, including auxiliary lemmas, cleaner formulations, or sharper bounds, that it does not flag as important. Human experts also look for these byproducts, test how broadly they apply, and promote the helpful ones to named results. In short, AI broadens the search and provides systematic tests, while human experts provide direction and judgment, turning vague ideas into clear, testable theorems.
### 5.1 From assumptions to conclusions: AI-guided discovery
#### 5.1.1 AI-guided proposal of candidate conclusions
Human experts begin with a fixed setting, assumptions, class of objects, and admissible ambient space, but the precise conclusion is still open. In this situation, they prompt the AI to propose candidate consequences of the assumptions, including but not limited to plausible properties, equivalent formulations, reductions, and statements about extreme or boundary regimes. To encourage diversity, they ask for multiple variants with short explanations and, when appropriate, suggested counterexamples. Since the model can make mistakes or overstate what is true, each proposal must provide light supporting evidence, such as tests on simple and edge cases, quick numerical checks, and references to comparable results. The returned suggestions are then filtered by explicit criteria, and for each candidate we record whether it passes or fails and why.
Human experts then analyze and select. They test validity more thoroughly, evaluate whether a candidate improves interpretability or tightens bounds, and keep the statements that clarify mechanisms or simplify later analysis. From these surviving candidates, they distill a clean, testable theorem shape, including assumptions and theorems. AI is used to expand it into a coherent, step-by-step argument. Nonsurviving claims are recorded as negative evidence and inform the next round of prompts.
Example. We illustrate the discovery workflow on the Grover-type iteration. Our goal is to explore the properties of a simple projector driven dynamics underlying the Grover search operator. We utilize AI to see what structural statements it can help surface. At a high level, we study the evolution of pure states under repeated updates driven by a fixed projector and ask for invariants, norm identities, and scalar recursions that describe this process.
Firstly, we consider the general exponential update. Concretely, fix a projector $H=H^†=H^2$ and consider pure states $ψ_k=|ψ_k⟩⟨ψ_k|$ . Define $q_k=⟨ψ_k|H|ψ_k⟩∈[0,1]$ and $γ_k=√{q_k(1-q_k)}$ . We study the following exact exponential step
$$
\displaystyle V_k=\exp\bigl(t_k[H,ψ_k]\bigr), U_k+1=V_kU_k, ψ_k+1=U_k+1ψ_0U_k+1^†. \tag{2}
$$
We are not confident about which properties of this update are crucial, and hence do not fix the final theorem in advance. Instead, we ask the model to surface plausible consequences of the dynamics, such as invariance properties, norm identities, scalar recursions, or one step convergence conditions. These suggestions are then checked for internal consistency and usefulness for the later analysis, retaining only statements that clarify the mechanism or simplify the argument. This leads to the following formal statement.
**Proposition 5.1 (Exact step via exponential (“Exp update”))**
*Let $H=H^†=H^2$ and define $q_k=⟨ψ_k|H|ψ_k⟩$ and $γ_k=√{q_k(1-q_k)}$ . The following properties hold for (2):
- the gradient norm identity $\|[H,ψ_k]\|_F=√{2} γ_k$ ;
- the state $|ψ_k⟩$ remains in the real two dimensional Grover plane spanned by $\{|ψ_0⟩, H|ψ_0⟩\}$ ;
- the quantity $q_k+1$ has a closed form recursion obtained by viewing the update as a rotation on this plane;
- there exists a positive one shot step $t_0^*=\frac{\arccos√{q_0}}{γ_0},$ such that $e^t_0^{*[H,ψ_0]}|ψ_0⟩=|ψ^*⟩$ and $\max L(U)=1$ are attained in a single update.*
To obtain Proposition 5.1, we use a prompt that fixes the dynamical setting and leaves the conclusions open. The prompt can be found in Appendix A.6. The prompt first asks the model to restate all assumptions and domains, including projector properties of $H$ , rank-one nature of $ψ_k$ , ranges of $q_k$ and $γ_k$ , and the unitary evolution of $U_k$ and $ψ_k$ . We then instruct the model to generate a list of concise candidate statements, each tagged with a simple type label (for example, invariant, norm identity, scalar recursion, or convergence guarantee) and accompanied by a brief informal explanation of why the statement might be useful.
These prompts are guided by human intuition about Grover-type dynamics. We explicitly mention structures which are expected to matter, such as behavior in the Grover plane, gradient norms, scalar recursions, and one step convergence, so that the search is not completely unguided. At the same time, the prompt leaves room for the model to propose additional kinds of structure when it detects patterns that fit the assumptions. Finally, the prompt requests that the model select a small, coherent subset of surviving candidates and package them into a single proposition with numbered parts, together with short, step-by-step derivations that cite only standard facts. Proposition 5.1 is the result of this process, after human experts review the candidates, verify the calculations, and make minor edits for clarity and integration with other results of the paper.
#### 5.1.2 Human abstraction and cross-setting transfer
After one iteration of the discovery loop, human experts extract patterns: recurring steps, reusable lemmas, and canonical normalizations. These ingredients are summarized into a portable proof schema: what to assume, what to try first, which invariants to test, and which failure modes to monitor. The schema is then transferred to nearby settings—such as related function spaces, modified boundary conditions, or perturbed parameter ranges. Human experts prompt the AI to adapt earlier lemmas, inequalities, and constants to generate variants on similar cases.
In summary, the working loop for exploring conclusions of fixed assumptions is as
$propose → check → distill → prove → transfer,$
with the AI broadening the search and providing rapid, evidence backed suggestions, and human experts supplying direction, skepticism, selection, and cross setting reuse. The outcome is not only a theorem for the initial setting, but also a transferable pattern that speeds up discovery in related regimes.
Example. We treat the projector-driven instance in Section 5.1.1 as an exemplar for transfer. From the prior round, the AI returned several properties that survived lightweight checks and human validation (an invariant working subspace, a stable two direction gradient plane, a scalar progress statistic with a simple recursion, and a local surrogate update that preserves structure within controlled error). Rather than focus on derivations here, we abstract these survivors into a portable schema and use them to organize proofs in similar settings. Concretely, we keep the invariance and closure statements as the core of the schema, and ask the model to instantiate them under new assumptions while providing the same evidence pack (toy and edge case numerics, minimal counterexamples, and references to comparable mechanisms). The central lemma we retain is as follows.
**Theorem 5.2 (Invariant22D subspace lemma)**
*Let $H$ be a projector, $ψ_0$ a rank-one projector, and define iterates as follows. Let $V_k$ be any finite product of factors of the form $e^iθ H$ and $e^iθψ_0$ , set $U_k+1:=V_kU_k$ with $U_0=I$ , and let $ψ_k:=U_kψ_0U_k^†$ . Define
$$
q_k:=⟨ψ_k|H|ψ_k⟩∈[0,1], τ_k:=√{q_k(1-q_k)}∈\Bigl[0,\tfrac{1}{2}\Bigr],
$$
and $X_0:=[H,ψ_0],Y_0:=i[H,X_0].$ Then the following properties hold
- The state $|ψ_k⟩$ remains in the fixed two dimensional subspace $S:=_ℂ\{|ψ_0⟩, H|ψ_0⟩\}$ (the Grover plane) for all $k$ .
- Each gradient $f(U_k)=[H,ψ_k]$ lies in $_ℝ\{X_0,Y_0\}$ for all $k$ .*
The prompt is given in Appendix A.7. For cross-setting transfer, we treat Proposition 5.1 as a base lemma. In a new but related setting, we prompt the AI to (i) identify a candidate invariant working subspace and the corresponding two direction gradient plane; (ii) specify a scalar progress statistic and its recursion; and (iii) propose a structured local surrogate for the exact update together with its claimed accuracy. We retain control over assumptions and acceptance criteria, require the same lightweight evidence, and record any failures as negative evidence to refine the stepsize window or repair premises. In this way, the example yields a reusable pattern: instantiate the invariant plane and gradient closure, reduce the analysis to the induced scalar recursion, and let the model fill in setting-specific proofs under our checkpoints, producing concise theorems for each new regime while preserving the core statements above. The proof of this theorem is also worked with LLM.
### 5.2 Property constrained synthesis
Human experts aim to construct an object that satisfies a fixed list of properties, even though a closed-form expression or parameterization is not yet known. They use the AI system as a combined generator and tester to speed up this search. First, human experts specify the required properties, the admissible ambient space, and representative edge cases, and ask the AI to propose concrete, parameterized candidates with short explanations. Second, they ask the AI to perform lightweight checks on its own proposals: targeted numerical experiments, edge case tests, and small stress tests that either support the desired properties or produce counterexamples. The AI returns both the most promising candidates and the corresponding experimental traces.
Human experts then apply acceptance criteria such as correctness on the stated tests, simplicity of form, and efficiency in resources or parameter count. They also push the AI to refine candidates toward leaner parameterizations that still satisfy all required properties. This propose-test-refine loop continues until one or two candidates consistently pass screening and reveal a stable underlying mechanism. At that point, human experts request a proof plan for the surviving form and complete the argument. If failures persist, they tighten assumptions or narrow the scope and restart the loop.
This workflow reduces human effort while broadening the search space. The AI can explore more variants than human experts would typically try by hand and can adapt patterns from related problems. To reduce the risk of fabricated or unsupported claims, every AI proposal is tied to verifiable evidence, numerical trials, stress tests, or simple certificates, so that only candidates supported by reproducible checks progress to formal proof.
Example. We treat the design of the retraction in our update rule as a property-constrained search guided by the AI. The target properties are fixed in advance:
- $γ(t;x,y)$ is a product of factors of the form $e^iθ H$ or $e^iθψ_0$ ;
- $γ(0;x,y)=I$ ;
- for any target tangent $Z∈W:=span_ℝ\{X_0,Y_0\}$ with $Z=xX_0+yY_0$ (where $X_0:=[H,ψ_0]$ , $Y_0:=i[H,X_0]$ ), the initial velocity satisfies $γ^\prime(0;x,y)=Z$ .
We ask the model to propose short product forms and parameter couplings that might satisfy (P1)–(P3). In addition, we require it to validate each proposal numerically on a seed set $S⊂ℝ^2$ : it must check (i) (P1) syntactically, (ii) (P2) exactly, and (iii) (P3) by a finite-difference test
$$
≤ft\|\frac{γ(h;x,y)-I}{h}-(xX_0+yY_0)\right\|_F≤ε \tag{3}
$$
for a small step size $h$ , and report pass/fail results for each $(x,y)∈S$ . Only the shortest product that passes on $S$ (and on simple edge cases such as $x=0$ or $y=0$ ) is selected and then sent to detailed proof.
**Theorem 5.3**
*Define the following length-5 product retraction
$$
R^(5)_U(η):=e^ia_1He^ib_1ψ_0e^i≤ft(a_2-a_1\right)He^ib_2ψ_0e^-ia_2H U, \tag{5}
$$
with real parameters $(a_1,a_2,b_1,b_2)$ are defined as
$$
\displaystyle\begin{aligned} A&:=(y,x), R:=√{x^2+y^2}, a_1=A+\frac{π}{2},\\
a_2&=A-\frac{π}{2}, b_1=-\frac{R}{2}, b_2=\frac{R}{2}.\end{aligned} \tag{5}
$$
Then, The corresponding $γ(t)$ satisfies (P1) to (P3)
$$
γ(t;x,y)=R^(5)_U(tη)={e^ia_1He^itb_1ψ_0e^i≤ft(a_2-a_1\right)He^itb_2ψ_0e^-ia_2H} U, t≥ 0. \tag{5}
$$*
For theorems that require an explicit, workable construction, we obtain the retraction in Theorem 1 by turning the design task into a property-constrained synthesis problem encoded in the prompt above. Instead of guessing product forms by hand, we tell the model exactly which ingredients are allowed (factors of the form $e^iθ H$ and $e^iθψ_0$ ), what the target space is (the two dimensional subspace $W=span_ℝ\{X_0,Y_0\}$ ), and which properties must hold (P1) to (P3). The prompt first asks the model to restate these constraints in its own words and then to propose a small list of candidate products of different lengths, together with a short explanation of why each ordering and parameter coupling might satisfy the target properties. The prompt is given in Appendix A.8.
The prompt then forces each candidate through a concrete testing stage. For a fixed seed set $S⊂ℝ^2$ , a step size $h$ , and a tolerance $ε$ , the model must write executable Python code that implements $γ(t;x,y)$ , checks (P1) syntactically and (P2) exactly, and verifies (P3) numerically via the finite difference condition (3) for $(x,y)∈S$ , including edge cases. The code and its pass or fail reports come back as part of the model’s reply, and human experts can rerun these tests independently.
Among all candidates that pass the numerical checks, we select the shortest product that appears robust and ask the model to restate it in a theorem ready form together with a brief proof plan. Human experts then inspect the proposed parameter constraints, replace the informal proof sketch with a full symbolic derivation, and integrate the result into the main argument. In this way, the AI handles the combinatorial search over product structures and preliminary validation, while human experts control the specification of properties, the choice of tests, and the final rigorous proof, leading to the length-5 retraction stated above.
### 5.3 Human-AI collaborative proof for conjectures
Proving complex conjectures is sensitive to the choice of domain, geometric setting, and technical assumptions. In our workflow, the collaboration between human experts and an AI assistant is organized into three stages that start from an informal conjecture and end with a precise theorem and proof.
In the first stage, human experts interact with the AI to fix the exact statement: they clarify the objects, the ambient space, and the assumptions until the claim is unambiguous. In the second stage, they confirm a feasible proof route by consulting the literature and asking the AI to surface related results and standard techniques, and they organize these ingredients into a coherent proof plan. In the third stage, they calibrate the constants and parameters that appear along this route: the AI proposes local bounds, human experts check them against theorem level requirements, and numerical stress tests validate or refute the underlying inequalities. Finally, human experts seek for higher level results or stronger theorems based on what they have already discovered.
Each stage produces concrete outputs. The first stage produces a checklist of objects, spaces, and assumptions written in normalized notation. The second stage produces a proof skeleton that records the main strategy, intermediate lemmas, and their logical dependencies. The third stage produces tables of constants and logs of numerical tests. The last stage generates final updated complete theorems. These artifacts make the human-AI collaboration reproducible and allow other researchers to restart or adapt the process from any stage.
#### 5.3.1 Scoping with AI: objects, ambient spaces, and assumptions
Human experts usually start from a rough target theorem in which several concepts and assumptions are still vague. In the first stage, they conduct short rounds of interaction with the AI whose purpose is to make these ingredients precise. In each round, the AI is asked to define the relevant objects, fix the ambient space (for instance, a Euclidean space, a Riemannian manifold, or a function space), specify the metric and the associated notion of gradient, and list all assumptions in a consistent format. The round ends with an explicit checklist of domains of variables, regularity or convexity requirements, boundary cases, and notation. Human experts review this checklist, resolve inconsistencies, and repeat the cycle until the statement is internally consistent and the AI can restate it in the agreed notation without contradictions or hidden assumptions.
Example. We start from an informal conjecture that gradient descent with the 5-factor retraction on the unitary group should reach a point with gradient norm at most $ε$ in $O(√{N}/ε^2)$ iterations, for the target function $f(U) = \bigl\{H Uψ_0U^†\bigr\},$ defined on the unitary group $U(N)$ equipped with the canonical Riemannian metric induced by the Frobenius inner product. At this point, the geometric setting is still unfixed. We can understand from the perspective of both the Euclidean setting and the manifold setting. It is not yet clear which notion of Lipschitz continuity will control the iteration complexity.
After several scoping rounds with the AI, we fix the following setting. Gradients and norms are understood in this Riemannian sense. Following standard practice in numerical optimization, we expect that some Lipschitz constant of the (Riemannian) gradient will enter the complexity analysis. The output of the first stage is therefore a precise target theorem. It specifies the domain $U∈U(N)$ with its canonical metric, the objective $f$ , the assumption that the Riemannian gradient of $f$ is Lipschitz with constant $L_g$ , and the goal of proving an iteration bound of order $O(√{N}/ε^2)$ for the 5-factor retraction gradient method.
In this phase, the AI is not used to design the proof, but to expand the informal conjecture into a well-posed statement about $(U(N),canonical metric)$ , the function $f$ , and the constant $L_g$ that later appears in the complexity bound. The prompt used for this example is given in Appendix A.9.
#### 5.3.2 Route confirmation: literature guided plan
Once the statement is fixed, the second stage searches for a feasible proof route. Human experts read the relevant literature and ask the AI to retrieve related results, known inequalities, and standard proof patterns that match the scoped setting. The goal is not to obtain a complete proof from the AI, but to construct a detailed proof skeleton, including but not limited to a main strategy, a sequence of reductions, and key lemmas and inequalities with clear logical dependencies. The AI is used to suggest plausible decompositions of the main claim, to recall standard complexity bounds under comparable assumptions, and to point to candidate references. Human experts then check compatibility with the scoped statement and record which external results will be instantiated and which conditions remain to be verified.
Example. For the convergence conjecture above, experience suggests that the iteration complexity of a gradient method is controlled by a Lipschitz constant of the gradient. As a first attempt, we ask the AI to estimate a Euclidean Lipschitz constant of the gradient and to combine it with standard Euclidean gradient descent bounds. The resulting rate has the wrong dependence on $N$ and is closer to $O(N/ε^2)$ than to the desired $O(√{N}/ε^2)$ . This shows that the Euclidean Lipschitz notion is not aligned with the target rate in our manifold setting.
We then ask the AI to search for complexity results for Riemannian gradient descent with retractions. The prompt is given in Appendix A.10. By discussion with our collaborators, we note that some of the relevant parts of [boumal2019global] may be helpful for our proof. We adopt the standard complexity result for Riemannian gradient descent with a Lipschitz continuous Riemannian gradient. This shifts the focus from a Euclidean Lipschitz constant to the Lipschitz constant $L_g$ of the pullback gradient of $f$ on $(U(N),canonical metric)$ . The desired rate $O(√{N}/ε^2)$ will follow if we can prove that the Lipschitz constant of the pullback gradient satisfies $L_Rie∈ O≤ft(√{\frac{N}{M}}\right).$ Using a constant step size $t=1/L_Rie$ , the Riemannian update achieves the targeted convergence rate. The final statement gives as follows.
**Theorem 5.4 (Baseline Complexity)**
*Suppose we run with the 5-factor retraction $R_U$ defined in (4), and choose a fixed step size $t_k=1/L_Rie$ , where $L_Rie=O(√{N/M})$ is defined as above. Then, for any $ε>0$ ,
$$
T≥≤ft\lceil\frac{2L_Rie}{ε^2}\right\rceil \Longrightarrow \min_0≤ k≤ T-1≤ft\|f≤ft(U_k\right)\right\|≤ε.
$$*
Thus the second stage produces a proof plan consisting of two main tasks. The first task is to establish a sharp estimate of $L_Rie$ on $U(N)$ with the canonical metric and the 5-factor retraction. The second task is to verify that the assumptions of the Riemannian complexity theorem are satisfied by our algorithm and manifold. The remaining work, namely the refinement of inequalities, calibration of constants, and numerical stress tests for the bound on $L_Rie$ , is carried out in the third stage.
#### 5.3.3 Parameter discovery: iterative estimates and numerical tests
Along the chosen route, some lemmas or inequalities involve parameters or coefficients that need sharp bounds. At this stage, human experts iterate with the AI on two parallel tracks.
(1) Parameter proposals and goal checks. Human experts state the explicit requirements that the final theorem imposes on the parameters. For example, that certain error terms must be bounded by a fraction of $ε$ . The AI proposes candidate values or bounds. Human experts test them against these requirements. Failed candidates are revised with short explanations (e.g. “this choice violates the inequality for large $N$ ”). Passing candidates are kept as the current best estimates. Over a few rounds, this yields a small table of admissible constants with clear justifications.
(2) Numerical stress tests for inequalities. For inequalities tied to the parameters, human experts ask AI to run simple numerical checks, often in low dimensions. They sample inputs from the relevant domain and verify whether each sample satisfies the inequality. When counterexamples appear, the language model analyze the pattern (for instance, whether violations occur only near the boundary of the domain) and tighten assumptions if needed.
By alternating these steps, human experts break the large problem into smaller, verifiable pieces that the AI can help address. The AI assists with variant generation, quick retrieval of known bounds, and parameter tuning, while human experts control the framework, proof logic, and acceptance criteria. At the end, the conjecture is refined into a stable theorem with a clear scope, a documented proof path, and constants validated by both analysis and targeted experiments.
Example. Continuing the running example, to prove the Lipschitz estimate above we first isolate the contribution of the retraction. We focus on the following two standard inequalities for a retraction $(·)$ :
$$
≤ft\|_x(η)-x\right\|≤α\|η\|, ≤ft\|_x(η)-x-η\right\|≤β\|η\|^2.
$$
We ask the AI to propose candidate values for $(α,β)$ that are valid on $U(N)$ for our chosen five factor retraction $R_U$ in Theorem 5.3. The language model suggests $α_tight=1, β_tight=\frac{1}{4c_0},$ where $c_0:=≤ft\|X_0\right\|_F=≤ft\|Y_0\right\|_F=≤ft\|≤ft[X_0,ψ_0\right]\right\|_F=\frac{√{2M(N-M)}}{N},$ for a suitable universal constant $c_0$ , and flags these as potentially tight. Human experts do not adopt these values blindly. The processed theorem states as follows.
**Theorem 5.5 (Tight first and second order bounds)**
*Consider the 5-factor retraction $R_U$ defined in (4). For all $U∈U(N)$ and $η∈WU$ , it holds
$$
≤ft\|R_U(η)-U\right\|_F≤\|η\|_F, ≤ft\|R_U(η)-U-η\right\|_F≤\frac{1}{4c_0}\|η\|_F^2.
$$
Moreover, both are globally tight: $\tfrac{≤ft\|R_U(η)-U\right\|_F}{\|η\|_F}→ 1,$ $\tfrac{≤ft\|R_U(η)-U-η\right\|_F}{\|η\|_F^2}→\frac{1}{4c_0},$ as $η→ 0$ .*
Guided by the prompt in Appendix A.11, the language model executes human’s task with an explicit propose-test-prove loop. The model first proposes $(α,β)$ , then itself designs and runs numerical stress tests on random $x∈U(N)$ and tangent vectors $η$ . If violations or unstable behavior are detected, the model revises its proposal and repeats the tests. Only once a pair $(α,β)$ consistently passes these numerical checks does the language model step in to turn the numerically validated guess into a full proof, for example, by checking the retraction assumptions and constructing a tightness argument around the hardest cases surfaced by the AI. In this way, the prompt shapes a tight human-AI interaction loop: the AI accelerates constant discovery and stress testing, while human experts focus on validation and theory, which together lead more quickly to reliable and near optimal parameters.
#### 5.3.4 Refining the theorem: structural insights and improved results
The collaboration does not conclude with the first successful proof. In the final stage, human experts review the baseline result to identify structural properties of the problem that may have been underutilized in the initial rough analysis. The goal here is to strengthen the theorem, including improving convergence rates, weakening assumptions, or simplifying the final constants.
In this phase, the interaction loop shifts from verification to discovery of structure. Human experts hypothesize stronger conditions (such as strong convexity, or the Polyak-Łojasiewicz (PL) inequality) and ask the AI to attempt to derive these conditions for the scoped object. If the AI can successfully derive a bound for the gradient norm in terms of the function value gap, the complexity analysis can be upgraded significantly without changing the underlying algorithm. This stage transforms a generic “worst-case” theorem into a “problem-specific” sharp result.
Example. Returning to our running example, Theorem 5.4 establishes a convergence rate of $O(ε^-2)$ . This is the standard guarantee for Riemannian gradient descent on general nonconvex smooth functions. However, human experts suspect that the specific objective function $f(U)=(HUψ_0U^†)$ possesses a better geometry near the optimum, specifically a relationship between the magnitude of the gradient and the suboptimality gap. We ask the language model for ways to get sharper convergence result. The concrete prompt is given in Appendix A.12.
The AI explored potential methods to achieve a faster convergence rate and proposed a feasible solution based on the PL property. In addition to identifying this path, the AI also clearly outlined the important verification steps we need to follow to validate this approach. The final refined result is stated as follows.
**Theorem 5.6 (Best Complexity via PL Inequality)**
*Consider the same assumptions as in Theorem 5.4. Let $q_k:=f≤ft(U_k\right)∈[0,1]$ be the objective value at step $k$ , and let $q_\max=1$ be the global maximum. Suppose the initial point satisfies a local contraction condition. Then, the Riemannian PL inequality holds, and for any target accuracy $0<ε≤ q_0$ , the iterates satisfy the optimality gap $1-q_T≤ε$ in at most $T=≤ft\lceil 6L_Rie\log≤ft(\frac{1}{ε}\right)\right\rceil$ iterations.*
This final improvement demonstrates the power of the workflow. The baseline proof provided the safety guarantees ( $L$ -smoothness), while the refinement stage exploited specific geometry to yield an exponential speedup in the theoretical rate, all formally verified through the same human-AI pipeline.
## 6 Roles of human and AI
We distinguish two roles for AI in theorem development: helping to prove a fixed statement and helping to discover new statements. In both cases, humans remain responsible for deciding what is asked, what is accepted, and how the results are recorded.
In theorem proving, human experts first fix the statement, the setting, and what counts as a satisfactory proof. They decide which definitions are allowed, which assumptions may be used, and which intermediate claims would be helpful. The LLM then works inside this frame. It suggests candidate lemmas, fills in algebraic or analytic steps, proposes formulations, and points to related known results. Any such suggestion is treated as a draft. Humans check whether the step is valid under the stated assumptions, whether it conflicts with known results, and whether it fits the overall argument. Only after this check is the step integrated into the proof with its role and dependencies made explicit. In theorem discovery, the setting is fixed but the conclusion is not. Humans specify the regime of interest and what they value in the result, such as interpretability, sharp bounds, or usefulness for later work. The LLM then proposes candidate statements and supporting evidence. Humans screen these candidates, refine the promising ones into precise conjectures. Recurring arguments can be turned into reusable patterns that can be adapted to similar problems with small changes in assumptions or constants.
In both settings, generation and validation are kept separate. Every AI-generated statement, lemma, counterexample, or constant should come with some form of evidence. Humans first perform a local check, verifying that the claim is correct under the given assumptions and notation, and then a global check, confirming that it fits coherently into the developing proof or conjecture. In this way, the LLM speeds up search and variation, while humans keep control over correctness, standards, and the final mathematical record.
## 7 Conclusion
We presented a practical human-in-the-loop workflow for frontier mathematics with a structured propose-check cycle. By enforcing a clear division of labor where human experts retain control over problem formulation and acceptance criteria while the AI generates candidate conjectures and auxiliary lemmas accompanied by machine verifiable evidence, we ensure that exploratory velocity does not compromise mathematical rigor. The efficacy of this methodology is demonstrated through a comprehensive case study on Riemannian optimization perspective for Grover’s algorithm, where the interactive pipeline successfully identified invariant subspaces, synthesized retraction operators via property constrained search, and refined convergence guarantees using Riemannian geometry. Ultimately, this framework transforms large language models into reliable research partners by converting model outputs into auditable artifacts, providing a scalable template for integrating AI into frontier scientific computing while maintaining transparent proof obligations.
## Appendix A Prompts for AI and replies
All prompts in this section can be copied from the relevant text blocks in the file “README.md” at https://github.com/optsuite/MathResearchPrompts.
### A.1 Prompts for Section 3.1
You are an expert in both quantum algorithms and mathematical optimization.
I want to identify promising points of contact between quantum algorithms and optimization that could lead to clean, analyzable research problems. You can refer to the paper I give you. Please do the following:
1. Give a concise briefing that figures out:
- The main quantum algorithmic primitives that are relevant here.
- The main optimization paradigms that might interact with them.
- Typical objectives, loss functions, and structural assumptions on each side.
1. Propose 5-8 concrete candidate research directions at this interface. For each direction, provide:
- A short description of the core idea.
- The main mathematical objects and assumptions.
- The nearest classical or existing results and what gap or limitation they leave.
- A plausible class of analysis techniques.
1. For each direction, add 2-3 sentences of feasibility notes:
- Why would this direction admit a clean theorem (or why it might fail).
- Any obvious degenerate or trivial regimes to watch out for.
- Whether you expect complexity or convergence guarantees to be within reach.
Format your answer as a numbered list of candidate directions, each with compact bullet points and feasibility notes. Avoid overly speculative ideas that are disconnected from existing theory.
### A.2 Prompts for Section 3.2
You are a theoretical mathematician specializing in the intersection of quantum algorithms and Riemannian optimization. Your goal is to build connection between quantum algorithmic structures and Riemannian optimization. We are investigating a Riemannian optimization explanation for quantum search algorithm. Specifically, we hypothesize that Grover’s algorithm can be rigorously interpreted as a form of Riemannian gradient descent. We need to identify the underlying connection before attempting a proof.
Task: Please provide a detailed theoretical framing for this intersection:
1. Object Identification: Define the precise mathematical objects on both sides. This must include the manifold of quantum states and the specific Riemannian gradient update rules that serve as the continuous analog.
1. Properties and Symmetries: Analyze the essential properties of Grover iterations, such as unitarity and query complexity. How do these map to the oracle complexity in Riemannian optimization?
1. Alignment Check: Identify specific regimes or limiting cases where the standard gradient like updates and the discrete Grover iterations coincide structurally.
### A.3 Prompts for Section 4.1
You are a careful mathematical assistant collaborating with human experts. When you are asked to prove a statement, you must:
1. restate all assumptions, notation, and domains of all variables;
1. give a numbered, line-by-line argument in which every nontrivial inference is explicitly justified;
1. cite standard results by their usual names (e.g. spectral theorem, Cauchy–Schwarz inequality) and never fabricate new references.
Prove the following statement in a concise but fully rigorous way. In your proof, you should in particular:
1. explain carefully why $f(U)=0$ is equivalent to $[H,ψ_U]=0$ .
1. prove both directions of the optimality claim: that $f(U)=0$ implies that $U$ is a global optimizer with $f(U)∈\{0,1\}$ , and that any global optimizer must satisfy $f(U)=0$ .
The statement gives as [Statement of Theorem 4.1].
Output format. Return only:
1. a LaTeX proof environment with a numbered, step-by-step derivation;
1. a short LaTeX itemize list of adversarial checks a reader could perform.
Do not output any text outside these two parts.
### A.4 Prompts for Section 4.2
Content. You are a careful mathematical assistant participating in a prove-or-disprove workflow. Your task is to analyze the structural statement below about commutators of Hermitian matrices and the Lie algebra $\mathfrak{su}(n)$ . When reasoning about this statement, you must:
1. Restate all assumptions, notation, and domains of the variables (including the ambient space $M_n(ℂ)$ , (skew-)Hermitian conditions, and the trace operator).
1. Run two explicit branches:
- Proof branch: Try to show that every traceless skew-Hermitian matrix can be written as a commutator $[A,B]$ with $A^†=A$ and $B^†=B$ . Use concrete constructions, basis expansions, or dimension arguments.
- Disproof branch: In parallel, look for structural obstructions or counterexamples. Analyze the subspace spanned by such commutators, check invariants, and probe whether some elements of $\mathfrak{su}(n)$ might fail to be commutators.
1. Within each branch, give a line-by-line argument in which every non-trivial inference is explicitly justified.
1. Cite standard facts (e.g. basic properties of commutators, spectral theorem, Lie algebra identities) by their usual names and never fabricate new references.
1. After exploring both branches, provide a final verdict: decide whether the proposition is true or false. If it is true, present a concise but fully rigorous proof; if it is false, present an explicit counterexample and explain why it fails.
Target statement (to prove or disprove). [Statement of Proposition 4.2].
Required output format. Return only the following three parts in LaTeX:
1. A Proof branch subsection with a numbered, step-by-step derivation attempting to prove the proposition.
1. A Disproof branch subsection with a numbered, step-by-step analysis searching for obstructions or counterexamples.
1. A Final verdict paragraph stating clearly whether the proposition is true or false, together with either a complete proof or a concrete counterexample, followed by a short itemize list of adversarial checks a human reader could perform.
Do not output any commentary outside these three parts.
### A.5 Model reply for Section 4.3
The part of the model output that inspired us to obtain Theorem 4.3 is as follows.
The Invariant “Jordan” Plane (Working Subspace). Because $H$ is a projector and $ψ_0$ is rank-one, the evolution is strictly confined to the Krylov subspace $K=span\{|ψ_0⟩,H|ψ_0⟩\}$ .
1. Algebraic reason: The operators $H$ and $ψ_0$ , when restricted to the subspace containing $|ψ_0⟩$ , form a closed $2× 2$ algebra (a single Jordan block of the pair $\{H,ψ_0\}$ ).
1. Geometric intuition: This is a “Grover plane” on the projective Hilbert space connecting the start state $ψ_0$ and the target state (the projection of $H$ ).
1. Subspace: The state $ψ_k$ remains in the same 2D “Jordan plane” $K$ as the baseline. The operators $H$ and $ψ_0$ act as $2× 2$ matrices on this subspace (specifically, rank-1 projectors with overlap angle $θ_0=\arccos√{q_0}$ ).
1. Dynamics: While the baseline flows continuously along the gradient $[H,ψ_k]$ , the product ansatz $e^iθ He^iφψ_0$ performs discrete rotations (Euler angle compositions) within the same 2D plane. It acts as a “bang-bang” control to approximate the geodesic flow.
Our observation The model identified that the system’s evolution is invariant under a specific 2D subspace, effectively reducing the dynamics to SU(2) rotations. We realized that this geometric confinement implies the existence of a low-dimensional algebraic structure. Consequently, we were able to derive Theorem 4.3, which replaces high-dimensional matrix operations with efficient, closed-form scalar recurrences ( $x,y,z,q$ ) suitable for classical tracking.
### A.6 Prompts for Section 5.1.1
You are a careful mathematical assistant helping with theorem discovery for a fixed dynamical setting. The assumptions and notation are fixed; the conclusions are not.
Setting. [Theorem setting for Proposition 5.1]. We study the following update rules for $U_k+1$ and $ψ_k+1$ .
Exact exponential step (“Exp update”): [exact update scheme in Proposition 5.1].
Our broader goal is to surface structurally meaningful consequences of this dynamics. These may include (but are not limited to) invariants, norm and energy identities, dimensional reductions, stability or monotonicity statements, convergence and one shot optimality conditions, and useful lemmas for later analysis.
Task. Starting from the setting above, use assumption-driven discovery to propose candidate conclusions. Proceed as follows.
1. Restate all assumptions and domains (projector properties of $H$ , rank-one nature of $ψ_k$ , ranges of $q_k$ and $γ_k$ , and the unitary dynamics for $U_k$ and $ψ_k$ ).
1. Generate candidate statements. Propose a list of concise, LaTeX-ready candidate claims. For each candidate:
- assign a type label that you choose (for example, Invariant, Norm identity, Scalar recursion, Convergence guarantee, etc.);
- provide a one or two sentence informal explanation of what the claim says and why it might be useful.
At least some candidates should reflect both local information (e.g. behavior in the Grover plane,) and global information (e.g. long-time dynamics), but you are free to propose additional categories of structural statements beyond these.
1. Selection. From the candidates that pass the tests, select a coherent subset (typically $3$ - $5$ items) that best captures the core structure of the Exp update. Combine them into a single proposition with numbered parts (i), (ii), (iii).
1. Clarity and rigor. When presenting the final proposition, give short, line-by-line derivations for each numbered item, with explicit justifications and citations of any standard facts used (e.g. properties of projectors, commutators, unitary rotations in a two-dimensional subspace). Avoid hand-waving and do not fabricate references.
Required output format. Return only:
1. a numbered list of candidate statements with their type labels, informal explanations, and pass/fail/inconclusive labels from the light-weight tests;
1. a final LaTeX proposition environment collecting the selected statements into a single theorem-style statement, together with a concise, step-by-step proof;
1. a short itemize list of adversarial checks that a human reader could apply to stress-test the final proposition and its assumptions.
### A.7 Prompts for Section 5.1.2
You are a careful mathematical assistant collaborating with human experts on theorem discovery and cross-setting transfer.
Treat the setting below as one instance of a more general pattern rather than as an isolated calculation. Your goals are to extract a reusable schema that can be instantiated in nearby settings and apply it on a similar setting.
Baseline target. [Statement of Proposition 5.1].
Instructions. Organize your answer into three sections.
1. Abstract schema. Extract the structural ingredients behind the baseline target including but not limited to.
- the working invariant subspace;
- the associated “gradient plane” or tangent plane;
- the scalar progress coordinate;
- the structured local update
1. Transfer notes (invariant-product setting).
Transfer the above conclusion in the following setting. [Basic setting in Theorem 5.2]. In this product setting:
- Propose candidate analogues of the baseline schema.
- Formulate concrete transferred statements (propositions or conjectures).
- Give me the proof of the new results you propose.
Output format. a final LaTeX proposition environment collecting the selected surviving statements into a single theorem-style statement, together with a concise, step-by-step proof.
### A.8 Prompts for Section 5.2
Content. You are a careful mathematical assistant for mathematical discovery. The goal is to construct a product retraction $γ(t;x,y)$ that satisfies a fixed list of properties; the admissible building blocks and the target properties are given, but the concrete product form is not.
Setting. Let $H=H^†=H^2$ be a projector and let $ψ_0$ be a rank-one projector. Define $X_0:=[H,ψ_0], Y_0:=i[H,X_0], W:=span_ℝ\{X_0,Y_0\}.$ For each $(x,y)∈ℝ^2$ , we consider tangent targets $Z=xX_0+yY_0∈W,$ and search for retractions $γ(t;x,y)$ on the unitary group with the following properties: [Constraints (P1) - (P3)].
Task. Design $γ(t;x,y)$ by property-constrained synthesis. Proceed as follows.
1. Restate the constraints. Summarize the admissible factor types, the target space $W$ , and properties (P1)–(P3) in your own words, making clear which quantities are fixed data ( $H,ψ_0,X_0,Y_0$ ) and which are design choices (product length, coefficient couplings, dependence on $t,x,y$ ).
1. Propose candidate product forms. Generate a small, ordered list of candidate ansätze for $γ(t;x,y)$ :
- Each candidate must be an explicit product of exponentials $e^iθ_jH$ or $e^iθ_jψ_0$ with scalar parameters $(a_j,b_j,\dots)$ that may depend on $t,x,y$ .
- Prefer shorter products; include candidates of different lengths (e.g. length $5,6,\dots$ ) so that there is a chance to find the shortest viable form.
- For each candidate, give a one- or two-sentence explanation of how the chosen ordering and parameter couplings might help satisfy (P2)-(P3).
1. Numerical finite-difference tests. For each candidate, use a seed set $S⊂ℝ^2$ , a small step size $h>0$ , and a tolerance $ε>0$ to write concrete code (e.g. in Python) that:
- implements $γ(t;x,y)$ for given $(x,y)$ and parameter values;
- checks (P1) syntactically;
- checks (P2) exactly at $t=0$ ;
- checks (P3) numerically on the seed set $S$ via the finite-difference test [Equation (3)] and reports pass/fail outcomes for the test, including edge cases such as $(x,0)$ and $(0,y)$ .
The code must be executable, and you should run it to verify your construction.
1. Selection and refinement. Among all candidates that pass the numerical tests on $S$ , identify the shortest product that appears robust. For this selected candidate:
- summarize the final parameter constraints;
- restate the product in a clean, theorem-ready form;
- sketch a proof plan for why (P1)-(P3) hold exactly, indicating which algebraic identities and expansions need to be verified.
Required output format. Return only:
1. a numbered list of candidate product forms with their informal explanations and symbolic viability labels;
1. the fully specified, shortest selected candidate in LaTeX, together with a brief, step-by-step derivation of the parameter constraints ensuring (P1)-(P3);
1. executable Python code for the numerical tests on $S$ , including the finite-difference check above, and a short itemize list of adversarial checks a human reader could apply to stress-test the construction.
### A.9 Prompts for Section 5.3.1
You are an expert mathematical research collaborator specializing in geometric analysis, numerical optimization, and formal verification. I will present a rough, informal target theorem or conjecture. Your goal is to help me formalize this statement and analyze its provability.
Core Responsibilities:
1. Clarification: take my vague concepts and propose precise mathematical definitions. Explicitly define the ambient space, the metric, and the notion of gradient. List necessary assumptions required to make the statement well-posed.
1. Feasibility and proof strategy: analyze the logical structure of the conjectured bound or equality. Propose feasible proof paths: Suggest specific techniques. Identify potential bottlenecks or technical difficulties in the proof.
1. Literature and context: connect the conjecture to standard results or known theorems in the field. If the conjecture seems standard or trivial, point it out. If it contradicts known counterexamples, warn me immediately.
Format: Use LaTeX for all mathematical expressions. Your response must be logically organized, prioritizing mathematical clarity and insight over formatting.
### A.10 Prompts for Section 5.3.2
You are familiar with Riemannian optimization and first-order complexity theory. I am looking at a gradient method on a Riemannian manifold. A naive Euclidean analysis treats the manifold as a subset of a Euclidean space, takes a Lipschitz constant of the ambient gradient, and plugs this into standard Euclidean gradient-descent bounds; this gives the wrong dependence on the dimension. I want to understand the correct Riemannian framework and the relevant literature. Please do the following:
1. Explain briefly why ambient Euclidean Lipschitz constants for $∇ f$ can lead to suboptimal or dimension-misaligned complexity bounds for algorithms that are intrinsically Riemannian, and why the natural object is a Lipschitz constant for the Riemannian gradient (or for the pullback gradient under a retraction).
1. List 3-6 key references (books or papers) on Riemannian gradient descent or related first-order methods with retractions and Lipschitz-continuous Riemannian gradients. For each reference, give a short summary (2-3 sentences) indicating:
- the type of manifold considered,
- the smoothness assumptions,
- the basic complexity statement.
1. From these references, extract a generic complexity theorem for Riemannian gradient descent with retractions and Lipschitz-continuous Riemannian gradient and list the main structural assumptions on the manifold, the retraction, and the function.
### A.11 Prompts for Section 5.3.3
You are a mathematical assistant with strong background in matrix manifolds and Riemannian optimization.
Setting. Work on the unitary group $U(N)=\{U∈ℂ^N× N:U^∗U=I\},$ equipped with the canonical Riemannian metric induced by the Frobenius inner product. Let $\|·\|$ denote the Frobenius norm, and $T_xU(N)$ the tangent space at $x∈U(N)$ . We use the following length-5 product retraction [Equation (4)] with real parameters $(a_1,a_2,b_1,b_2)$ via (5). Here $H$ and $ψ_0$ are fixed Hermitian matrices, and $(x,y)$ are scalar coefficients associated with the tangent vector $η$ (you may assume a reasonable linear relation). The retraction at $U∈U(N)$ in direction $η∈ T_UU(N)$ is defined by $_U(η):=γ(1;x_η,y_η)$ for the corresponding scalars $(x_η,y_η)$ .
Goal. Find sharp global constants $α$ and $β$ (ideally optimal, or close to optimal) such that, for all $U∈U(N)$ and all tangent vectors $η∈ T_UU(N)$ in a suitable step-size range, $\|_U(η)-U\|≤α\|η\|, \|_U(η)-U-η\|≤β\|η\|^2.$
Requirement. You must proceed in the following order:
1. propose candidate constants and simple numerical tests.
- Propose reasonable candidate constants $(α,β)$ , with a brief explanation.
- Then design and explicitly perform simple numerical experiments that you would run to test these constants.
- Based on these tests, explain how you would confirm or adjust your candidate $(α,β)$ (for example, by taking them slightly larger).
1. give a theoretical justification.
- Using the explicit product form of $γ(t;x,y)$ , derive theoretical bounds that prove the two inequalities above with your final choice of constants (or with slightly relaxed constants if needed).
- Keep the argument as simple and direct as possible, using standard matrix inequalities and expansions, and make the dependence on $N$ clear if it appears.
1. comment briefly on tightness. Explain whether the constants you obtain seem tight or near-tight, using both your heuristic reasoning and the (hypothetical) numerical evidence.
### A.12 Prompts for Section 5.3.4
You are an expert in both quantum algorithms and mathematical optimization. We are analyzing the convergence of a Riemannian gradient descent algorithm with retractions on $U(N)$ . The objective function is: $f(U)=(HUψ_0U^†)$ where $H$ and $ψ_0$ are Hermitian matrices. The manifold is equipped with the canonical metric induced by the Frobenius inner product.
Current Baseline Result We have successfully established a complexity bound. The current theorem is as follows: [Statement of Theorem 5.4].
Request for Deeper Theoretical Analysis The result above gives a sublinear rate ( $O(ε^-2)$ ), which applies to generic smooth non-convex functions. However, our objective function $f(U)$ has a very specific algebraic structure (a linear trace function on the unitary group). I suspect that the baseline analysis is too conservative because it ignores this specific structure. Please perform a deeper theoretical analysis to see if we can improve this bound:
1. Structural Analysis: Analyze the algebraic relationship between the norm of the Riemannian gradient, $\|f(U)\|$ , and the function value gap. Does the specific form of $f(U)$ imply a stronger geometric property than simple smoothness?
1. Improved Convergence: If such a relationship exists, does it allow us to prove a faster convergence rate (e.g., linear convergence instead of sublinear) under the same algorithmic settings?
1. Refined Theorem: If you find a stronger bound, please formulate a new theorem that reflects this improved rate and the corresponding iteration count $T$ .