Proving olympiad geometry theorems on a superconducting quantum processor

• URL: http://arxiv.org/abs/2609.14533v1
• Date: Sun, 13 Sep 2026 14:10:44 GMT
• Title: Proving olympiad geometry theorems on a superconducting quantum processor
• Abstract summary: Automated proving seeks to use computational systems to prove or disprove logical statements.<n>Recent neuro-symbolic systems have achieved remarkable progress, but their operation is constrained by classical computational parallelism.<n>Here we report the realization of automated geometry theorem proving on a fully programmable superconducting quantum processor.
• Score: 18.064812936697283
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Automated theorem proving seeks to use computational systems to prove or disprove mathematical and logical statements [1, 2]. It underpins a wide range of applications, and enhancing theorem-proving capabilities remains a central objective in artificial intelligence [3]. Although recent neuro-symbolic systems have achieved remarkable progress [4-7], their operation is ultimately constrained by classical computational architectures. Quantum computing [8], by contrast, enables information encoding and coherent parallelism beyond classical limits [9-14], raising the possibility of accelerating structured symbolic deduction [15]. Here we report the experimental realization of automated geometry theorem proving on a fully programmable superconducting quantum processor. We develop two complementary quantum proving frameworks. The first implements Wu's algebraic elimination method using quantum pseudo-division, with multivariate polynomials represented in superposition states, enabling quantum algebraic theorem proving. The second implements the full-angle method as backward symbolic reasoning through a hybrid quantum strategy-guided architecture, demonstrating a general route toward quantum symbolic proof search. As illustrative examples, we prove two theorems on a superconducting quantum processor: the perpendicularity of the diagonals of a square and a 1978 International Mathematical Olympiad geometry problem. Our results establish, at the experimental level, automated logical reasoning as a viable task for near-term quantum processors and provide a concrete pathway toward quantum-enhanced symbolic intelligence.

Related papers

• Quantum Computing Algebra (QCA), the theory and implementation [0.2249916681499244]
  We present a real geometric algebra framework designed for the direct translation of the Dirac formalism into geometric algebra representations.<n>We show how quantum gates and multi-qubit systems can be efficiently represented and generated computationally.
  arXiv  Detail & Related papers  (2026-06-16T07:27:40Z)
• Quantum automated theorem proving [15.134110328567838]
  We propose a generic framework for quantum automated theorem proving.<n>We introduce quantum representations of knowledge bases and propose corresponding reasoning algorithms for a variety of tasks.<n>We show how automated reasoning can be achieved with quantum resolution in both propositional and first-order logic.
  arXiv  Detail & Related papers  (2026-01-12T19:39:33Z)
• Exponential quantum speedups in quantum chemistry with linear depth [0.0]
  We prove a connection to particle number conserving matchgate circuits with fermionic magic state inputs.<n>We apply this result to quantum multi-reference methods designed for near-term hardware.<n>We discuss the implications for achieving exponential quantum advantage in quantum chemistry on near-term hardware.
  arXiv  Detail & Related papers  (2025-03-26T23:15:32Z)
• Bridging Classical and Quantum: Group-Theoretic Approach to Quantum Circuit Simulation [0.0]
  Efficiently simulating quantum circuits on classical computers is a fundamental challenge in quantum computing. This paper presents a novel theoretical approach that achieves exponential speedups (polynomial runtime) over existing simulators. The findings may have implications for quantum algorithm design, error correction, and the development of more efficient quantum simulators.
  arXiv  Detail & Related papers  (2024-07-28T20:02:21Z)
• From Entanglement to Universality: A Multiparticle Spacetime Algebra Approach to Quantum Computational Gates Revisited [0.0]
  We focus on testing the usefulness of geometric algebras (GAs) techniques in two applications to quantum computing. First, we offer an explicit algebraic characterization of one- and two-qubit quantum states together with a MSTA description of one- and two-qubit quantum computational gates. In this first application, we devote special attention to the concept of entanglement, focusing on entangled quantum states and two-qubit entangling quantum gates.
  arXiv  Detail & Related papers  (2024-05-13T19:51:26Z)
• Quantum Circuit Completeness: Extensions and Simplifications [44.99833362998488]
  The first complete equational theory for quantum circuits has only recently been introduced. We simplify the equational theory by proving that several rules can be derived from the remaining ones. The complete equational theory can be extended to quantum circuits with ancillae or qubit discarding.
  arXiv  Detail & Related papers  (2023-03-06T13:31:27Z)
• A Complete Equational Theory for Quantum Circuits [58.720142291102135]
  We introduce the first complete equational theory for quantum circuits. Two circuits represent the same unitary map if and only if they can be transformed one into the other using the equations.
  arXiv  Detail & Related papers  (2022-06-21T17:56:31Z)
• No-signalling constrains quantum computation with indefinite causal structure [45.279573215172285]
  We develop a formalism for quantum computation with indefinite causal structures. We characterize the computational structure of higher order quantum maps. We prove that these rules, which have a computational and information-theoretic nature, are determined by the more physical notion of the signalling relations between the quantum systems.
  arXiv  Detail & Related papers  (2022-02-21T13:43:50Z)
• Realization of arbitrary doubly-controlled quantum phase gates [62.997667081978825]
  We introduce a high-fidelity gate set inspired by a proposal for near-term quantum advantage in optimization problems. By orchestrating coherent, multi-level control over three transmon qutrits, we synthesize a family of deterministic, continuous-angle quantum phase gates acting in the natural three-qubit computational basis.
  arXiv  Detail & Related papers  (2021-08-03T17:49:09Z)
• Depth-efficient proofs of quantumness [77.34726150561087]
  A proof of quantumness is a type of challenge-response protocol in which a classical verifier can efficiently certify quantum advantage of an untrusted prover. In this paper, we give two proof of quantumness constructions in which the prover need only perform constant-depth quantum circuits.
  arXiv  Detail & Related papers  (2021-07-05T17:45:41Z)
• Quantum simulation of gauge theory via orbifold lattice [47.28069960496992]
  We propose a new framework for simulating $textU(k)$ Yang-Mills theory on a universal quantum computer. We discuss the application of our constructions to computing static properties and real-time dynamics of Yang-Mills theories.
  arXiv  Detail & Related papers  (2020-11-12T18:49:11Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.