Skip to content
aiqbench takeAI + Quantum

aiqbench analysis

This paper presents a rigorous human-in-the-loop framework where LLMs act as search engines for mathematical proofs while experts maintain control over problem formulation and verification. The study specifically bridges classical manifold optimization with Grover's quantum search algorithm, demonstrating how AI can identify invariant subspaces within quantum-compatible retractions. By providing reusable templates and a structured failure-mode analysis, the work offers a practical blueprint for integrating generative models into high-stakes scientific discovery without compromising mathematical rigor.
Source coveringarXiv
What this isA model's reading of the article and related coverage, written for aiqbench. Not the publisher's words.

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

arXiv2 min read

arXiv:2512.09443v3 Announce Type: replace-cross 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} \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.

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} \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.

Human-Computer Interaction (cs.HC); Artificial Intelligence (cs.AI); Optimization and Control (math.OC)

arXiv:2512.09443 [cs.HC]

(or arXiv:2512.09443v3 [cs.HC] for this version)

https://doi.org/10.48550/arXiv.2512.09443 Focus to learn more arXiv-issued DOI via DataCite

arXivLabs is a framework that allows collaborators to develop and share new arXiv features directly on our website.

Both individuals and organizations that work with arXivLabs have embraced and accepted our values of openness, community, excellence, and user data privacy. arXiv is committed to these values and only works with partners that adhere to them.

Have an idea for a project that will add value for arXiv's community? Learn more about arXivLabs.

Full text under the publisher's open licence · 285 words

Related coverage