# A Human-AI Collaborative Workflow for Mathematical Discovery: A Case Study in Grover-Compatible Riemannian Optimization

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

## Key facts

- Cited by 4 papers in the map (data through 14 Oct 2026).
- Builds on 30 of its 62 references that are in the map.
- First posted on arXiv 10 Dec 2025.

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

- [Chain-of-Thought Prompting Elicits Reasoning in Large Language Models](https://mlsanity.com/paper/2201.11903/) (2022)
- [Retrieval-Augmented Generation for Knowledge-Intensive NLP Tasks](https://mlsanity.com/paper/2005.11401/) (2020)
- [BART: Denoising Sequence-to-Sequence Pre-training for Natural Language Generation, Translation, and Comprehension](https://mlsanity.com/paper/1910.13461/) (2019)
- [Solving Quantitative Reasoning Problems with Language Models](https://mlsanity.com/paper/2206.14858/) (2022)
- [PEGASUS: Pre-training with Extracted Gap-sentences for Abstractive Summarization](https://mlsanity.com/paper/1912.08777/) (2019)
- [The AI Scientist: Towards Fully Automated Open-Ended Scientific Discovery](https://mlsanity.com/paper/2408.06292/) (2024)
- [Convex Optimization: Algorithms and Complexity](https://mlsanity.com/paper/1405.4980/) (2014)
- [AI Feynman: a Physics-Inspired Method for Symbolic Regression](https://mlsanity.com/paper/1905.11481/) (2019)
- [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023)
- [Generative Language Modeling for Automated Theorem Proving](https://mlsanity.com/paper/2009.03393/) (2020)
- [DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition](https://mlsanity.com/paper/2504.21801/) (2025)
- [Deep Research Agents: A Systematic Examination And Roadmap](https://mlsanity.com/paper/2506.18096/) (2025)
- [ReviewerGPT? An Exploratory Study on Using Large Language Models for Paper Reviewing](https://mlsanity.com/paper/2306.00622/) (2023)
- [AutoSurvey: Large Language Models Can Automatically Write Surveys](https://mlsanity.com/paper/2406.10252/) (2024)
- [Gold-medalist Performance in Solving Olympiad Geometry with AlphaGeometry2](https://mlsanity.com/paper/2502.03544/) (2025)
- [DeepSeekMath-V2: Towards Self-Verifiable Mathematical Reasoning](https://mlsanity.com/paper/2511.22570/) (2025)
- [MLR-Copilot: Autonomous Machine Learning Research based on Large Language Models Agents](https://mlsanity.com/paper/2408.14033/) (2024)
- [OpenReviewer: A Specialized Large Language Model for Generating Critical Scientific Paper Reviews](https://mlsanity.com/paper/2412.11948/) (2024)
- [Global rates of convergence for nonconvex optimization on manifolds](https://mlsanity.com/paper/1605.08101/) (2016)
- [ReviewRobot: Explainable Paper Review Generation based on Knowledge Synthesis](https://mlsanity.com/paper/2010.06119/) (2020)
- [A Comprehensive Survey of Deep Research: Systems, Methodologies, and Applications](https://mlsanity.com/paper/2506.12594/) (2025)
- [Iterative Refinement of Project-Level Code Context for Precise Code Generation with Compiler Feedback](https://mlsanity.com/paper/2403.16792/) (2024)
- [SurveyX: Academic Survey Automation via Large Language Models](https://mlsanity.com/paper/2502.14776/) (2025)
- [Methods for Convex (L0,L1)-Smooth Optimization: Clipping, Acceleration, and Adaptivity](https://mlsanity.com/paper/2409.14989/) (2024)
- [ResearchCodeAgent: An LLM Multi-Agent System for Automated Codification of Research Methodologies](https://mlsanity.com/paper/2504.20117/) (2025)
- [Machine Learning meets Algebraic Combinatorics: A Suite of Datasets Capturing Research-level Conjecturing Ability in Pure Mathematics](https://mlsanity.com/paper/2503.06366/) (2025)
- [Machine learning assisted exploration for affine Deligne-Lusztig varieties](https://mlsanity.com/paper/2308.11355/) (2023)
- [LLM-Ref: Enhancing Reference Handling in Technical Writing with Large Language Models](https://mlsanity.com/paper/2411.00294/) (2024)
- [Near-Optimal Convergence of Accelerated Gradient Methods under Generalized and (L0, L1)-Smoothness](https://mlsanity.com/paper/2508.06884/) (2025)
- [A Grover-compatible manifold optimization algorithm for quantum search](https://mlsanity.com/paper/2512.08432/) (2025)

## Built on by (most cited first, 4 of 4)

- [Towards Autonomous Mathematics Research](https://mlsanity.com/paper/2602.10177/) (2026)
- [ReasFlow: Assisting Reasoning-Centric Scientific Discovery in Applied Mathematics via a Knowledge-Based Multi-Agent System](https://mlsanity.com/paper/2607.14178/) (2026)
- [Vibe Reasoning: Eliciting Frontier AI Mathematical Capabilities -- A Case Study on IMO 2025 Problem 6](https://mlsanity.com/paper/2512.19287/) (2025)
- [From Meta Idea to Advanced Mathematical Discovery -- Human-AI Co-Discovery of Sign-Embedding Quantum Algorithms](https://mlsanity.com/paper/2606.24899/) (2026)

## Abstract (arXiv)

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 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 main case study on the connection between manifold optimization and Grover's quantum search algorithm, where the pipeline identifies invariant subspaces and explores Grover-compatible retractions. The main case study uses the corresponding Grover-compatible convergence analysis, including an O(√N log(1/varepsilon)) PL-based bound established in the companion mathematical work, to illustrate the refinement stage of the workflow. Prompt records and reusable templates for implementing the workflow are provided. We further include a multi-oracle case study, document representative failed and corrected routes arising from this setting, and provide a structured failure-mode analysis.