Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Log inSign up
Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Blog
Job Board
Q3AS

© 2026 Aqora Quantum S.A.S.

TermsPrivacyLegal Notice

arXiv:2601.07953

Quantum automated theorem proving

Zheng-Zhi Sun, Qi Ye, Dong-Ling Deng

quant-phcs.AISubmitted Jan 12, 2026• Announced Jan 14, 2026• 0 citations
arXivHTMLPDF

Abstract

Automated theorem proving, or more broadly automated reasoning, aims at using computer programs to automatically prove or disprove mathematical theorems and logical statements. It takes on an essential role across a vast array of applications and the quest for enhanced theorem-proving capabilities remains a prominent pursuit in artificial intelligence. Here, we propose a generic framework for quantum automated theorem proving, where the intrinsic quantum superposition and entanglement features would lead to potential advantages. In particular, we introduce quantum representations of knowledge bases and propose corresponding reasoning algorithms for a variety of tasks. We show how automated reasoning can be achieved with quantum resolution in both propositional and first-order logic with quadratically reduced query complexity. In addition, we propose the quantum algebraic proving method for geometric theorems, extending Wu's algebraic approach beyond the classical setting. Through concrete examples, including geometry problems from the International Mathematical Olympiad, we demonstrate how a quantum computer may prove geometric theorems with quadratic better query complexity. Our results establish a primary approach towards building quantum automatic theorem provers, which would be crucial for practical applications of both near-term and future quantum technologies.

Related papers

Automated Theorem Proving for Quantum Circuit Verification

Jincheng Zhang

This paper presents a novel approach to automated theorem proving specifically tailored for quantum circuit verification. The core idea is to construct a formal system that leverages logical reasoning and proof techniques to rigorously analyze quantum circuit designs. This system aims to identify errors and inconsistencies within the circuit, ensuring compliance with the fundamental principles of quantum mechanics. The proposed method moves beyond traditional circuit simulation, offering a mathematically sound guarantee of correctness. We detail the architecture of the theorem prover, focusing on the representation of quantum circuits and the application of proof strategies. The system utilizes a combination of techniques including logical deduction, model checking, and constraint solving, adapted for the unique characteristics of quantum computation. The paper outlines the key components of this system and highlights its potential to significantly improve the trustworthiness and reliability of quantum computing technologies. The central aim is to establish a robust framework for automated verification, reducing the risk of errors and accelerating the development of quantum software.

•Aug 31, 2026•0 citations

Proving olympiad geometry theorems on a superconducting quantum processor

Ning Wang, Zheng-Zhi Sun, Zhengyi Cui +32 more

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.

quant-pharXiv:2609.14533•Sep 15, 2026•0 citations

Symbolic Specification and Reasoning for Quantum Data and Operations

Mingsheng Ying

In quantum information and computation research, symbolic methods have been widely used for human specification and reasoning about quantum states and operations. At the same time, they are essential for ensuring the scalability and efficiency of automated reasoning and verification tools for quantum algorithms and programs. However, a formal theory for symbolic specification and reasoning about quantum data and operations is still lacking, which significantly limits the practical applicability of automated verification techniques in quantum computing. In this paper, we present a general logical framework, called Symbolic Operator Logic $\mathbf{SOL}$, which enables symbolic specification and reasoning about quantum data and operations. Within this framework, a classical first-order logical language is embedded into a language of formal operators used to specify quantum data and operations, including their recursive definitions. This embedding allows reasoning about their properties modulo a chosen theory of the underlying classical data (e.g., Boolean algebra or group theory), thereby leveraging existing automated verification tools developed for classical computing. It should be emphasised that this embedding of classical first-order logic into $\mathbf{SOL}$ is precisely what makes the symbolic method possible. We envision that this framework can provide a conceptual foundation for the formal verification and automated theorem proving of quantum computation and information in proof assistants such as Lean, Coq, and related systems.

cs.PLCross-listedarXiv:2512.22383•Dec 30, 2025•0 citations

Quantum Entanglement-Accelerated Symbolic Reasoning

Jincheng Zhang

This paper explores the potential of leveraging quantum entanglement to significantly accelerate symbolic reasoning and knowledge graph queries. Traditional symbolic reasoning methods often struggle with the inherent challenges of encoding and searching large amounts of logical information, leading to computational bottlenecks. We propose a novel approach that utilizes quantum entanglement to overcome these limitations. The core idea is to decompose symbolic logic problems into multiple entangled qubit sets. Through superposition and interference of these entangled states, parallel inference is enabled. Finally, quantum measurements yield the solution. This approach promises exponential speedups compared to classical methods, offering a fundamentally new paradigm for logical deduction and knowledge retrieval. The paper details the theoretical framework, outlining the key equations and mathematical representations underpinning the proposed methodology. We present a detailed model that incorporates the principles of quantum mechanics to accelerate the process of symbolic inference. This research contributes to the emerging field of quantum information science and its potential applications in artificial intelligence and knowledge management.

•Sep 7, 2026•0 citations

Automated Theorem Proving for Quantum Circuit Verification using Abstract Interpretation

Jincheng Zhang

Quantum circuit verification is a critical yet notoriously challenging task in quantum computing. Full simulation of quantum circuits scales exponentially with the number of qubits and circuit depth, rendering it impractical for even moderately sized circuits. This paper proposes a novel approach to automated theorem proving for quantum circuit verification leveraging abstract interpretation. Our core idea is to approximate the behavior of quantum circuits using abstract interpretations, significantly reducing the computational complexity of the verification process. We outline a framework where abstract domains are constructed to represent the key properties of quantum circuits, such as qubit state fidelities and gate operations. The framework then employs logical reasoning and inference rules based on these abstract representations to automatically determine the correctness of a circuit against a given specification. We demonstrate the feasibility of this approach and discuss its potential to dramatically improve the efficiency and scalability of quantum circuit verification. The key benefit lies in shifting the verification burden from exact simulation to a more tractable abstract analysis.

•Sep 1, 2026•0 citations

Geometric Proof by Quantum Computation

Jincheng Zhang

This paper explores the application of quantum computation to revolutionize geometric proof. We propose a novel quantum algorithm designed to accelerate the verification of complex geometric theorems, moving beyond the limitations of classical methods. The core mechanism relies on quantum superposition and entanglement to represent and manipulate geometric shapes, enabling the efficient execution of intricate proofs. The research focuses on demonstrating the potential of this approach to significantly reduce computational time and increase the reliability of geometric theorems. The paper details the algorithm's design, mathematical foundations, and preliminary experimental results, highlighting the significant advantages offered by quantum computation in this domain.

•Sep 5, 2026•0 citations
Automated theorem proving, or more broadly automated reasoning, aims at using computer programs to automatically prove or disprove mathematical theorems and logical statements. It takes on an essential role across a vast array of applications and the quest for enhanced theorem-proving capabilities remains a prominent pursuit in artificial intelligence. Here, we propose a generic framework for quantum automated theorem proving, where the intrinsic quantum superposition and entanglement features would lead to potential advantages. In particular, we introduce quantum representations of knowledge bases and propose corresponding reasoning algorithms for a variety of tasks. We show how automated reasoning can be achieved with quantum resolution in both propositional and first-order logic with quadratically reduced query complexity. In addition, we propose the quantum algebraic proving method for geometric theorems, extending Wu's algebraic approach beyond the classical setting. Through concrete examples, including geometry problems from the International Mathematical Olympiad, we demonstrate how a quantum computer may prove geometric theorems with quadratic better query complexity. Our results establish a primary approach towards building quantum automatic theorem provers, which would be crucial for practical applications of both near-term and future quantum technologies.
This paper presents a novel approach to automated theorem proving specifically tailored for quantum circuit verification. The core idea is to construct a formal system that leverages logical reasoning and proof techniques to rigorously analyze quantum circuit designs. This system aims to identify errors and inconsistencies within the circuit, ensuring compliance with the fundamental principles of quantum mechanics. The proposed method moves beyond traditional circuit simulation, offering a mathematically sound guarantee of correctness. We detail the architecture of the theorem prover, focusing on the representation of quantum circuits and the application of proof strategies. The system utilizes a combination of techniques including logical deduction, model checking, and constraint solving, adapted for the unique characteristics of quantum computation. The paper outlines the key components of this system and highlights its potential to significantly improve the trustworthiness and reliability of quantum computing technologies. The central aim is to establish a robust framework for automated verification, reducing the risk of errors and accelerating the development of quantum software.
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.
In quantum information and computation research, symbolic methods have been widely used for human specification and reasoning about quantum states and operations. At the same time, they are essential for ensuring the scalability and efficiency of automated reasoning and verification tools for quantum algorithms and programs. However, a formal theory for symbolic specification and reasoning about quantum data and operations is still lacking, which significantly limits the practical applicability of automated verification techniques in quantum computing. In this paper, we present a general logical framework, called Symbolic Operator Logic SOL\mathbf{SOL}SOL, which enables symbolic specification and reasoning about quantum data and operations. Within this framework, a classical first-order logical language is embedded into a language of formal operators used to specify quantum data and operations, including their recursive definitions. This embedding allows reasoning about their properties modulo a chosen theory of the underlying classical data (e.g., Boolean algebra or group theory), thereby leveraging existing automated verification tools developed for classical computing. It should be emphasised that this embedding of classical first-order logic into SOL\mathbf{SOL}SOL is precisely what makes the symbolic method possible. We envision that this framework can provide a conceptual foundation for the formal verification and automated theorem proving of quantum computation and information in proof assistants such as Lean, Coq, and related systems.
This paper explores the potential of leveraging quantum entanglement to significantly accelerate symbolic reasoning and knowledge graph queries. Traditional symbolic reasoning methods often struggle with the inherent challenges of encoding and searching large amounts of logical information, leading to computational bottlenecks. We propose a novel approach that utilizes quantum entanglement to overcome these limitations. The core idea is to decompose symbolic logic problems into multiple entangled qubit sets. Through superposition and interference of these entangled states, parallel inference is enabled. Finally, quantum measurements yield the solution. This approach promises exponential speedups compared to classical methods, offering a fundamentally new paradigm for logical deduction and knowledge retrieval. The paper details the theoretical framework, outlining the key equations and mathematical representations underpinning the proposed methodology. We present a detailed model that incorporates the principles of quantum mechanics to accelerate the process of symbolic inference. This research contributes to the emerging field of quantum information science and its potential applications in artificial intelligence and knowledge management.
Quantum circuit verification is a critical yet notoriously challenging task in quantum computing. Full simulation of quantum circuits scales exponentially with the number of qubits and circuit depth, rendering it impractical for even moderately sized circuits. This paper proposes a novel approach to automated theorem proving for quantum circuit verification leveraging abstract interpretation. Our core idea is to approximate the behavior of quantum circuits using abstract interpretations, significantly reducing the computational complexity of the verification process. We outline a framework where abstract domains are constructed to represent the key properties of quantum circuits, such as qubit state fidelities and gate operations. The framework then employs logical reasoning and inference rules based on these abstract representations to automatically determine the correctness of a circuit against a given specification. We demonstrate the feasibility of this approach and discuss its potential to dramatically improve the efficiency and scalability of quantum circuit verification. The key benefit lies in shifting the verification burden from exact simulation to a more tractable abstract analysis.
This paper explores the application of quantum computation to revolutionize geometric proof. We propose a novel quantum algorithm designed to accelerate the verification of complex geometric theorems, moving beyond the limitations of classical methods. The core mechanism relies on quantum superposition and entanglement to represent and manipulate geometric shapes, enabling the efficient execution of intricate proofs. The research focuses on demonstrating the potential of this approach to significantly reduce computational time and increase the reliability of geometric theorems. The paper details the algorithm's design, mathematical foundations, and preliminary experimental results, highlighting the significant advantages offered by quantum computation in this domain.