A Human-AI Collaborative Workflow for Mathematical Discovery: A Case Study in Grover-Compatible Riemannian Optimization
cs.HC, cs.AI, math.OC
Submitted: 2025-12-10
Updated: 2026-09-21
Comments: This paper was previously titled "Advancing Mathematical Research via Human-AI Interactive Theorem Proving''
Code: https://github.com/optsuite/MathResearchPrompts
License: http://creativecommons.org/licenses/by/4.0/
The gist: We investigate how large language models can be used as research tools in scientific computing while preserving mathematical rigor.
Terminology
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 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(sqrt N (1/epsilon)) 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.
Sources
- Iterative Refinement of Project-Level Code Context for Precise Code Generation with Compiler Feedback
- Machine Learning meets Algebraic Combinatorics: A Suite of Datasets Capturing Research-level Conjecturing Ability in Pure Mathematics
- Gold-medalist Performance in Solving Olympiad Geometry with AlphaGeometry2
- LLM-Ref: Enhancing Reference Handling in Technical Writing with Large Language Models
- Distinguishing Calabi-Yau Topology using Machine Learning
- Winning Gold at IMO 2025 with a Model-Agnostic Verification-and-Refinement Pipeline
- Deep Research Agents: A Systematic Examination And Roadmap
- OpenReviewer: A Specialized Large Language Model for Generating Critical Scientific Paper Reviews
- BART: Denoising Sequence-to-Sequence Pre-training for Natural Language Generation, Translation, and Comprehension
- MLR-Copilot: Autonomous Machine Learning Research based on Large Language Models Agents
- SurveyX: Academic Survey Automation via Large Language Models
- ReviewerGPT? An Exploratory Study on Using Large Language Models for Paper Reviewing
- The AI Scientist: Towards Fully Automated Open-Ended Scientific Discovery
- ReviewRobot: Explainable Paper Review Generation based on Knowledge Synthesis
- A Comprehensive Survey of Deep Research: Systems, Methodologies, and Applications
Related papers
- EduGage: A Multimodal Dataset and Benchmark for Sensor-Based Momentary Assessment of Engagement in Self-Guided Video Learning
- EvoDesign: Agentic Editable Diagram Creation via Design Expertise Evolution
- HAGI++: Head-Assisted Gaze Imputation and Generation
- Linking Behaviour and Perception to Evaluate Meaningful Human Control over Partially Automated Driving
- Review of Explainable Decision Support and Adaptive Human-Machine Interfaces for Automation Transparency in Maritime Autonomous Surface Ships
- Towards Cognitive Process-Aware Proactive Writing Support