Searcharxiv⌕ Search
Home/Archive/arXiv

arXiv · 2610.30216

Lean-QuantumAlg: A Framework for AI Agents to Produce Quantum Algorithms that Humans Can Trust

Lei Zhang·Mingrui Jing·Yusheng Zhao·Jiahong Liu·Xin Wang
View original source ↗Read source document ↗Export metadata ↓

Abstract

AI agents are increasingly capable of constructing quantum algorithms and proofs, yet machine-checked proofs alone cannot guarantee that the intended problem is solved or that resource claims match the verified computation.Here we introduce Lean-QuantumAlg, a Lean 4 framework for trustworthy AI-assisted development of quantum algorithms.Its Algorithm-Solves-Problem contract binds correctness, success probability, borrowed-state restoration and quantum and classical resource bounds to a single execution, while separating the guarantees that Lean checks from the problem specifications and execution models that humans review. We demonstrate the framework on nine AI-formalized quantum algorithms, from Grover search to quantum attacks on RSA-2048 and P-256, with less than 1% of each algorithm's imported source code requiring statement-level human review once the shared framework has been audited. By integrating reusable mathematical foundations, certified algorithmic primitives and execution-grounded verification, Lean-QuantumAlg provides a basis for AI agents to construct and certify quantum algorithms, opening a path toward scalable AI-driven discovery of quantum algorithms.

Explore related subjects

quant-ph

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

Lei Zhang, Mingrui Jing, Yusheng Zhao, Jiahong Liu, Xin Wang. 2026-10-21. Lean-QuantumAlg: A Framework for AI Agents to Produce Quantum Algorithms that Humans Can Trust. https://arxiv.org/abs/2610.30216

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

arXiv2026

Computational reach of machine learning models is independent of untrained quantum resources

This paper proves that if an untrained quantum circuit is used as a resource in a machine learning model, then on average no resource quantum circuit is better than any other that can achieve the same set of computational effects. The paper also proves a supporting theorem that even if certain mild idealisations are omitted, the average quantum advantage remains negligible at best. These results cast serious doubt on several proposals to use untrained quantum circuits in machine learning models: at best such claims should be substantiated empirically, as this paper proves there is no a priori theoretical reason to suppose that introducing an untrained quantum circuit will increase performance.

quant-ph↗
arXiv2026

Operator quantum singular value transformation: Spectral mapping, design and topological invariants

Quantum singular value transformation (QSVT) provides a unifying framework for quantum algorithms by applying the polynomials of quantum signal processing (QSP) to block-encoded matrices. We connect this framework with spectral analysis, design and topological protection in condensed matter physics. Extending QSVT beyond matrices to possibly infinite-dimensional operators (operator QSVT), we establish the following. First, it transforms every block of the operator by the QSP polynomials; no singular value decomposition is needed. Second, a spectral mapping theorem determines the full spectrum of the QSVT operator, including continuous spectra, from the embedded operator through the QSP polynomial, allowing spectral analysis without translation invariance. Third, the spectral mapping turns QSP into spectral design: the QSP phases can stretch, fold and separate the bands and place the eigenvalues. Finally, the kernel sectors that conventional QSVT usually sets aside carry a topological index, invariant under the choice of QSP phases, local perturbations and gap-preserving deformations, which guarantees topologically protected states. These results unify two quantum walks: Szegedy's walk from quantum algorithms and the split-step walk from condensed matter physics. Their kernel sectors encode the graph's Euler characteristic and the difference of bulk winding numbers, respectively. For the split-step walk, QSP breaks chiral symmetry but not the topological protection, and can move the protected state into a continuous band to form a bound state in the continuum (BIC).

quant-ph↗
arXiv2026

Quantum theory of molecular orientation

We formulate a quantum phase space for rotational and nuclear-spin states of rigid molecules. For each nuclear spin isomer, we re-derive the isomer's admissible angular momentum states from molecular geometry and nuclear-spin data, introduce its angular position states using quantization theory, and develop a generalized Fourier transform converting between the two. We classify molecules into three types -- asymmetric, rotationally symmetric, and perrotationally symmetric -- with the last type having no macroscopic analogue due to nuclear-spin statistics constraints. We discuss two general features in perrotationally symmetric state spaces that are Hamiltonian-independent and induced solely by symmetry and spin statistics. First, we quantify when and how an isomer's state space is completely rotation-spin entangled, meaning that it does not admit any separable states. Second, we identify isomers whose position states house an internal pseudo-spin or "fiber" degree of freedom, and the fiber's Berry phase or matrix after adiabatic changes in position yields naturally robust operations, akin to braiding anyonic quasiparticles or realizing fault-tolerant quantum gates. We outline how the fiber can be used as a quantum error-correcting code and discuss scenarios where these features can be experimentally probed

quant-ph↗