2601.07953

# Quantum automated theorem proving **Authors**: Zheng-Zhi Sun, Qi Ye, Dong-Ling Deng > Center for Quantum Information, IIIS, Tsinghua University, Beijing 100084, China > Center for Quantum Information, IIIS, Tsinghua University, Beijing 100084, ChinaShanghai Qi Zhi Institute, Shanghai 200232, China > dldeng@tsinghua.edu.cnCenter for Quantum Information, IIIS, Tsinghua University, Beijing 100084, ChinaShanghai Qi Zhi Institute, Shanghai 200232, ChinaHefei National Laboratory, Hefei 230088, China 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. Automated theorem proving (ATP) lies at the heart of symbolic artificial intelligence, formal verification, and mathematical reasoning [24, 49]. Its goal is to mechanize logical inference: given a set of axioms or hypotheses, an ATP system determines—through sound and complete inference rules—whether a target conclusion follows. Over the past decades, ATP has become indispensable in domains ranging from hardware and software verification [34] to the formalization of modern mathematics, where machine-checked proofs now reach a level of rigor unattainable by human reasoning alone (e.g., the formalization of the four-color theorem and the Kepler conjecture) [26, 32]. Recent successes include the large-scale formal verification of sophisticated mathematical results [28] and the emergence of geometry solvers capable of handling Olympiad-level problems without human-provided demonstrations [70, 30, 38]. Despite these advances, ATP continues to face a fundamental scalability barrier. Logical inference—whether based on resolution, unification, or algebraic elimination—typically requires exploring a vast combinatorial search space [24, 49]. As the size of the knowledge base grows, the number of candidate inference steps increases rapidly, leading to severe time and memory costs. Even state-of-the-art systems that combine symbolic deduction with learned heuristics, such as neural-guided theorem provers and recent geometry engines, remain constrained by this underlying combinatorial explosion [70, 30, 38]. In practice, much of the computational effort in ATP is spent repeatedly searching for valid inference steps, filtering out invalid candidates, and performing algebraic manipulations whose cost grows polynomially or exponentially with problem size. *[Error downloading image: .//fig-qatp-sketch.pdf]* Figure 1: An illustration of quantum automated theorem proving. a, The badminton-basketball reasoning task expressed in natural language. The initial knowledge base in this case consists of ten sentences and the target is to infer whether Bob likes both badminton and basketball or not (see Supplementary Information Section II.B for details). b, The IMO 2008 Geometry Problem 1 diagram and statements. c, Left panel: first-order logic representation of the knowledge base for the badminton-basketball reasoning task; Right panel: algebraic expressions of the knowledge base for the IMO 2008 Geometry Problem 1. By using different encoding strategies, these knowledge bases expressed in formal languages are mapped into either quantum states or quantum circuits, depending on the specific task. d, Reasoning on a quantum computer. Quantum computing [54], grounded in the principles of quantum mechanics, would offer a fundamentally different computational paradigm for addressing these challenges. By exploiting quantum superposition and interference, quantum algorithms can evaluate many candidate solutions simultaneously and amplify the probability of desired outcomes. Landmark developments in quantum hardware—including programmable superconducting circuits [4, 75, 44, 43, 76, 41], trapped ions [23, 52], photonic systems [79, 50], and Rydberg-atom arrays [22, 9] —together with latest breakthroughs in quantum supremacy [4, 79, 75, 50] and quantum error correction [2, 67, 53, 9, 31, 27, 71, 45], are bringing quantum computation closer to the regime where nontrivial and noise-resilient algorithms can be executed reliably. Indeed, the interplay between quantum computing and machine learning has given rise to a new research frontier of quantum machine learning [8, 20, 17, 12, 46]. A variety of quantum learning algorithms with potential advantages have been proposed [33, 48, 21, 25, 47, 40] and some of them have been demonstrated in proof-of-principle experiments [35, 36, 37, 55]. These advances motivate the question of whether quantum resources can be harnessed not only for numerical computation or optimization, but also for symbolic reasoning. Here, we introduce quantum automated theorem proving (QATP): a general framework that integrates quantum algorithms with the core inference mechanisms of ATP while preserving the semantics of classical logic. Rather than replacing symbolic reasoning with heuristic optimization, QATP targets the dominant computational bottlenecks of theorem proving—namely, large-scale search, clause selection, and algebraic verification—by embedding them into quantum subroutines with provable performance guarantees. We develop quantum resolution algorithms for propositional and first-order logic that reduce the query complexity of inference, and we construct a quantum implementation of Wu’s method [73] for geometric theorem proving by reformulating polynomial manipulation and identity testing in a quantum-compatible form. Through concrete examples, including geometry problems from the International Mathematical Olympiad (IMO) [39], we demonstrate how a quantum computer may achieve ATP with quadratic improved query complexity. By connecting quantum algorithms with formal logic and algebraic proof systems, this work opens a pathway toward scalable, verifiable reasoning on quantum computers and establishes a bridge between quantum computation and symbolic artificial intelligence. *[Error downloading image: .//fig-qatp-propositional-logic.pdf]* Figure 2: Quantum resolution for propositional logic. a, Schematic overview of the quantum resolution procedure. For a given reasoning task, the knowledge base is expressed in propositional logic as a single sentence in conjunctive normal form, which is a conjunction of $M$ clauses. The quantum resolution process consists of four main steps. First, an appropriate encoding unitary $U_{\text{KB}}$ is constructed to load the classical knowledge base into quantum memory. Applying $U_{\text{KB}}$ to the initial state $|\mathbf{0}\rangle=|0·s 0\rangle$ prepares a many-body quantum state $|\Psi\rangle_{\text{KB}}$ that encodes the entire knowledge base. Second, we apply the quantum resolution unitary $U_{\text{R}}$ to calculate the resolution results for every propositional variable, and a verification circuit to identify valid resolvents with exactly one resolved variable (see Supplementary Information Section II.A), yielding the state $|\Psi\rangle_{\text{R}}$ . This state is a uniform superposition of $M^{2}$ components— $s$ of which correspond to valid clauses (state $\left|1\right\rangle$ on the last qubit) and the remaining $M^{2}-s$ to invalid ones (state $\left|0\right\rangle$ on the last qubit). Each clause after resolution is denoted as $L_{j}$ ( $j=1,...,M^{2}$ ). Third, amplitude amplification increases the probability of observing valid components from $s/M^{2}$ to $\Omega(1)$ . Finally, measuring the post-amplification state $|\Psi\rangle_{\text{A}}$ in the computational basis yields the $s$ valid clauses. If an empty clause is obtained, the reasoning process terminates and the target conclusion is derived. Otherwise, the newly generated clauses are added to the knowledge base, and the procedure is repeated until either an empty clause arises (the theorem is proved) or no new clause can be obtained (the theorem cannot be inferred). b, Quantum circuit implementing the encoding unitary $U_{\text{KB}}$ . This circuit consists of $M$ controlled subcircuits. Each subcircuit maps the state from $\left|\bf{0}\right\rangle$ on $N$ ququarts (bottom wire) to the state representing the $m$ -th clause, conditioned on the state $\left|m\right\rangle$ on the $k=\log_{2}M$ index qubits (top wire). c, Circuit representation of the quantum resolution unitary $U_{\text{R}}$ . This circuit resolves two variables $c_{1}$ and $c_{2}$ and outputs the resolution result $\mathcal{R}({c_{1}},{c_{2}})$ on the third ququart. d, Quantum circuit for amplitude amplification. Here, $H$ denotes the Hadamard gate, and $X$ and $Z$ represent the Pauli- $X$ and Pauli- $Z$ operators, respectively. The key idea is to entangle states corresponding to valid (invalid) clauses with state $\left|1\right\rangle$ ( $\left|0\right\rangle$ ) of the last qubit, and to amplify the amplitude of valid clauses. After $O(M/\sqrt{s})$ iterations, the probability of obtaining valid clauses is increased from $s/M^{2}$ to $\Omega(1)$ . Notations and the general framework We first introduce some basic notations and the general framework for QATP (Fig. 1). Classically, ATP establishes mathematical truths through a framework of formal logic [49]. This foundation comprises the syntax and semantics of logical languages, which together construct expressions that can be rigorously evaluated. These expressions populate a knowledge base, which is a repository of sentences in a formal language that enables precise inference. Key representation languages include propositional logic, which handles binary statements, and first-order logic, which extends this with quantifiers and predicates to model complex relationships. The core ATP process involves translating a conjecture into this formal framework and then systematically exploring its logical consequences by applying inference rules until the theorem is proven or refuted. In Fig. 1, we sketch the general pipeline for QATP. Suppose that we have a reasoning task, such as the badminton-basketball reasoning task (Fig. 1 a) or the IMO 2008 Geometry Problem 1 (Fig. 1 b), which is typically described in natural language. We first represent the knowledge base of the task in a formal language (Fig. 1 c). Using an appropriate encoding strategy, we map the knowledge base into a quantum state and prepare this state on a quantum computer. We then execute the reasoning quantum circuits, such as quantum resolution, on the prepared state. We measure the output states to deduce new valid sentences. If the obtained new sentences include the targeted conclusion, we terminate the process, and the conclusion is proved. Otherwise, we update the knowledge base with these new sentences and repeat the reasoning process until the conclusion is deduced or no new sentences can be obtained (Fig. 1 d). In the latter case, we conclude that the target conclusion cannot be deduced from the knowledge base if the inference algorithm used is complete. In the following, we give two concrete examples of quantum reasoning, one on quantum resolution in propositional and first-order logic, and the other that extends Wu’s method for proving geometric theorems into the quantum domain, to demonstrate how QATP would work and showcase potential advantages compared to their classical counterparts. Quantum resolution In classical ATP, one of the most fundamental and powerful inference rules is resolution [56, 58]. This rule is sound in both propositional and first-order logic, complete in propositional logic, and refutation-complete in first-order logic. It plays a central role in a wide range of applications. In this section, we introduce quantum resolution algorithms and explore their potential quantum advantages. To begin with, we first outline the basic principles and procedures underlying the use of resolution algorithms in ATP. The resolution method is typically used in a refutation-based manner [56, 58]: it seeks to derive a contradiction from the axioms together with the negation of the theorem to be proved, thus indirectly establishing the validity of the theorem. This process starts by transforming the logical statements into conjunctive normal form (CNF), which is a canonical format expressing formulas as conjunctions of disjunctions of literals. Once in CNF, the algorithm iteratively applies the resolution rule, selecting pairs of clauses and resolving their complementary literals to generate new clauses. The basic form of resolution for clauses in propositional logic is given by $$ \displaystyle{{{a_{1}}\vee\cdots\vee{a_{n}}\vee c,{b_{1}}\vee\cdots\vee{b_{m}}\vee\neg c}\over{{a_{1}}\vee\cdots\vee{a_{n}}\vee{b_{1}}\vee\cdots\vee{b_{m}}}}, \tag{1} $$ where $a_{i}$ , $b_{i}$ , and $c$ are literals, and the horizontal line denotes logical entailment. A literal is either a propositional variable or its negation—each representing a statement that can be true or false. The symbols $\vee$ , $\wedge$ , and $\neg$ are logical operators known as “disjunction”, “conjunction”, and “negation”, respectively. The resolution rule operates by eliminating complementary literals—that is, instances of the same propositional variable appearing with opposite polarities—and retaining the remaining literals from the two input clauses. A resolution step is valid only when exactly one such complementary pair is resolved. If the resulting clause is valid and not already present in the knowledge base, it is added to the knowledge base. This process continues iteratively until an empty clause representing the contradiction is derived, thus proving the original theorem. If no further resolutions are possible, the theorem cannot be inferred from the given knowledge base. Propositional resolution is a sound and complete inference method, making it a cornerstone of the classical automated theorem proving. It also serves as a canonical example for developing the quantum inference system introduced below. To introduce QATP within the framework of propositional logic (Fig. 2), we first represent the knowledge base as a many-body quantum state composed of four-level quantum systems (ququarts). Each ququart can be equivalently mapped onto a pair of standard qubits. For a clause involving $N$ propositional variables, we assign $N$ ququarts, where the state of each ququart encodes the status of its corresponding propositional variable—namely, absent, positive, negative, or resolved. The index of each ququart corresponds directly to that of the associated propositional variable. Since literals within a clause in CNF are implicitly connected by disjunctions, the disjunction symbols are omitted (Fig. 2 a). As an illustrative example, consider a knowledge base with four propositional variables $A$ , $B$ , $C$ , and $D$ . The clause $A\vee\neg C$ is represented by the quantum state $\left|1\right\rangle_{A}\left|0\right\rangle_{B}\left|2\right\rangle_{C}\left|0\right\rangle_{D}$ . In this encoding, $\left|1\right\rangle_{A}$ denotes the presence of the positive literal $A$ ; $\left|0\right\rangle_{B}$ and $\left|0\right\rangle_{D}$ represent the absence of $B$ and $D$ in the clause; and $\left|2\right\rangle_{C}$ corresponds to the negated literal $\neg C$ . The remaining basis state, $\left|3\right\rangle$ , is reserved to indicate the resolved status arising from the successful elimination of a pair of complementary literals during the resolution process. We further define a quantum circuit within this framework to implement the resolution process in our QATP approach. The quantum resolution circuit takes three input ququarts. Two ququarts, prepared in the states $|c_{1}\rangle$ and $|c_{2}\rangle$ , represent the premises of the resolution. These states encode the status (positive, negative, or absent) of a common propositional variable in their respective clauses. The third ququart is initialized in the state $|0\rangle$ and stores the resolution result produced by the circuit, as described by (Fig. 2 c) $$ \displaystyle{U_{\text{R}}}\left|{{c_{1}}}\right\rangle\left|{{c_{2}}}\right\rangle\left|0\right\rangle=\left|{{c_{1}}}\right\rangle\left|{{c_{2}}}\right\rangle\left|\mathcal{R}({c_{1}},{c_{2}})\right\rangle, \tag{2} $$ where $\mathcal{R}({c_{1}},{c_{2}})$ denotes the conclusion from resolving $c_{1}$ and $c_{2}$ . The circuit begins by identifying complementary literals in the two input clauses. When such a pair is detected, the circuit marks their successful resolution by setting the corresponding ququart to the state $|3\rangle$ . This state encodes the fact that the literals have been resolved, while all remaining ququarts preserve their previous values, reflecting the unaltered components of the clauses. Since this procedure can be executed in parallel across all propositional variables, the overall quantum circuit operates with a constant depth. By maintaining clause polarity and faithfully resolving complementary literals, the circuit accurately performs the quantum resolution operation, ensuring that the quantum-encoded logical structure undergoes the correct transformation. The detailed implementation of the quantum resolution unitary $U_{\text{R}}$ is provided in the Supplementary Information Fig. 1. In the classical ATP scenario, for a knowledge base containing $M$ clauses, the resolution inference requires evaluating every possible pairwise combination of clauses. This results in a query complexity of $O(M^{2})$ with respect to the knowledge base. In contrast, within our QATP framework, the unitary operator $U_{\text{KB}}$ (Fig. 2 b) is used to load the knowledge base into a quantum memory, after which the amplitude amplification subroutine (Fig. 2 d) increases the probability of observing valid resolution outcomes. Suppose that there are $s$ valid resolution results, where $s$ is an unknown but typically small integer. By employing the fixed-point quantum search algorithm [78], the QATP process requires only $O(M/\sqrt{s})$ queries to $U_{\text{KB}}$ . Considering that $O(s\log s)$ samples are needed to recover all the valid resulting clauses, the total query complexity becomes $O(M\sqrt{s}\log s)$ , yielding a quadratic speedup over its classical counterpart. We note that such a quadratic speedup has the same origin as Grover’s search algorithm [29]. In addition, we mention that propositional entailment is co-NP complete [58, 3], hence every known inference algorithm for propositional logic has a worst-case complexity that is exponential in the size of the input and quantum algorithms cannot solve all cases efficiently. The QATP framework can be extended to first-order logic in a conceptually straightforward manner. This extension proceeds by first transforming first-order sentences into clause form via Skolemization and conversion into CNF. A central part of this process is the elimination of existential quantifiers through Skolemization [56], which replaces each existential variable with a Skolem function or constant depending on the universally quantified variables in scope, while preserving satisfiability. The remaining universal quantifiers can then be removed, since variables in clause form are implicitly universally quantified. The resulting quantifier-free first-order clauses provide the basis for subsequent propositionalization. After this transformation, first-order reasoning can in principle be carried out using resolution. However, resolution in first-order logic typically requires an additional unification step, which is computationally expensive on classical computers [58] and poses significant challenges for direct quantum implementation. We circumvent this difficulty by invoking Herbrand’s theorem [58], which states that a set $W$ of clauses is unsatisfiable if and only if some finite subset of its Herbrand base $H_{W}(W)$ is unsatisfiable. Here, $H_{W}$ denotes the Herbrand universe of $W$ , consisting of all ground terms generated from the function and constant symbols appearing in $W$ . By working with ground instances drawn from the Herbrand universe, first-order reasoning is reduced to propositional reasoning, enabling the application of the QATP framework without requiring quantum unification. *[Error downloading image: .//fig-qp-unitary.pdf]* Figure 3: The quantum pseudo-division algorithm. We consider a general scenario of dividing a polynomial S by another polynomial T with respect to the variable $y$ . a, A sketch of ${U_{\text{S},y}}$ , which represents the coefficients of $y$ with varying degrees. The qubits that encode the variables $\bf{x}$ are omitted, and the state $\left|{\sum\limits_{\bf{i}}^{\bf{I}}{\text{s}({\bf{i}},d)\prod\limits_{k}^{\text{K}}{x_{k}^{{i_{k}}}}}}\right\rangle$ is abbreviated as $\left|{\text{s}({\bf{i}},d)}\right\rangle$ . b, A sketch of ${U_{\text{R},y}}$ that represents the remainder polynomial for S divided by T. Here, for simplicity, we write $\left|{\text{r}({\bf{i}},{\bf{j}},d)}\right\rangle$ as the abbreviation of $\left|{\sum\limits_{{\bf{i}},\bf{j}}^{\bf{I},\bf{J}}{\text{r}({\bf{i}},{\bf{j}},d)\prod\limits_{k}^{\text{K}}{x_{k}^{{i_{k}}+{j_{k}}}}}}\right\rangle$ . The number of qubits represented by $\left|\bf{0}\right\rangle$ in the red box is generally greater than the input state $\left|\bf{0}\right\rangle$ for ${U_{\text{R},y}}$ or ${U_{\text{T},y}}$ , because these qubits for ${U_{\text{R},y}}$ represent the product of the polynomials for the coefficients of S and T. The resulting polynomials usually have a higher degree. c, Basic arithmetic circuits used in the construction of ${U_{\text{R},y}}$ . The circuits $U_{+}$ , $U_{-}$ , and $U_{×}$ are designed to implement addition, subtraction, and multiplication of the input states, respectively. d, The quantum circuit for ${U_{\text{R},y}}$ that represents the remainder polynomial. The states in the red boxes are the input states and those in the green boxes are the output states of ${U_{\text{R},y}}$ . The key output $\left|{{\rm{r}}({\bf{i}},{\bf{j}},d)}\right\rangle=\left|{{\rm{s}}({\bf{i}},d){\rm{t}}({\bf{j}},{{\rm{D}}_{\rm{t}}})-{\rm{t}}({\bf{j}},d+{{\rm{D}}_{\rm{t}}}-{{\rm{D}}_{\rm{s}}}){\rm{s}}({\bf{i}},{{\rm{D}}_{\rm{s}}})}\right\rangle$ is obtained after the portion of the circuit preceding the blue dashed line is executed. The remaining qubits in the purple boxes serve as auxiliary qubits that can be prepared to the desired states (purple boxes) with one layer of single-qubit gates. These auxiliary qubits are reset after the state $\left|{\text{r}({\bf{i}},{\bf{j}},d)}\right\rangle$ is produced. QATP for geometric theorems We now discuss QATP for geometric theorems, with a focus on Wu’s method, which is a powerful and seminal algebraic approach to automated geometric theorem proving [15]. Instead of reasoning on geometric figures directly, Wu’s method encodes geometric conditions—such as incidences, parallels, or perpendicularities—into systems of polynomial equations defined over coordinate variables. The central task then becomes determining whether a set of hypothesis polynomials implies a conclusion polynomial. The core mechanism of Wu’s method involves polynomial pseudo-division and successive algebraic elimination, which systematically transform and reduce the polynomial system to a canonical form. If the final remainder polynomial vanishes identically after a sequence of reductions, the geometric theorem is thereby proved. Wu’s method has exerted a lasting influence on computer algebra and symbolic reasoning, forming the foundation of several modern systems for automated geometric theorem proving and computer-assisted proof verification. [14]. However, its computational complexity—dominated by high-degree polynomial manipulations—poses significant scalability challenges, motivating the exploration of potential quantum-enhanced implementations. *[Error downloading image: .//fig-qpp-2008p1b.pdf]* Figure 4: An illustration of QATP for an IMO geometry problem. a, The IMO 2008 Geometry Problem 1 in natural language. b, Coordinate assignment and hypothesis algebraic equations for this geometry problem. Without loss of generality, we assign the coordinates of the first point A as (0, 0), and those of the second point B as (0, $x_{4}$ ). This choice corresponds to setting $x_{1}=x_{2}=x_{3}=0$ . For simplicity, here we only explicitly show a small portion of the hypothesis algebraic equations. c, The triangular form of the hypothesis equations and one of the conclusion equation $g_{1}$ . d, Successive pseudo-division of the conclusion by the triangulated hypotheses. The variable with the largest subscript in the conclusion is $x_{22}$ , which is removed in the first pseudo-division using $h_{16}$ . The last pseudo-remainder $R_{6}$ is zero, proving the validity of the conclusion $g_{1}$ . The number of monomials in the pseudo-remainders determines the computational time and space required for a given proof, potentially being very large for certain cases [73, 15]. For this particular problem, the largest number is 16172. e, A sketch of the quantum circuit for pseudo-division of the conclusion polynomial $g_{1}$ by $h_{16}$ . This circuit involves two copies of the circuit representing $g_{1}$ and two copies of the circuit representing $h_{16}$ , together with an arithmetic circuit required to perform pseudo-division. f, Quantum gates used in representing polynomials with quantum circuits. g, The quantum circuit for representing $h_{16}$ with seven qubits. This circuit calculates the coefficients of $h_{16}$ in variable $x_{22}$ . We first perform quantum Fourier transform on the output qubits, and then use controlled phase gates to add phases determined by the value of the input variables and the degree of the variable being eliminated. The last step is to revert the phase of the quantum state back to the binary representation on the qubits. We use the circuit for $h_{16}$ on seven qubits in this figure as a simple demonstration. The complete circuits of $h_{16}$ employed in the first step of quantum pseudo-division in fact requires more qubits to represent $x_{4}$ , $x_{20}$ , the exponent of $x_{22}$ , and the output. It involves 28 qubits and has a depth of 89, which is too complicated for clear visualization. To extend Wu’s method into the quantum domain, a crucial step is to implement polynomial pseudo-division on a quantum computer. To achieve this, we first need to find an appropriate representation for encoding polynomials in quantum form. A straightforward approach exploits quantum state encoding of polynomial coefficients. The polynomial is represented as an entangled quantum state, with each component corresponding to a single coefficient (see Supplementary Information Section III.B for details). However, this approach faces a number of challenges. First, polynomial multiplication and subtraction required in pseudo-division involve arithmetic operations on coefficients. Although basic integer arithmetic can be efficiently performed using quantum Fourier transform–based algorithms [57], the task of combining like terms in polynomial multiplication remains cumbersome. This difficulty arises because, under the quantum superposition principle, the coefficients of a polynomial are encoded across multiple superposed states on the same qubits. Comparing degrees and merging coefficients of equal degree fall beyond the scope of standard quantum arithmetic algorithms [69]. Second, combining like terms is inherently irreversible, further complicating its quantum implementation. Third, the quantum no-cloning theorem [72] forbids the duplication of arbitrary unknown quantum states, preventing the direct reuse of the resulting quantum state from one pseudo-division step as input to the next. Finally, after each pseudo-division step, the resulting state becomes highly entangled with the input polynomial states, complicating subsequent operations and rendering the overall process highly intricate and resource-intensive. We overcome these difficulties by introducing a quantum pseudo-division algorithm based on circuit encoding of the point-value representation of polynomials (Fig. 3). In such a representation, a polynomial $\text{F}(\mathbf{x})$ is represented by $M$ point-value pairs $\{\mathbf{x},\text{F}(\mathbf{x})\}$ , where $\mathbf{x}=(x_{1},x_{2},·s,x_{\text{K}})$ denotes the variables. With this representation, algebraic operations of polynomials reduce to operations on corresponding point-value pairs, thus circumventing the first and second challenges faced by the quantum state encoding approach discussed above. In the quantum scenario, these $M$ point-value pairs are further encoded into a quantum state $|\psi{\rangle_{\rm{F}}}=\sum\nolimits_{m}^{M}{\left|{{{\bf{x}}_{m}}}\right\rangle\left|{{\rm{F}}({{\bf{x}}_{m}})}\right\rangle}$ , which in turn can be prepared by a unitary $U_{\text{F}}$ specified by a quantum circuit with a depth scaling linearly with $M$ : $$ \displaystyle{U_{\text{F}}}\left|{\bf{x}}\right\rangle{\left|\bf{0}\right\rangle}=\left|{\bf{x}}\right\rangle\left|{\text{F}({\bf{x}})}\right\rangle. \tag{3} $$ In this way, each polynomial is represented by a unitary implemented by a quantum circuit. This representation allows cloning of the polynomial, and reduces pseudo-division to the construction of the quantum circuit for the remainder polynomial (Fig. 3 b,d). More concretely, we consider dividing polynomial ${\rm{S}}=\sum\limits_{{\bf{i}},{d_{1}}}^{{\bf{I}},{{\rm{D}}_{\rm{s}}}}{{\rm{s}}({\bf{i}},{d_{1}})\prod\limits_{k}^{\rm{K}}{x_{k}^{{i_{k}}}}{y^{{d_{1}}}}}$ by ${\rm{T}}=\sum\limits_{{\bf{j}},{d_{2}}}^{{\bf{J}},{{\rm{D}}_{\rm{t}}}}{{\rm{t}}\left({{\bf{j}},{d_{2}}}\right)\prod\limits_{k}^{\rm{K}}{x_{k}^{{j_{k}}}}{y^{{d_{2}}}}}$ with respect to the variable $y$ . Here, $\text{s}({\bf{i}},{d_{1}})$ and $\text{t}({{\bf{j}},{d_{2}}})$ represent the coefficients with $\mathbf{i}\equiv(i_{1},i_{2},·s,i_{\text{K}})$ and $\mathbf{j}\equiv(j_{1},j_{2},·s,j_{\text{K}})$ denoting collectively the exponents of corresponding variables; the maximum degrees of these two polynomials in the variables $x_{k}$ and $y$ are denoted as $\text{I}_{k}$ , $\text{J}_{k}$ , $\text{D}_{\text{s}}$ , and $\text{D}_{\text{t}}$ , respectively. Without loss of generality, we suppose ${{\rm{D}}_{\rm{s}}}>{{\rm{D}}_{\rm{t}}}$ . In order to obtain the remainder polynomial for S divided by T with respect to $y$ , a crucial subroutine involves computing the coefficient of variable $y$ with varying degrees. Those coefficients are themselves polynomials in variables $\bf{x}$ , which in turn can be represented by a unitary $U_{\text{S},y}$ (Fig. 3 a): $$ \displaystyle{U_{\text{S},y}}\left|d\right\rangle\left|{\bf{x}}\right\rangle\left|{\bf{0}}\right\rangle=\left|d\right\rangle\left|{\bf{x}}\right\rangle\left|{\sum\limits_{\bf{i}}^{\bf{I}}{\text{s}({\bf{i}},d)\prod\limits_{k}^{\text{K}}{x_{k}^{{i_{k}}}}}}\right\rangle. \tag{4} $$ Here, $\sum\limits_{\bf{i}}^{\bf{I}}{\text{s}({\bf{i}},{d})\prod\limits_{k}^{\text{K}}{x_{k}^{{i_{k}}}}}$ denotes the coefficient of $y^{d}$ in S. An illustration of our quantum pseudo-division algorithm is shown in Fig. 3. With this quantum pseudo-division algorithm, the general procedure for proving geometric theorems with a quantum computer is now straightforward and consists of the following major steps: Step $1$ , for a given geometric theorem proving problem, we translate it into a series of algebraic equations, yielding a set of hypothesis equations and another set of conclusion equations; Step $2$ , we transform the set of hypotheses equations into the triangular form by using the quantum pseudo-division algorithm repeatedly; Step $3$ , for each conclusion equation, we perform successive pseudo-division on the transformed hypotheses in triangular form to obtain the final remainder; Step $4$ , we measure the final state to check whether the final remainder is zero. If it is, the corresponding conclusion is then proved. We mention that step $2$ and $3$ can be implemented with a unified quantum circuit and one only needs to measure at the step $4$ (Supplementary Information Section III.C). As an illustrative example, we now apply our general protocol for proving geometric theorems to the IMO 2008 Geometry Problem 1 (Fig. 4 a) [39, 70, 66]. In Fig. 4 b, we present a diagram for the IMO problem in the coordinate plane and translate the hypotheses of the problem into algebraic equations. We then triangulate these hypotheses through pseudo-divisions so that each subsequent hypothesis equation introduces only one new variable (Fig. 4 c). We prove the conclusion by successively eliminating variables through pseudo-division, starting with the variable with the largest subscript and the last hypothesis polynomial. More concretely, we start by dividing the conclusion polynomial $g_{1}$ by $h_{16}$ with respect to $x_{22}$ , leading to a pseudo-remainder which is further divided by $h_{15}$ to remove $x_{21}$ . We repeat these steps and find that the final pseudo-remainder $R_{6}$ for dividing $R_{7}$ by $h_{1}$ with respect to $x_{6}$ is zero (Fig. 4 d), thus proving the conclusion $g_{1}$ . The key subroutine for executing quantum pseudo-division is implemented by constructing the pseudo-remainder circuit from circuits representing the dividend and divisor, as illustrated in Fig. 4 e. The resulting polynomial is represented by the circuit $U_{\text{R}}$ , which incorporates two copies of the circuit corresponding to the conclusion $g_{1}$ , two copies of the circuit for the divisor $h_{16}$ , and additional arithmetic subcircuits that realize the pseudo-division operations as shown in Fig. 3 d. For the demonstration of the quantum implementation of pseudo-division, we present a scheme for constructing a circuit that represents a multivariate polynomial as a univariate polynomial with respect to a chosen variable ( $x_{22}$ in this case), where the circuit depth scales linearly with the number of nonzero terms. A general framework for circuit construction is provided later in this section. As shown in Fig. 4 g, we illustrate the construction for the polynomial $h_{16}$ implemented on seven qubits. Since $h_{16}$ serves as the divisor for eliminating the variable $x_{22}$ , it can be expressed as $h_{16}=1· x_{22}^{1}+(x_{20}-x_{4})· x_{22}^{0}$ . In this circuit, the first two qubits encode the respective values of $x_{4}$ and $x_{20}$ , while the next two qubits represent the exponent of $x_{22}$ . Although the exponent of $x_{22}$ in $h_{16}$ is either 0 or 1, two qubits are required to accommodate the binary representation of “2” (i.e., “10”), as $h_{16}$ is multiplied by $x_{22}$ during the division of the conclusion $g_{1}$ . The remaining three qubits encode the coefficient values of $h_{16}$ in $x_{22}$ for different exponents, together with the input values of $x_{4}$ and $x_{20}$ . We apply a quantum Fourier transform to the three output qubits initially in the state $\left|\mathbf{0}\right\rangle$ , producing the uniform superposition $\frac{1}{\sqrt{8}}\sum_{k=0}^{7}\left|k\right\rangle$ . To compute all monomials in $h_{16}$ , controlled phase-shift gates are applied to the output qubits, conditioned on the qubits encoding $x_{20}$ , $x_{4}$ , and the exponent of $x_{22}$ . After executing all controlled operations, the output qubits evolve to the state $\sum_{k}\frac{e^{\pi ik(x_{20}-x_{4})/4}}{2\sqrt{2}}\left|k\right\rangle$ if the exponent of $x_{22}$ is 0, or to $\sum_{k}\frac{e^{\pi ik/4}}{2\sqrt{2}}\left|k\right\rangle$ if the exponent is 1. Subsequently, an inverse quantum Fourier transform is applied to recover the binary-encoded coefficients of $h_{16}$ as functions of $x_{22}$ . The complete circuits used for the first step of quantum pseudo-division employ 28 qubits, with circuit depths of 4068 for the conclusion $g_{1}$ and 89 for $h_{16}$ . Notably, in each quantum pseudo-division step, the resulting circuit is constructed directly from those of the dividend and divisor (as depicted in Fig. 4 e), implying that its depth is independent of the number of monomials. This contrasts with the classical implementation of Wu’s method that operates on coefficient representations of polynomials [77], where both space and time complexity increase sharply as the number of monomials grows across successive pseudo-remainders during the proof process. We now analyze the complexity of implementing Wu’s method on a quantum computer. We focus on two aspects: (i) the gate complexity required to encode multivariate polynomials and perform arithmetic operations on them, and (ii) the query complexity associated with polynomial identity testing (PIT) [65, 59, 60], namely determining whether the final pseudo-remainder is identically zero or not. As discussed above, within the framework for quantum implementation of geometric theorem proving, the overall workflow decomposes into three fundamental subroutines, whose complexities are analyzed one-by-one in the following. The first subroutine concerns the construction of quantum circuits that encode the hypothesis polynomials. We outline two strategies for this task. One approach is to classically evaluate a polynomial at $M$ input points, thereby generating $M$ point–value pairs, which are subsequently loaded into a quantum circuit. This yields a circuit depth of $O(M\log M)$ , analogous to the knowledge-base encoding unitary $U_{\text{KB}}$ shown in Fig. 2 b. Here, $M$ is determined by the number of evaluation points required in the final PIT stage. An alternative strategy is to construct the polynomial circuit directly from its algebraic structure, explicitly encoding each monomial and summing them coherently. As illustrated in Fig. 4 g, a polynomial with $M$ nonzero monomials gives rise to a circuit whose depth scales linearly with $M$ . The gate complexity associated with generating a single monomial is analyzed in the Supplementary Information Section III.C. This direct construction allows full freedom in selecting the number of point–value evaluations used later in PIT. Importantly, the overhead of building the hypothesis circuits is modest, as this step is performed only once at the outset of the proof protocol. Moreover, in typical geometric reasoning tasks, the hypothesis polynomials are substantially simpler than the intermediate polynomials generated during subsequent proof derivations. The second subroutine constructs a circuit that represents a polynomial with respect to a chosen division variable. This task can be formulated as an interpolation problem: given a circuit $U_{\text{S}}$ that evaluates a multivariate polynomial S, the objective is to construct a circuit $U_{\text{S},y}$ that outputs the coefficients of S corresponding to different powers of the variable $y$ . Classical algorithms typically implement this step using the fast Fourier transform (FFT) [16, 61, 10]. While such reversible classical procedures can, in principle, be translated into quantum circuits [54], we instead adopt Kravchuk polynomials [68] as the interpolation basis. This choice avoids the substantial overhead associated with complex-valued floating-point arithmetic in FFT-based methods. The resulting construction requires ${{\rm{D}}_{\rm{s}}}$ queries to $U_{\text{S}}$ , matching the query complexity of the classical FFT approach in polynomial interpolation, while the depth of the remaining operations scales as $O({{\rm{D}}_{\rm{s}}}\log{{\rm{D}}_{\rm{s}}})$ when suitable ancillary qubits are available. Additional details are provided in the Supplementary Information Section III.C. The third subroutine comprises the quantum arithmetic circuits required to implement pseudo-division. This component consists of integer addition, subtraction, and multiplication modules, as illustrated in Fig. 3 d. The circuit depth of these arithmetic operations scales polynomially with the number of qubits involved [57]. In practice, this cost is insignificant compared with the depth of the circuits encoding the polynomials themselves. In particular, encoding $M$ evaluation points requires only $\log_{2}M$ qubits to represent the evaluation domain. After constructing the circuit that computes the final pseudo-remainder, the remaining task is to determine whether this circuit represents the zero polynomial. This is achieved by evaluating the polynomial on a finite set G of points and checking whether it vanishes on all elements of G. A fixed-point quantum search algorithm [78] can be employed to search for points at which the polynomial evaluates to a nonzero value. Specifically, if there are $h$ points in G at which the polynomial is nonzero, then $O(\log(2/\delta)\sqrt{|\text{G}|/h})$ queries to the quantum evaluation circuit suffice to achieve a success probability of $1-\delta^{2}$ . By contrast, a classical randomized strategy based on independent sampling with replacement requires $O(\log(1/\delta)|\text{G}|/h)$ queries to reach the same confidence level in the regime where $h$ is small. This yields a quadratic speedup with respect to the size of the evaluation set $|\text{G}|$ . Discussion and outlook In summary, we have introduced a general QATP framework that applies quantum computation to accelerate core inference procedures in classical automated reasoning. By developing quantum implementations of the resolution method for propositional and first-order logic, as well as a quantum formulation of Wu’s method for geometric theorem proving, we have shown that established symbolic reasoning paradigms can be embedded into quantum computational paradigms without modifying their logical foundations. For propositional and first-order logic, our quantum resolution procedure achieves a quadratic speedup in query complexity for identifying valid resolvents by replacing classical exhaustive search with quantum search. This speedup is optimal for unstructured search problems and aligns with known lower bounds in the quantum query model [5, 1]. For geometric theorem proving, we reformulated Wu’s method as an quantum algebraic reasoning process based on polynomial pseudo-division, reducing proof verification to polynomial identity testing. Quantum circuits enable the coherent evaluation of polynomials at multiple points via superposition, and quantum search yields an overall quadratic advantage in detecting nonzero evaluations. A circuit realization for the 2008 IMO Geometry Problem 1 demonstrates the feasibility of end-to-end geometric proofs within this framework. More broadly, our work represents an primary step toward the systematic adaptation of automated theorem proving to the quantum domain. The quantum reasoning procedures introduced here evaluate the validity of a conclusion given access to a knowledge base or a set of geometric relations and can be rigorously analyzed within the quantum decision-tree (query) model. In this setting, QATP naturally appears as a search problem—for example, searching for a contradiction in resolution or for nonzero evaluations in PIT—while also fitting into the broader framework of total Boolean function evaluation [11, 1]. For such functions, the bounded-error quantum query complexity is lower bounded by the sixth root of the classical deterministic query complexity [5, 1]. Within this theoretical landscape, our approach achieves a quadratic separation, matching the largest separation currently known for unstructured problems and enabled by quantum search techniques [29, 6]. We also investigated quantum circuit constructions for representing and manipulating multivariate polynomials, which are central to algebraic methods for geometric reasoning. Although the quantum circuit model is universal [19, 7, 13], implementing an arbitrary $n$ -bit reversible function can still require $\Omega(n2^{n}/\log n)$ elementary gates in the worst case [64, 74]. Our focus therefore lies on the structured algebraic operations arising in Wu’s method. In particular, we developed quantum circuit constructions for polynomial pseudo-division and employed Kravchuk polynomials as an interpolation basis over integer-valued domains, thereby avoiding costly complex-valued floating-point arithmetic and enabling efficient circuit realizations. These techniques allow multivariate polynomials to be manipulated coherently and integrated into end-to-end quantum geometric proofs. While evaluating polynomial values may appear straightforward, the algebraic transformations required in geometric theorem proving—such as pseudo-division, interpolation, and successive elimination—introduce substantial structural complexity. Understanding how these structured operations interact with quantum resources remains an open problem. An important direction for future work is to identify restricted classes of geometric constraints whose algebraic structure may admit stronger quantum advantages, potentially exceeding quadratic speedups. Looking forward, it would be interesting and important to carry out experimental demonstrations of quantum automated reasoning with current noisy or early fault-tolerant quantum devices. This would be a crucial step toward practical applications of quantum technologies in symbolic artificial intelligence. Acknowledgements We thank X. Gao, A. Anshu, P. H. Yao, X. Sun, W. J. Jiang, W. K. Li, X.-S. Gao, M. Ying, and L.-M. Duan for enlightening discussions. This work is supported by the National Natural Science Foundation of China (Grant No. T2225008 and T24B2002), the Innovation Program for Quantum Science and Technology (Grant No. 2021ZD0302203), the Tsinghua University Dushi Program, and the Shanghai Qi Zhi Institute Innovation Program SQZ202318. Z.-Z. S. is additionally funded by China Postdoctoral Science Foundation (Certificated Number: 2025T180926). References - [1] S. Aaronson and A. Ambainis (2014) The need for structure in quantum speedups. Theory Comput. 10 (1), pp. 133–166. External Links: ISSN 1557-2862, Document Cited by: Quantum automated theorem proving, Quantum automated theorem proving. - [2] R. Acharya, I. Aleiner, R. Allen, T. I. Andersen, M. Ansmann, F. Arute, K. Arya, A. Asfaw, J. Atalaya, R. Babbush, et al. (2023-02) Suppressing quantum errors by scaling a surface code logical qubit. Nature 614 (7949), pp. 676–681. External Links: ISSN 1476-4687, Document Cited by: Quantum automated theorem proving. - [3] S. Arora (2009) Computational complexity. Cambridge University Press, Cambridge, UK. External Links: ISBN 9780521424264 Cited by: Quantum automated theorem proving. - [4] F. Arute, K. Arya, R. Babbush, D. Bacon, J. C. Bardin, R. Barends, R. Biswas, S. Boixo, F. G. S. L. Brandao, D. A. Buell, et al. (2019-10) Quantum supremacy using a programmable superconducting processor. Nature 574 (7779), pp. 505–510. External Links: ISSN 1476-4687, Document Cited by: Quantum automated theorem proving. - [5] R. Beals, H. Buhrman, R. Cleve, M. Mosca, and R. de Wolf (2001-07) Quantum lower bounds by polynomials. J. ACM 48 (4), pp. 778–797. External Links: ISSN 1557-735X, Document Cited by: Quantum automated theorem proving, Quantum automated theorem proving. - [6] C. H. Bennett, E. Bernstein, G. Brassard, and U. Vazirani (1997-10) Strengths and weaknesses of quantum computing. SIAM J. Comput. 26 (5), pp. 1510–1523. External Links: ISSN 1095-7111, Document Cited by: Quantum automated theorem proving. - [7] E. Bernstein and U. Vazirani (1993) Quantum complexity theory. In Proceedings of the Twenty-Fifth Annual ACM Symposium on Theory of Computing, STOC ’93, pp. 11–20. External Links: Document, ISBN 0897915917, Link Cited by: Quantum automated theorem proving. - [8] J. Biamonte, P. Wittek, N. Pancotti, P. Rebentrost, N. Wiebe, and S. Lloyd (2017-09) Quantum machine learning. Nature 549 (7671), pp. 195–202. External Links: Document Cited by: Quantum automated theorem proving. - [9] D. Bluvstein, S. J. Evered, A. A. Geim, S. H. Li, H. Zhou, T. Manovitz, S. Ebadi, M. Cain, M. Kalinowski, D. Hangleiter, et al. (2024) Logical quantum processor based on reconfigurable atom arrays. Nature 626 (7997), pp. 58–65. External Links: ISSN 1476-4687, Document Cited by: Quantum automated theorem proving. - [10] A. Borodin and R. Moenck (1974-06) Fast modular transforms. J. Comput. Syst. Sci. 8 (3), pp. 366–386. External Links: ISSN 0022-0000, Document Cited by: Quantum automated theorem proving. - [11] H. Buhrman and R. de Wolf (2002-10) Complexity measures and decision tree complexity: a survey. Theor. Comput. Sci. 288 (1), pp. 21–43. External Links: ISSN 0304-3975, Document Cited by: Quantum automated theorem proving. - [12] M. Cerezo, G. Verdon, H. Huang, L. Cincio, and P. J. Coles (2022-09) Challenges and opportunities in quantum machine learning. Nat. Comput. Sci. 2 (9), pp. 567–576. External Links: Document Cited by: Quantum automated theorem proving. - [13] A. Chi-Chih Yao (1993) Quantum circuit complexity. In Proceedings of 1993 IEEE 34th Annual Foundations of Computer Science, SFCS-93, pp. 352–361. External Links: Document Cited by: Quantum automated theorem proving. - [14] S. Chou, X. Gao, and J. Zhang (1994) Machine proofs in geometry: automated production of readable proofs for geometry theorems. World Scientific, Singapore. Cited by: Quantum automated theorem proving. - [15] S. Chou (1988-09) An introduction to Wu's method for mechanical theorem proving in geometry. J. Autom. Reasoning 4 (3), pp. 237–267. External Links: Document Cited by: Figure 4, §III.1, §III.1, §III.1, §III.1, §III, Quantum automated theorem proving. - [16] J. W. Cooley and J. W. Tukey (1965) An algorithm for the machine calculation of complex fourier series. Math. Comput. 19 (90), pp. 297–301. External Links: ISSN 1088-6842, Document Cited by: Quantum automated theorem proving. - [17] S. Das Sarma, D. Deng, and L. Duan (2019-03) Machine learning meets quantum physics. Phys. Today 72 (3), pp. 48–54. External Links: Document Cited by: Quantum automated theorem proving. - [18] R. A. Demillo and R. J. Lipton (1978-06) A probabilistic remark on algebraic program testing. Inf. Process. Lett. 7 (4), pp. 193–195. External Links: ISSN 0020-0190, Document Cited by: §IV, §IV. - [19] D. Deutsch and R. Penrose (1985) Quantum theory, the church–turing principle and the universal quantum computer. Proc. R. Soc. Lond. A 400 (1818), pp. 97–117. External Links: Document, Link Cited by: Quantum automated theorem proving. - [20] V. Dunjko and H. J. Briegel (2018-06) Machine learning & artificial intelligence in the quantum domain: a review of recent progress. Rep. Prog. Phys. 81 (7), pp. 074001. External Links: Document Cited by: Quantum automated theorem proving. - [21] V. Dunjko, J. M. Taylor, and H. J. Briegel (2016-09) Quantum-enhanced machine learning. Phys. Rev. Lett. 117, pp. 130501. External Links: Document, Link Cited by: Quantum automated theorem proving. - [22] S. Ebadi, T. T. Wang, H. Levine, A. Keesling, G. Semeghini, A. Omran, D. Bluvstein, R. Samajdar, H. Pichler, W. W. Ho, et al. (2021-07) Quantum phases of matter on a 256-atom programmable quantum simulator. Nature 595 (7866), pp. 227–232. External Links: ISSN 1476-4687, Document Cited by: Quantum automated theorem proving. - [23] L. Egan, D. M. Debroy, C. Noel, A. Risinger, D. Zhu, D. Biswas, M. Newman, M. Li, K. R. Brown, M. Cetina, and C. Monroe (2021-10) Fault-tolerant control of an error-corrected qubit. Nature 598 (7880), pp. 281–286. External Links: ISSN 1476-4687, Document Cited by: Quantum automated theorem proving. - [24] M. Fitting (2013) First-order logic and automated theorem proving. Springer New York. Cited by: §II.2, Quantum automated theorem proving, Quantum automated theorem proving. - [25] X. Gao, Z.-Y. Zhang, and L.-M. Duan (2018-12) A quantum machine learning algorithm based on generative models. Sci. Adv. 4 (12), pp. eaat9004. External Links: Document Cited by: Quantum automated theorem proving. - [26] G. Gonthier (2008) Formal proof–the four-color theorem. Notices of the AMS 55 (11), pp. 1382–1393. Cited by: Quantum automated theorem proving. - [27] Google Quantum AI et al. (2025-02-01) Quantum error correction below the surface code threshold. Nature 638 (8052), pp. 920–926. External Links: ISSN 1476-4687, Document, Link Cited by: Quantum automated theorem proving. - [28] W. T. Gowers, B. Green, F. Manners, and T. Tao (2025) On a conjecture of marton. Ann. of Math. 201 (2), pp. 515–549. External Links: Link, Document Cited by: Quantum automated theorem proving. - [29] L. K. Grover (1996) A fast quantum mechanical algorithm for database search. In Proceedings of the Twenty-Eighth Annual ACM Symposium on Theory of Computing, STOC ’96, pp. 212–219. External Links: ISBN 0897917855, Link, Document Cited by: Quantum automated theorem proving, Quantum automated theorem proving. - [30] D. Guo, D. Yang, H. Zhang, J. Song, P. Wang, Q. Zhu, R. Xu, R. Zhang, S. Ma, X. Bi, et al. (2025) Deepseek-r1 incentivizes reasoning in llms through reinforcement learning. Nature 645 (8081), pp. 633–638. External Links: Link, Document Cited by: Quantum automated theorem proving, Quantum automated theorem proving. - [31] R. S. Gupta, N. Sundaresan, T. Alexander, C. J. Wood, S. T. Merkel, M. B. Healy, M. Hillenbrand, T. Jochym-O’Connor, J. R. Wootton, T. J. Yoder, et al. (2024) Encoding a magic state with beyond break-even fidelity. Nature 625 (7994), pp. 259–263. External Links: ISSN 0028-0836, 1476-4687, Document Cited by: Quantum automated theorem proving. - [32] T. Hales, M. Adams, G. Bauer, T. D. Dang, J. Harrison, L. T. Hoang, C. Kaliszyk, V. Magron, S. McLaughlin, T. T. Nguyen, Q. T. Nguyen, T. Nipkow, S. Obua, J. Pleso, J. Rute, A. Solovyev, T. H. A. Ta, N. T. Tran, T. D. Trieu, J. Urban, K. Vu, and R. Zumkeller (2017) A formal proof of the kepler conjecture. Forum Math. Pi 5, pp. e2. External Links: ISSN 2050-5086, Document Cited by: Quantum automated theorem proving. - [33] A. W. Harrow, A. Hassidim, and S. Lloyd (2009-10) Quantum Algorithm for Linear Systems of Equations. Phys. Rev. Lett. 103 (15), pp. 150502. External Links: Document Cited by: Quantum automated theorem proving. - [34] O. Hasan and S. Tahar (2015) Formal verification methods. In Encyclopedia of Information Science and Technology, Third Edition, pp. 7162–7170. Cited by: Quantum automated theorem proving. - [35] V. Havlíček, A. D. Córcoles, K. Temme, A. W. Harrow, A. Kandala, J. M. Chow, and J. M. Gambetta (2019-03) Supervised learning with quantum-enhanced feature spaces. Nature 567 (7747), pp. 209–212. External Links: Document Cited by: Quantum automated theorem proving. - [36] L. Hu, S. Wu, W. Cai, Y. Ma, X. Mu, Y. Xu, H. Wang, Y. Song, D. Deng, C. Zou, and L. Sun (2019-01) Quantum generative adversarial learning in a superconducting quantum circuit. Sci. Adv. 5 (1), pp. eaav2761. External Links: Document Cited by: Quantum automated theorem proving. - [37] H. Huang, M. Broughton, J. Cotler, S. Chen, J. Li, M. Mohseni, H. Neven, R. Babbush, R. Kueng, J. Preskill, et al. (2022) Quantum advantage in learning from experiments. Science 376 (6598), pp. 1182–1186. External Links: Link, Document Cited by: Quantum automated theorem proving. - [38] T. Hubert, R. Mehta, L. Sartran, M. Z. Horváth, G. Žužić, E. Wieser, A. Huang, J. Schrittwieser, Y. Schroecker, H. Masoom, et al. (2025) Olympiad-level formal mathematical reasoning with reinforcement learning. Nature. External Links: Document Cited by: Quantum automated theorem proving, Quantum automated theorem proving. - [39] (2025) International mathematical olympiad. Note: https://www.imo-official.org Accessed: 2026-01-12 Cited by: Quantum automated theorem proving, Quantum automated theorem proving. - [40] S. Jerbi, L. J. Fiderer, H. Poulsen Nautrup, J. M. Kübler, H. J. Briegel, and V. Dunjko (2023-01) Quantum machine learning beyond kernel methods. Nat. Commun. 14 (1), pp. 517. External Links: Document Cited by: Quantum automated theorem proving. - [41] F. Jin, S. Jiang, X. Zhu, Z. Bao, F. Shen, K. Wang, Z. Zhu, S. Xu, Z. Song, J. Chen, et al. (2025) Topological prethermal strong zero modes on superconducting processors. Nature 645 (8081), pp. 626–632. External Links: Document Cited by: Quantum automated theorem proving. - [42] V. Kabanets and R. Impagliazzo (2003) Derandomizing polynomial identity tests means proving circuit lower bounds. In Proceedings of the Thirty-Fifth Annual ACM Symposium on Theory of Computing, STOC ’03, pp. 355–364. External Links: Document Cited by: §IV, §IV. - [43] Y. Kim, A. Eddins, S. Anand, K. X. Wei, E. van den Berg, S. Rosenblatt, H. Nayfeh, Y. Wu, M. Zaletel, K. Temme, and A. Kandala (2023-06) Evidence for the utility of quantum computing before fault tolerance. Nature 618 (7965), pp. 500–505. External Links: ISSN 1476-4687, Document Cited by: Quantum automated theorem proving. - [44] S. Krinner, N. Lacroix, A. Remm, A. Di Paolo, E. Genois, C. Leroux, C. Hellings, S. Lazar, F. Swiadek, J. Herrmann, et al. (2022-05) Realizing repeated quantum error correction in a distance-three surface code. Nature 605 (7911), pp. 669–674. External Links: ISSN 1476-4687, Document Cited by: Quantum automated theorem proving. - [45] N. Lacroix, A. Bourassa, F. J. Heras, L. M. Zhang, J. Bausch, A. W. Senior, T. Edlich, N. Shutty, V. Sivak, A. Bengtsson, et al. (2025) Scaling and logic in the color code on a superconducting quantum processor. Nature 645, pp. 614. External Links: Document Cited by: Quantum automated theorem proving. - [46] W. Li, Y. Ma, and D. Deng (2025) Pitfalls and prospects of quantum machine learning. Nat. Comput. Sci. 5, pp. 1095–1097. External Links: Link, Document Cited by: Quantum automated theorem proving. - [47] Y. Liu, S. Arunachalam, and K. Temme (2021-09) A rigorous and robust quantum speed-up in supervised machine learning. Nat. Phys. 17 (9), pp. 1013–1017. External Links: Document Cited by: Quantum automated theorem proving. - [48] S. Lloyd, M. Mohseni, and P. Rebentrost (2014-09) Quantum principal component analysis. Nat. Phys. 10 (9), pp. 631–633. External Links: Document Cited by: Quantum automated theorem proving. - [49] D. W. Loveland (2016) Automated theorem proving: a logical basis. North Holland. Cited by: §I, Quantum automated theorem proving, Quantum automated theorem proving, Quantum automated theorem proving. - [50] L. S. Madsen, F. Laudenbach, M. Falamarzi. Askarani, F. Rortais, T. Vincent, J. F. F. Bulmer, F. M. Miatto, L. Neuhaus, L. G. Helt, M. J. Collins, et al. (2022-06) Quantum computational advantage with a programmable photonic processor. Nature 606 (7912), pp. 75–81. External Links: ISSN 1476-4687, Document Cited by: Quantum automated theorem proving. - [51] A. Montanaro (2016-01) Quantum algorithms: an overview. npj Quantum Inf. 2 (1), pp. 15023. External Links: ISSN 2056-6387, Document Cited by: §IV. - [52] S. A. Moses, C. H. Baldwin, M. S. Allman, R. Ancona, L. Ascarrunz, C. Barnes, J. Bartolotta, B. Bjork, P. Blanchard, M. Bohn, et al. (2023-12) A race-track trapped-ion quantum processor. Phys. Rev. X 13, pp. 041052. External Links: Document, Link Cited by: Quantum automated theorem proving. - [53] Z. Ni, S. Li, X. Deng, Y. Cai, L. Zhang, W. Wang, Z. Yang, H. Yu, F. Yan, S. Liu, et al. (2023-03) Beating the break-even point with a discrete-variable-encoded logical qubit. Nature 616 (7955), pp. 56–60. External Links: ISSN 1476-4687, Document Cited by: Quantum automated theorem proving. - [54] M. A. Nielsen and I. L. Chuang (2012-06) Quantum computation and quantum information: 10th anniversary edition. Cambridge University Press. External Links: ISBN 9780511976667 Cited by: Quantum automated theorem proving, Quantum automated theorem proving. - [55] W. Ren, W. Li, S. Xu, K. Wang, W. Jiang, F. Jin, X. Zhu, J. Chen, Z. Song, P. Zhang, et al. (2022-11) Experimental quantum adversarial learning with programmable superconducting qubits. Nat. Comput. Sci. 2 (11), pp. 711–717. External Links: Document Cited by: Quantum automated theorem proving. - [56] J. A. Robinson (1965-01) A machine-oriented logic based on the resolution principle. J. ACM 12 (1), pp. 23–41. External Links: ISSN 0004-5411, Document Cited by: Quantum automated theorem proving, Quantum automated theorem proving. - [57] L. Ruiz-Perez and J. C. Garcia-Escartin (2017-04) Quantum arithmetic with the quantum fourier transform. Quantum Inf. Process. 16 (6), pp. 152. External Links: Document Cited by: Quantum automated theorem proving, Quantum automated theorem proving. - [58] S. J. Russell and P. Norvig (2020) Artificial intelligence a modern approach. Pearson. External Links: ISBN 9780134610993 Cited by: §I, §I, §I, §II.2, §II.2, §II.2, §II.2, Quantum automated theorem proving, Quantum automated theorem proving, Quantum automated theorem proving. - [59] N. Saxena (2009) Progress on polynomial identity testing. Bulletin of the European Association for Theoretical Computer Science 99, pp. 49–79. Cited by: Quantum automated theorem proving. - [60] N. Saxena (2014) Progress on polynomial identity testing-II. In Perspectives in Computational Complexity: The Somenath Biswas Anniversary Volume, pp. 131–146. External Links: ISBN 978-3-319-05446-9, Document, Link Cited by: Quantum automated theorem proving. - [61] A. Schönhage and V. Strassen (1971-09) Schnelle multiplikation großer zahlen. Computing 7 (3–4), pp. 281–292. External Links: ISSN 1436-5057, Document Cited by: Quantum automated theorem proving. - [62] J. T. Schwartz (1980-10) Fast probabilistic algorithms for verification of polynomial identities. J. ACM 27 (4), pp. 701–717. External Links: ISSN 0004-5411, Link, Document Cited by: §IV, §IV. - [63] R. Seidel, N. Tcholtchev, S. Bock, C. K. Becker, and M. Hauswirth (2022) Efficient floating point arithmetic for quantum computers. IEEE Access 10, pp. 72400–72415. External Links: ISSN 2169-3536, Document Cited by: §III.3.2. - [64] V.V. Shende, A.K. Prasad, I.L. Markov, and J.P. Hayes (2003-06) Synthesis of reversible logic circuits. IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst. 22 (6), pp. 710–722. External Links: ISSN 0278-0070, Document Cited by: Quantum automated theorem proving. - [65] A. Shpilka and A. Yehudayoff (2010-03) Arithmetic circuits: a survey of recent results and open questions. Found. Trends Theor. Comput. Sci. 5 (3–4), pp. 207–388. External Links: Document Cited by: §IV, Quantum automated theorem proving. - [66] S. Sinha, A. Prabhu, P. Kumaraguru, S. Bhat, and M. Bethge (2024) Wu’s method can boost symbolic ai to rival silver medalists and alphageometry to outperform gold medalists at imo geometry. External Links: 2404.06405 Cited by: Quantum automated theorem proving. - [67] V. V. Sivak, A. Eickbusch, B. Royer, S. Singh, I. Tsioutsios, S. Ganjam, A. Miano, B. L. Brock, A. Z. Ding, L. Frunzio, et al. (2023-03) Real-time quantum error correction beyond break-even. Nature 616 (7955), pp. 50–55. External Links: ISSN 1476-4687, Document Cited by: Quantum automated theorem proving. - [68] G. Szegő (1939) Orthogonal polynomials. American Mathematical Society. Cited by: §III.3.2, Quantum automated theorem proving. - [69] Y. Takahashi (2009) Quantum arithmetic circuits: a survey. IEICE Transactions on Fundamentals of Electronics, Communications and Computer Sciences E92.A (5), pp. 1276–1283. External Links: Document Cited by: Quantum automated theorem proving. - [70] T. H. Trinh, Y. Wu, Q. V. Le, H. He, and T. Luong (2024-01) Solving olympiad geometry without human demonstrations. Nature 625 (7995), pp. 476–482. External Links: ISSN 1476-4687, Document Cited by: Quantum automated theorem proving, Quantum automated theorem proving, Quantum automated theorem proving. - [71] K. Wang, Z. Lu, C. Zhang, G. Liu, J. Chen, Y. Wang, Y. Wu, S. Xu, X. Zhu, F. Jin, et al. (2025) Demonstration of low-overhead quantum error correction codes. External Links: 2505.09684 Cited by: Quantum automated theorem proving. - [72] W. K. Wootters and W. H. Zurek (1982) A single quantum cannot be cloned. Nature 299 (5886), pp. 802–803. External Links: Link, Document Cited by: Quantum automated theorem proving. - [73] W. Wu (1978) ON the decision problem and the mechanization of theorem-proving in elementary geometry. Sci. Sin. 21 (2), pp. 159–172. Cited by: Figure 4, Quantum automated theorem proving. - [74] X. Wu and L. Li (2024-12) Asymptotically optimal synthesis of reversible circuits. Inf. Comput. 301, pp. 105235. External Links: ISSN 0890-5401, Document Cited by: Quantum automated theorem proving. - [75] Y. Wu, W. Bao, S. Cao, F. Chen, M. Chen, X. Chen, T. Chung, H. Deng, Y. Du, D. Fan, et al. (2021-10) Strong quantum computational advantage using a superconducting quantum processor. prl 127 (18), pp. 180501. External Links: ISSN 1079-7114, Document Cited by: Quantum automated theorem proving. - [76] S. Xu, Z. Sun, K. Wang, H. Li, Z. Zhu, H. Dong, J. Deng, X. Zhang, J. Chen, Y. Wu, et al. (2024-07) Non-abelian braiding of fibonacci anyons with a superconducting processor. Nat. Phys. 20 (9), pp. 1469–1475. External Links: ISSN 1745-2481, Document Cited by: Quantum automated theorem proving. - [77] Z. Ye, S. Chou, and X. Gao (2008) An introduction to java geometry expert. In Proceedings of the 7th International Conference on Automated Deduction in Geometry, ADG’08, pp. 189–195. External Links: Document, ISBN 9783642210457, ISSN 1611-3349 Cited by: §III.1, Quantum automated theorem proving. - [78] T. J. Yoder, G. H. Low, and I. L. Chuang (2014-11) Fixed-point quantum search with an optimal number of queries. Phys. Rev. Lett. 113, pp. 210501. External Links: Document, Link Cited by: Quantum automated theorem proving, Quantum automated theorem proving. - [79] H. Zhong, H. Wang, Y. Deng, M. Chen, L. Peng, Y. Luo, J. Qin, D. Wu, X. Ding, Y. Hu, et al. (2020-12) Quantum computational advantage using photons. Science 370 (6523), pp. 1460–1463. External Links: ISSN 1095-9203, Document Cited by: Quantum automated theorem proving. - [80] R. Zippel (1979) Probabilistic algorithms for sparse polynomials. In Symbolic and Algebraic Computation, pp. 216–226. External Links: Document, ISBN 978-3-540-35128-3 Cited by: §IV, §IV. Supplementary Information: Quantum automated theorem proving Contents 1. I Preliminaries of automated theorem proving and propositional logic 1. II Quantum automated theorem proving in propositional logic and first-order logic 1. II.1 Quantum resolution in propositional logic 1. II.2 Quantum resolution in first-order logic 1. III Quantum automated theorem proving with Wu’s method 1. III.1 Preliminaries of Wu’s method 1. III.2 State-based quantum pseudo-division 1. III.3 Circuit-based quantum pseudo-division 1. III.3.1 Encoding polynomials into quantum circuits 1. III.3.2 Quantum polynomial interpolation 1. III.3.3 Quantum pseudo-division by constructing remainder circuit 1. IV Polynomial identity testing on quantum computers I Preliminaries of automated theorem proving and propositional logic We begin by reviewing the standard framework of automated theorem proving (ATP) in propositional logic [49, 58]. As a logic-based reasoning paradigm, ATP represents knowledge using formal sentences and derives conclusions by applying well-defined inference rules. Its defining characteristic is a deterministic, rule-based reasoning process, in which a knowledge base (KB) is encoded as a collection of formulas and logical consequences are derived through systematic inference. A knowledge base is a set of sentences expressed according to the syntax of a given logical representation. For example, in elementary arithmetic, the expression “ $x+y=4$ ” is a well-formed sentence, whereas “ $x4y+=$ ” is not. Beyond syntax, a logical system also requires a definition of semantics, which assigns meaning to sentences by specifying their truth values in different possible worlds. In arithmetic, the sentence “ $x+y=4$ ” is true in a world where $x=2$ and $y=2$ , but false in a world where $x=1$ and $y=1$ . A model is a mathematical abstraction representing such a possible world. If a sentence $\alpha$ is true in a model $m$ , we say that $m$ satisfies $\alpha$ , or that $m$ is a model of $\alpha$ . We denote by $M(\alpha)$ the set of all models of $\alpha$ . Logical reasoning is formalized through the notion of logical entailment, written as $$ \displaystyle\alpha\models\beta, $$ which means that the sentence $\beta$ is a logical consequence of the sentence $\alpha$ . Formally, $\alpha\models\beta$ if and only if $$ \displaystyle M(\alpha)\subseteq M(\beta). $$ In automated reasoning, new sentences are repeatedly derived from those already present in the knowledge base by applying inference rules. This process continues until no further derivations are possible or until a contradiction is obtained. An inference procedure is said to be sound (or truth-preserving) if every sentence it derives is logically entailed by the knowledge base. Soundness guarantees that no false statements are produced. The complementary notion is completeness: an inference procedure is complete if it can derive every sentence that is logically entailed by the knowledge base. Together, soundness and completeness ensure that all and only logically valid consequences can be derived [58]. Two inference rules are particularly prominent in propositional logic: modus ponens and resolution. Modus ponens–based reasoning is sound and complete for Horn clauses and can be implemented in linear time. However, Horn clauses are restricted to disjunctions containing at most one positive literal. In this work, we focus on resolution, which applies to arbitrary knowledge bases in propositional logic and extends naturally to first-order logic (FOL). Resolution is typically used in a refutation-based manner and constitutes a fundamental inference mechanism in classical ATP. The resolution rule in propositional logic takes the form $$ \displaystyle{{a_{1}\vee\cdots\vee a_{n}\vee c,\quad b_{1}\vee\cdots\vee b_{m}\vee\neg c}\over{a_{1}\vee\cdots\vee a_{n}\vee b_{1}\vee\cdots\vee b_{m}}}, $$ where all $a_{i}$ , $b_{i}$ , and $c$ are literals, and the horizontal line denotes logical entailment. A literal is either a propositional variable or its negation. The logical connectives $\vee$ , $\wedge$ , and $\neg$ denote disjunction, conjunction, and negation, respectively. In this manuscript, we occasionally use a comma to denote conjunction as an alternative to $\wedge$ . Several examples of resolution are given in Eq. (S4): $$ \displaystyle{{A\vee C,B\vee\neg C}\over{A\vee B}}, \displaystyle{{A\vee C\vee D,B\vee\neg C\vee D}\over{A\vee B\vee D}}, \displaystyle{{A\vee C\vee D,B\vee\neg C\vee\neg D}\over{A\vee C\vee D,B\vee\neg C\vee\neg D}}, \displaystyle{{C,\neg C}\over{\bot}} $$ Here, $A$ , $B$ , $C$ , and $D$ are propositional variables. Equation (S4a) illustrates a typical resolution step. In Eq. (S4b), both premises contain the same literal $D$ , which appears only once in the conclusion; this simplification is known as factoring. Equation (S4c) shows that when more than one pair of complementary literals appears across the premises, no resolution is possible. Finally, Eq. (S4d) produces the empty clause $\bot$ , which represents a contradiction [58]. The derivation of an empty clause signals inconsistency of the knowledge base and terminates the ATP process. Resolution applies to formulas expressed in conjunctive normal form (CNF), defined as a conjunction of clauses, each of which is a disjunction of literals. Every propositional logic formula is logically equivalent to a CNF formula. A standard transformation procedure proceeds as follows. We begin with formulas composed of the connectives $\neg$ , $\vee$ , and $\wedge$ , propositional variables, and parentheses. Any additional connectives (such as implication or biconditional) are first eliminated using logical equivalences. Negations are then pushed inward using De Morgan’s laws: $$ \displaystyle{\neg(a\wedge b)} \displaystyle\equiv{\neg a\vee\neg b}, \displaystyle{\neg(a\vee b)} \displaystyle\equiv{\neg a\wedge\neg b}. $$ Double negations are removed using $$ \displaystyle{\neg\neg a}\equiv a, $$ and finally, disjunction is distributed over conjunction: $$ \displaystyle{(a\wedge b)\vee c}\equiv{(a\vee c)\wedge(b\vee c)}. $$ Repeated application of these rules yields a conjunction of clauses, which constitutes the CNF representation of the knowledge base. To establish an entailment of the form $\text{KB}\models\alpha$ , resolution-based inference proceeds via proof by contradiction. One constructs the conjunction $\text{KB}\wedge\neg\alpha$ , converts it into CNF, and applies resolution iteratively. At each step, pairs of clauses containing complementary literals are resolved to produce new clauses, which are added to the set if not already present. This process continues until either no further clauses can be generated—indicating that KB does not entail $\alpha$ —or the empty clause $\bot$ is derived, which certifies that $\text{KB}\models\alpha$ . II Quantum automated theorem proving in propositional logic and first-order logic II.1 Quantum resolution in propositional logic In quantum automated theorem proving (QATP), the knowledge base—such as a collection of clauses in propositional logic—is encoded and processed directly on a quantum computer. We employ a quantum circuit to load the knowledge base into a quantum state. Concretely, this encoding is implemented by a unitary operator that takes as input a quantum register encoding the indices of clauses and entangles it with a data register storing the corresponding clause information: $$ \displaystyle{\left|j\right\rangle_{\text{I}}}{\left|0\right\rangle_{\text{D}}}\to{\left|j\right\rangle_{\text{I}}}{\left|{{m_{j}}}\right\rangle_{\text{D}}}, $$ where ${\left|j\right\rangle_{\text{I}}}$ denotes the state of the index register and ${\left|{{m_{j}}}\right\rangle_{\text{D}}}$ encodes the corresponding clause or coefficient in the data register. To perform reasoning in propositional logic, it is necessary to implement the resolution rule on a quantum computer. A central challenge arises from the fact that classical resolution is inherently irreversible: the premises cannot, in general, be reconstructed from the conclusion. In contrast, quantum circuits must be unitary and therefore reversible. In QATP, we address this challenge by introducing auxiliary qubits that store the resolution outcome while preserving the quantum states representing the premises. The basic quantum resolution operation is defined as $$ \displaystyle{U_{\text{R}}}\left|{{c_{1}}}\right\rangle\left|{{c_{2}}}\right\rangle\left|0\right\rangle=\left|{{c_{1}}}\right\rangle\left|{{c_{2}}}\right\rangle\left|\mathcal{R}(c_{1},c_{2})\right\rangle, $$ where $\left|{{c_{1}}}\right\rangle$ and $\left|{{c_{2}}}\right\rangle$ encode the premise clauses and $|\mathcal{R}(c_{1},c_{2})\rangle$ represents the resolution result. The process of quantum resolution is similar to the classical counterpart shown in Eq. (S3). This construction ensures reversibility by retaining the original premises. The explicit form of the quantum resolution circuit depends on the chosen clause representation. In CNF representation, each propositional variable is associated with a fixed register position, and its presence and polarity are encoded in the local quantum state. Logical disjunction symbols are omitted, as clauses are represented implicitly by the joint state of all variables. For example, the clause $A\vee\neg C$ can be encoded as ${\left|{1}\right\rangle_{A}}{\left|0\right\rangle_{B}}{\left|{2}\right\rangle_{C}}{\left|0\right\rangle_{D}}$ , where the four registers correspond to the propositional variables $\{A,B,C,D\}$ . The state $|1\rangle$ denotes the presence of a positive literal, $|2\rangle$ denotes the presence of a negated literal, and $|0\rangle$ denotes absence. The four basis states $|0\rangle$ , $|1\rangle$ , $|2\rangle$ , and $|3\rangle$ form a ququart (four-level system), which can equivalently be represented using two qubits as $|00\rangle$ , $|01\rangle$ , $|10\rangle$ , and $|11\rangle$ . Quantum resolution circuit operates by examining propositional variables one by one. For each variable, its occurrences in the two premise clauses determine how it is handled. In particular, a variable may appear in the two premises with opposite polarities, with the same polarity, in only one premise, or in neither premise, as shown in Eq. (S4). We first describe the unitary implementation for the representative situation shown in Eq. (S4a), and then explain how a verification circuit is used to judge the validity of all resolution situations shown in Eq. (S4). In Eq. (S4a), exactly one propositional variable (e.g., $C$ ) appears in the two premises with opposite polarities and is eliminated in the conclusion. The remaining propositional variables occur only in one clause of the premise and are recorded in the conclusion. The corresponding unitary action on a single propositional variable is $$ \displaystyle{U_{\text{R}}}\left|{0}\right\rangle\left|{0}\right\rangle\left|{0}\right\rangle=\left|{0}\right\rangle\left|{0}\right\rangle\left|{0}\right\rangle, \displaystyle{U_{\text{R}}}\left|{0}\right\rangle\left|{1}\right\rangle\left|{0}\right\rangle=\left|{0}\right\rangle\left|{1}\right\rangle\left|{1}\right\rangle, \displaystyle{U_{\text{R}}}\left|{0}\right\rangle\left|{2}\right\rangle\left|{0}\right\rangle=\left|{0}\right\rangle\left|{2}\right\rangle\left|{2}\right\rangle, \displaystyle{U_{\text{R}}}\left|{1}\right\rangle\left|{0}\right\rangle\left|{0}\right\rangle=\left|{1}\right\rangle\left|{0}\right\rangle\left|{1}\right\rangle, \displaystyle{U_{\text{R}}}\left|{1}\right\rangle\left|{1}\right\rangle\left|{0}\right\rangle=\left|{1}\right\rangle\left|{1}\right\rangle\left|{1}\right\rangle, \displaystyle{U_{\text{R}}}\left|{1}\right\rangle\left|{2}\right\rangle\left|{0}\right\rangle=\left|{1}\right\rangle\left|{2}\right\rangle\left|{3}\right\rangle, \displaystyle{U_{\text{R}}}\left|{2}\right\rangle\left|{0}\right\rangle\left|{0}\right\rangle=\left|{2}\right\rangle\left|{0}\right\rangle\left|{2}\right\rangle, \displaystyle{U_{\text{R}}}\left|{2}\right\rangle\left|{1}\right\rangle\left|{0}\right\rangle=\left|{2}\right\rangle\left|{1}\right\rangle\left|{3}\right\rangle, \displaystyle{U_{\text{R}}}\left|{2}\right\rangle\left|{2}\right\rangle\left|{0}\right\rangle=\left|{2}\right\rangle\left|{2}\right\rangle\left|{2}\right\rangle, $$ Here, the first two ququarts encode the premise literals and the third ququart encodes the conclusion. The four states $|0\rangle$ , $|1\rangle$ , $|2\rangle$ , and $|3\rangle$ represent absence, positive literal, negative literal, and resolved status, respectively. For a knowledge base with $N$ propositional variables, $N$ such resolution circuits are applied in parallel—one for each variable. When each ququart is encoded using two qubits, the full quantum resolution circuit takes the form shown in Fig. S1. Given a knowledge base containing $M$ clauses, the resolution circuit acts on the tensor product of two uniform superpositions over these clauses, producing $M^{2}$ candidate resolvents. Only resolvents in which exactly one propositional variable is marked as resolved (state $|3\rangle$ ) are considered valid; all other cases correspond to invalid resolutions, such as the situation shown in Eqs. (S4c), and are discarded. Valid resolvents are added to the knowledge base for the next resolution round. *[Error downloading image: .//fig-quantum-resolution-circuit.pdf]* Figure S1: Quantum circuit implementing the resolution operation for a single propositional variable. To determine whether a candidate resolvent is valid, we introduce a unitary circuit $U_{\text{J}}$ that checks whether exactly one propositional variable is in the state $|3\rangle$ . This circuit takes $N$ resolution outputs as input, uses $\log_{2}N$ auxiliary qubits, and writes the result to a single output qubit. The output is $|1\rangle$ if the resolvent is valid and $|0\rangle$ otherwise, as illustrated in Fig. S2 a. An explicit construction for $N=8$ is shown in Fig. S2 b. In this construction, we apply a quantum Fourier transform–based addition circuit to the auxiliary qubits, controlled by the resolution results. More specifically, this circuit adds one to the binary value stored in the auxiliary qubits whenever a resolution result $R_{n}$ is in the state $\lvert 3\rangle$ (corresponding to $\lvert 11\rangle$ in the qubit representation). In the final step, a Pauli- $X$ gate controlled on the auxiliary qubits being in the state $\lvert 001\rangle$ is applied, producing the output state $\lvert 1\rangle$ if and only if a valid conclusion is reached, that is, exactly one propositional variable is in the state $\lvert 3\rangle$ . The depth of this circuit is $O(N\log N)$ . *[Error downloading image: .//fig-judge-sucess-resolution-circuit.pdf]* Figure S2: Quantum circuit $U_{\text{J}}$ for validating resolution outcomes. a, Schematic illustration of $U_{\text{J}}$ , which outputs $\left|1\right\rangle$ if and only if exactly one propositional variable is in the state $\left|3\right\rangle$ . b, Explicit construction for $N=8$ . A quantum Fourier transform–based addition circuit counts the number of resolved variables, and a controlled Pauli- $X$ gate flags valid resolvents. We first apply the quantum Fourier transform to the $\log_{2}N$ auxiliary qubits, preparing the uniform superposition $\sum_{k=0}^{7}\lvert k\rangle/(2\sqrt{2})$ . For each resolution result $R_{n}$ in the state $\lvert 11\rangle$ , a phase factor $\exp(2\pi ik/8)$ is added to the state on auxiliary qubits. After applying the inverse quantum Fourier transform, the auxiliary register encodes the total number of resolution results in the state $\lvert 3\rangle$ . Finally, a Pauli- $X$ gate controlled on the auxiliary register being in the state $\lvert 001\rangle$ is used to output states indicating the validity of the result sentence onto the last qubit. As a concrete example, consider the knowledge base $\{A\vee\neg C,\;B\vee C,\;\neg B\}$ . This knowledge base is encoded as a uniform superposition of the quantum states ${\left|{1}\right\rangle_{A}}{\left|0\right\rangle_{B}}{\left|{2}\right\rangle_{C}}$ , ${\left|{0}\right\rangle_{A}}{\left|1\right\rangle_{B}}{\left|{1}\right\rangle_{C}}$ , and ${\left|{0}\right\rangle_{A}}{\left|2\right\rangle_{B}}{\left|{0}\right\rangle_{C}}$ . The direct product of two such superpositions forms the input to the quantum resolution circuit. Measurement of the output register in the computational (Pauli- $Z$ ) basis yields candidate resolvents. The termination conditions of quantum resolution mirror those of the classical procedure: the algorithm halts when either no new clauses can be derived or an empty clause—represented by the all-zero state—is produced. II.2 Quantum resolution in first-order logic First-order logic [24], also known as predicate logic, extends propositional logic by allowing statements about objects and their relations. A predicate denotes a Boolean-valued relation on a fixed number of arguments, returning either True or False. First-order logic also permits function symbols that map objects to objects, as well as constant symbols denoting specific (but model-dependent) elements of the domain. Unlike propositional variables, which range only over truth values, variables in first-order logic range over objects in the domain of a model. For example, the natural-language statement “John’s cat is a vehicle” can be expressed as $\mathrm{IsVehicle}(\mathrm{Cat}(\mathrm{John}))$ , where $\mathrm{IsVehicle}$ is a predicate symbol, $\mathrm{Cat}$ is a function symbol, and $\mathrm{John}$ is a constant symbol whose interpretation may vary across models. First-order logic additionally includes quantifiers that express statements about collections of objects. Universal quantification $∀$ asserts that a property holds for all objects, whereas existential quantification $∃$ asserts that there exists some object for which a property holds. For instance, “All cats are vehicles” can be written as $∀ x\bigl(\mathrm{IsCat}(x)→\mathrm{IsVehicle}(x)\bigr)$ , and “Some cats are vehicles” as $∃ x\bigl(\mathrm{IsCat}(x)\wedge\mathrm{IsVehicle}(x)\bigr)$ . In this work, we focus on first-order logic without equality, in which any sentence can be rewritten as a set of clauses in CNF [58]. Conversion to CNF. To apply resolution in first-order logic, sentences must first be converted to CNF. As in propositional logic, negations are pushed inward; in addition, negated quantifiers are transformed using $$ \displaystyle\neg\forall x\,P\;\Rightarrow\;\exists x\,\neg P, \displaystyle\neg\exists x\,P\;\Rightarrow\;\forall x\,\neg P, $$ where the symbol $\Rightarrow$ indicates a syntactic rewrite rather than logical implication. Double negations are eliminated using Eq. (S6). Next, bound variables are standardized apart: bound variables are renamed so that no variable symbol appears in more than one quantifier scope, preventing unintended interactions when quantifiers are later removed. Existential quantifiers are then eliminated by Skolemization. In the simplest case, $∃ x\,P(x)$ can be replaced by $P(A)$ , where $A$ is a fresh constant symbol. More generally, if the existential variable is within the scope of universal quantifiers, it is replaced by a new Skolem function of the universally quantified variables. As an example, consider the sentence “Either there is some sport that x likes, or x has doctors”, which in the first-order logic reads: $$ \displaystyle\forall x\bigl[\exists y\bigl(\mathrm{Sport}(y)\wedge\mathrm{Likes}(x,y)\bigr)\bigr]\;\vee\;\bigl[\exists z\,\mathrm{Doctor}(x,z)\bigr]. $$ Skolemization yields $$ \displaystyle\forall x\bigl(\mathrm{Sport}(F(x))\wedge\mathrm{Likes}(x,F(x))\bigr)\;\vee\;\mathrm{Doctor}(x,G(x)), $$ where $F$ and $G$ are Skolem functions. After Skolemization, the existential content is captured by these functions, and the remaining universal quantifiers may be dropped without loss of meaning, since all remaining variables are implicitly universally quantified. Finally, distributing $\vee$ over $\wedge$ using Eq. (S7) produces the CNF: $$ \displaystyle\bigl[\mathrm{Sport}(F(x))\vee\mathrm{Doctor}(x,G(x))\bigr]\wedge \displaystyle\bigl[\mathrm{Likes}(x,F(x))\vee\mathrm{Doctor}(x,G(x))\bigr]. $$ Resolution and unification. Resolution in first-order logic can be viewed as a lifted generalization of propositional resolution Eq. (S3). As in propositional logic, two clauses may be resolved when they contain complementary literals; in first-order logic, two literals are complementary if one can be made identical to the negation of the other by a suitable substitution. Determining such a substitution is the task of unification, which finds a mapping from variables to terms that makes two expressions syntactically identical. For example, $$ \displaystyle\mathrm{UNIFY}\bigl(\mathrm{Doctor}(\mathrm{John},x),\mathrm{Doctor}(\mathrm{John},\mathrm{Jane})\bigr)=\{x/\mathrm{Jane}\}. $$ Here, $\{x/\mathrm{Jane}\}$ replaces the variable $x$ with the term $\mathrm{Jane}$ . We write $\mathrm{SUBST}(\theta,p)$ for the result of applying substitution $\theta$ to an expression $p$ . Unification can then be defined abstractly as $$ \displaystyle\mathrm{UNIFY}(p,q)=\theta\quad\text{where}\quad\mathrm{SUBST}(\theta,p)=\mathrm{SUBST}(\theta,q). $$ Unlike an interpretation, which maps variables to domain objects, a substitution operates purely at the syntactic level by replacing variables with terms. With this notation, the (binary) resolution rule in first-order logic is given by $$ \displaystyle{{a_{1}\vee\cdots\vee a_{n}\vee c_{1},\quad b_{1}\vee\cdots\vee b_{m}\vee c_{2}}\over{\mathrm{SUBST}\!\left(\theta,\,a_{1}\vee\cdots\vee a_{n}\vee b_{1}\vee\cdots\vee b_{m}\right)}}, $$ where $\mathrm{UNIFY}(c_{1},\neg c_{2})=\theta$ . For instance, the clauses $\mathrm{Sport}(F(x))\vee\mathrm{Likes}(G(x),x)$ and $\neg\mathrm{Likes}(u,v)\vee\neg\mathrm{Doctor}(u,v)$ can be resolved by eliminating the complementary literals $\mathrm{Likes}(G(x),x)$ and $\neg\mathrm{Likes}(u,v)$ using the unifier $\theta=\{u/G(x),\,v/x\}$ , yielding the resolvent $$ \displaystyle\mathrm{Sport}(F(x))\vee\neg\mathrm{Doctor}(G(x),x). $$ This rule is called binary resolution because it resolves exactly one complementary pair of literals from two clauses. In first-order logic, binary resolution alone is not complete. Completeness is obtained by combining binary resolution with factoring, which merges two unifiable literals within a single clause and applies the corresponding unifier to the entire clause. The combination of binary resolution and factoring yields a complete refutation procedure for first-order logic without equality [58]. Now we give a concrete example on the badminton-basketball reasoning task mentioned in the main text (see Fig. 1 a). We start with sentences in English to form the knowledge base and state the conclusion we want to deduce: 1. Anyone likes sports that their father likes. 1. If someone likes badminton, then this person likes a certain type of badminton racket. 1. Alice does not like any kind of badminton racket. 1. Badminton and basketball are sports. 1. People who like the same sports play together. 1. People who play together either both like badminton or both like basketball. 1. Alice and Bob play together. 1. Alice’s father and Bob’s father do not play together. 1. Alice plays with her father. 1. Bob plays with his father. 1. Bob likes basketball and badminton. We assume that the first ten sentences belong to the knowledge base, and the last sentence is the conclusion we want to infer. We express these sentences in first-order logic as: 1. $∀ x,y\,\text{Likes}[\text{Father}(x),y]\wedge\text{Sport}(y)→\text{Likes}(x,y)$ ; 1. $∀ x\,\text{Likes}(x,\text{badminton})→[∃ y\,\text{Badmintonracket}(y)\wedge\text{Likes}(x,y)]$ 1. $∀ x\,\text{Badmintonracket}(x)→\neg\text{Likes(Alice, x)}$ ; 1. Sport(badminton); 1. Sport(basketball); 1. $∀ x,y,z\,\text{Sport}(x)\wedge\text{Likes}(y,x)\wedge\text{Likes}(z,x)→\text{Playtogether}(y,z)$ ; 1. $∀ x,y\,\text{Playtogether}(x,y)→[(\text{Likes}(x,\text{badminton})\wedge\text{Likes}(y,\text{badminton}))\vee(\text{Likes}(x,\text{basketball})\wedge\text{Likes}(y,\text{basketball}))]$ ; 1. Playtogether[Alice, Bob]; 1. $\neg\text{Playtogether[Father(Alice), Father(Bob)]}$ ; 1. Playtogether[Alice, Father(Alice)]; 1. Playtogether[Bob, Father(Bob)]; 1. $\text{Likes(Bob, basketball)}\wedge\text{Likes(Bob, badminton)}$ . The first eleven sentences are in the knowledge base and the last sentence is the conclusion we want to infer. Recalling that we prove $\text{KB}\models\alpha$ by proving the unsatisfiability of the conjunction $\text{KB}\wedge\neg\alpha$ . We transform these sentences to CNF as: 1. $\neg\text{Likes[Father}(x),y]\vee\neg\text{Sport}(y)\vee\text{Likes}(x,y)$ ; 1. $\neg\text{Likes}(x,\text{badminton})\vee\text{Badmintonracket}(F(x))$ ; 1. $\neg\text{Likes}(x,\text{badminton})\vee\text{Likes}(x,F(x))$ ; 1. $\neg\text{Badmintonracket}(x)\vee\neg\text{Likes(Alice},x)$ ; 1. Sport(badminton); 1. Sport(basketball); 1. $\neg\text{Sport}(x)\vee\neg\text{Likes}(y,x)\vee\neg\text{Likes}(z,x)\vee\text{Playtogether}(y,z)$ ; 1. $\neg\text{Playtogether}(x,y)\vee\text{Likes}(x,\text{badminton})\vee\text{Likes}(x,\text{basketball})$ ; 1. $\neg\text{Playtogether}(x,y)\vee\text{Likes}(y,\text{badminton})\vee\text{Likes}(x,\text{basketball})$ ; 1. $\neg\text{Playtogether}(x,y)\vee\text{Likes}(x,\text{badminton})\vee\text{Likes}(y,\text{basketball})$ ; 1. $\neg\text{Playtogether}(x,y)\vee\text{Likes}(y,\text{badminton})\vee\text{Likes}(y,\text{basketball})$ ; 1. Playtogether[Alice, Bob]; 1. $\neg\text{Playtogether[Father(Alice), Father(Bob)]}$ ; 1. Playtogether[Alice, Father(Alice)]; 1. Playtogether[Bob, Father(Bob)]; 1. $\neg\text{Likes(Bob, basketball)}\vee\neg\text{Likes(Bob, badminton)}$ . For illustration, we give the detailed process of transforming the second sentence $∀ x\,\text{Likes}(x,\text{badminton})→[∃ y\,\text{Badmintonracket}(y)\wedge\text{Likes}(x,y)]$ to CNF as an example: $$ \displaystyle\forall x\;\text{Likes}(x,\text{badminton})\to[\exists y\;\text{Badmintonracket}(y)\wedge\text{Likes}(x,y)]\Rightarrow \displaystyle\forall x\exists y\;\neg\text{Likes}(x,\text{badminton})\vee[\text{Badmintonracket}(y)\wedge\text{Likes}(x,y)]\Rightarrow \displaystyle\forall x\exists y\;[\neg\text{Likes}(x,\text{badminton})\vee\text{Badmintonracket}(y)]\wedge[\neg\text{Likes}(x,\text{badminton})\vee\text{Likes}(x,y)]\Rightarrow \displaystyle\forall x\;[\neg\text{Likes}(x,\text{badminton})\vee\text{Badmintonracket}(F(x))]\wedge[\neg\text{Likes}(x,\text{badminton})\vee\text{Likes}(x,F(x))]\Rightarrow \displaystyle[\neg\text{Likes}(x,\text{badminton})\vee\text{Badmintonracket}(F(x))]\wedge[\neg\text{Likes}(x,\text{badminton})\vee\text{Likes}(x,F(x))]. $$ The first transformation uses the relationship between implication and disjunction: $p→ q\equiv\neg p\vee q$ . The second transformation is to distribute $\vee$ over $\wedge$ using Eq. (S7). The next transformation is the skolemization, where $F$ is a Skolem function depending on $x$ . The last step is to remove the universal quantifier, since all remaining variables are implicitly universally quantified in CNF. The resolution proof that Bob’s father does not like basketball is given in Fig. S3. *[Error downloading image: .//fig-Bob-likes-badminton-basketball.pdf]* Figure S3: The resolution proof showing that Bob likes basketball and badminton. At each resolution step, the unified literals are shown in bold. Resolution in first-order logic has the additional step of unification compared to the resolution in propositional logic. This additional step, being computationally expensive on classical computers, poses a significant challenge to implementing quantum resolution in first-order logic. We address this problem by invoking the Herbrand’s theorem [58]. This theorem states that: if a set $W$ of clauses is unsatisfiable, then there exists a finite subset of $H_{W}(W)$ that is also unsatisfiable. $H_{W}(W)$ refers to the Herbrand base of $W$ . Given a set of clauses $W$ , then $H_{W}$ , the Herbrand universe of $W$ , is the set of all ground terms constructible from: 1. The function symbols in $W$ ; 1. The constant symbols in $W$ . Given a clause $\neg P(x,F(x,A))\vee\neg Q(x,A)\vee R(x,B)$ , the corresponding Herbrand universe is: $$ \displaystyle A,B,F(A,A),F(A,B),F(B,A),F(B,B),F(A,F(A,A)),\ldots $$ The Herbrand base of $W$ is the saturation of the set $W$ with respect to its Herbrand universe. The saturation is obtained by applying all possible substitutions of ground terms for variables in $W$ . Thus, the Herbrand base of $\neg P(x,F(x,A))\vee\neg Q(x,A)\vee R(x,B)$ is: $$ \displaystyle\neg P(A,F(A,A))\vee\neg Q(A,A)\vee R(A,B), \displaystyle\neg P(B,F(B,A))\vee\neg Q(B,A)\vee R(B,B), \displaystyle\neg P(F(A,A),F(F(A,A),A))\vee\neg Q(F(A,A),A)\vee R(F(A,A),B), \displaystyle\neg P(F(A,B),F(F(A,B),A))\vee\neg Q(F(A,B),A)\vee R(F(A,B),B),\ldots $$ If a set of clauses $W$ in first-order logic is unsatisfiable, we use the iterative process of adopting increasingly larger subsets of $H_{W}(W)$ . Since all the clauses have been propositionalized, we can use the same quantum resolution scheme described in Sec. II.1 to perform quantum resolution of first-order logic on a quantum computer. In each iteration, we propositionalize the problem within these subsets and apply the quantum resolution introduced in Eq. (S10), continuing this process until unsatisfiability is demonstrated. If $W$ is satisfiable, no quantum or classical algorithm can decide the validity for all first-order logic sentences, a property known as the semi-decidability of first-order logic [58]. III Quantum automated theorem proving with Wu’s method Compared with resolution-based reasoning, Wu’s method provides a more concrete and algebraic approach to automated theorem proving, and has proved highly effective for large classes of geometric problems [15]. The central idea of Wu’s method is to transform a geometric statement into an equivalent algebraic problem: by introducing an appropriate coordinate system, all geometric relations appearing in the hypotheses and the conclusion are expressed as polynomial equations. The proof then proceeds by eliminating variables from the conclusion polynomial using the known hypothesis polynomials through a systematic process of pseudo-division. If all dependent variables can be eliminated and the conclusion reduces to the trivial identity $0=0$ , the original geometric statement is proved. A major computational challenge in Wu’s method arises from the rapid growth of intermediate multivariate polynomials. These polynomials may contain an exponential number of terms, leading to significant time and space overhead in classical implementations. Quantum computers, by contrast, can store and process information in superposition, suggesting a natural opportunity to accelerate algebraic reasoning. In this work, we propose a quantum approach to geometric theorem proving that implements the pseudo-division steps of Wu’s method directly on a quantum computer, thereby enabling the reasoning of geometric statements within a quantum framework. III.1 Preliminaries of Wu’s method Before introducing the quantum implementation, we briefly review the essential idea of Wu’s method and its core algebraic ingredients. Wu’s method has been extensively developed and successfully applied in classical automated geometry proving [15, 77]. Compared with quantum resolution, its algebraic structure makes it particularly amenable to near-term quantum realization, as it relies on arithmetic operations rather than deep logical branching. The basic idea of Wu’s method is to prove elementary geometry statements by translating them into polynomial equations [15]. An appropriate coordinate system is first chosen to parameterize all points in the geometric configuration. The independent coordinate variables are denoted by $u_{1},...,u_{a}$ (collectively written as $\mathbf{u}$ ), while the remaining variables $x_{1},...,x_{b}$ (collectively written as $\mathbf{x}$ ) are algebraically dependent on $\mathbf{u}$ . Both the hypotheses and the conclusion of the geometric statement are then represented as polynomial equations in the variables $(\mathbf{u},\mathbf{x})$ . Wu’s method provides a systematic procedure to derive the conclusion through successive pseudo-division of these polynomials. In general, Wu’s method consists of three main steps. The first step converts the geometric statement into its algebraic form, yielding a set of polynomial equations. The second step performs triangulation of the hypothesis polynomials via pseudo-division, so that each polynomial introduces exactly one new dependent variable. The final step sequentially pseudo-divides the conclusion polynomial by the triangulated hypotheses, eliminating dependent variables one by one. After all dependent variables have been eliminated, the resulting pseudo-remainder is either a polynomial in $\mathbf{u}$ or identically zero. In the latter case, the conclusion follows from the hypotheses under generic (non-degenerate) conditions. Such non-degeneracy assumptions correspond to exceptional parameter values that are geometrically insignificant and are standard in Wu’s method [15]. As our focus is on the quantum implementation rather than geometric special cases, we restrict attention to the generic setting in which these conditions are satisfied. The fundamental algebraic operation used throughout Wu’s method is pseudo-division. Consider two multivariate polynomials S and T, which are to be pseudo-divided with respect to the variable $y$ , while the remaining variables are denoted by $x_{1},x_{2},...,x_{\text{K}}$ : $$ \displaystyle=\sum_{{\bf i},d_{1}}^{{\bf I},\text{D}_{\text{s}}}\text{s}({\bf i},d_{1})\prod_{k=1}^{\text{K}}x_{k}^{i_{k}}y^{d_{1}}, \displaystyle=\sum_{{\bf j},d_{2}}^{{\bf J},\text{D}_{\text{t}}}\text{t}({\bf j},d_{2})\prod_{k=1}^{\text{K}}x_{k}^{j_{k}}y^{d_{2}}, $$ where $\text{s}(·)$ and $\text{t}(·)$ denote the coefficients of S and T, respectively. The multi-indices ${\bf i}=(i_{1},...,i_{\text{K}})$ and ${\bf j}=(j_{1},...,j_{\text{K}})$ encode the degrees of the variables $x_{k}$ . We denote by $\text{D}_{\text{s}}$ and $\text{D}_{\text{t}}$ the degrees of S and T in $y$ , and by $\text{I}_{k}$ and $\text{J}_{k}$ the maximal degrees of the variables $x_{k}$ . Assuming $\text{D}_{\text{s}}>\text{D}_{\text{t}}$ , the first step of pseudo-division computes $$ \displaystyle\text{R}=\sum_{\bf j}^{\bf J}\text{t}({\bf j},\text{D}_{\text{t}})\prod_{k=1}^{\text{K}}x_{k}^{j_{k}}\text{S}-\sum_{\bf i}^{\bf I}\text{s}({\bf i},\text{D}_{\text{s}})\prod_{k=1}^{\text{K}}x_{k}^{i_{k}}\text{T}\,y^{\text{D}_{\text{s}}-\text{D}_{\text{t}}}, $$ where the two prefactors $\sum_{\bf j}^{\bf J}\text{t}({\bf j},\text{D}_{\text{t}})\prod_{k=1}^{\text{K}}x_{k}^{j_{k}}$ and $\sum_{\bf i}^{\bf I}\text{s}({\bf i},\text{D}_{\text{s}})\prod_{k=1}^{\text{K}}x_{k}^{i_{k}}$ are the leading coefficients of T and S with respect to $y$ , respectively. Expanding Eq. (S23), the resulting polynomial R can be written as $$ \displaystyle\text{R}=\sum_{{\bf i},{\bf j},d}^{{\bf I},{\bf J},\text{D}_{\text{s}}}\Bigl[\text{s}({\bf i},d)\,\text{t}({\bf j},\text{D}_{\text{t}})-\text{s}({\bf i},\text{D}_{\text{s}})\,\text{t}({\bf j},d+\text{D}_{\text{t}}-\text{D}_{\text{s}})\Bigr]\prod_{k=1}^{\text{K}}x_{k}^{i_{k}+j_{k}}y^{d}. $$ In particular, the coefficient of $y^{\text{D}_{\text{s}}}$ vanishes identically: $$ \displaystyle\sum_{{\bf i},{\bf j}}^{{\bf I},{\bf J}}\bigl[\text{s}({\bf i},\text{D}_{\text{s}})\text{t}({\bf j},\text{D}_{\text{t}})-\text{s}({\bf i},\text{D}_{\text{s}})\text{t}({\bf j},\text{D}_{\text{t}})\bigr]\prod_{k=1}^{\text{K}}x_{k}^{i_{k}+j_{k}}=0, $$ which implies that $\deg(\text{R},y)<\max[\deg(\text{S},y),\deg(\text{T},y)]$ . By iterating this procedure, the degree in $y$ is strictly reduced at each step, yielding the pseudo-remainder $\rm{prem}(\text{S},\text{T},y)$ satisfying $$ \displaystyle\deg[{\rm{prem}}({\rm{S}},{\rm{T}},y),y]<\min[\deg({\rm{S}},y),\deg({\rm{T}},y)]. $$ This pseudo-division procedure is used to eliminate variables during the triangulation of the hypotheses and, subsequently, during the elimination of variables from the conclusion polynomial. In Wu’s method, the conclusion is proved once the final pseudo-remainder vanishes identically, completing the algebraic proof of the original geometric statement. Now we analyze the complexity of Wu’s method. From Eq. (S24), computing all coefficients of the polynomial R in a single pseudo-division step requires, in the worst case, $$ \displaystyle({{\rm{D}}_{\rm{s}}}+{{\rm{D}}_{\rm{t}}}+2)\prod\limits_{k=1}^{\rm{K}}{{\rm{(}}{{\rm{I}}_{k}}{\rm{+1)}}}\prod\limits_{k=1}^{\rm{K}}{{\rm{(}}{{\rm{J}}_{k}}+1{\rm{)}}} $$ integer multiplications. Moreover, Eq. (S24) shows that the degree of R is bounded above by $$ \displaystyle\text{D}_{\text{s}}-1+\sum_{k=1}^{\text{K}}(\text{I}_{k}+\text{J}_{k}), $$ which is essentially the sum of the degrees of the two input polynomials. Because the resulting polynomial R is used as an input to subsequent pseudo-division steps, both the degree and the number of terms may increase rapidly as the procedure progresses, potentially leading to exponential growth. A central metric for the complexity of the overall proof is therefore the maximum number of terms appearing among all intermediate polynomials generated during successive pseudo-divisions [15]. For a polynomial of total degree D in K variables, the number of coefficients scales as the binomial coefficient $\binom{\text{D}+\text{K}}{\text{D}}$ , which grows exponentially with both D and K. Consequently, the worst-case time and space complexity of Wu’s method increases exponentially in the number of variables and the polynomial degree. Although Wu’s method is theoretically complete for equality-based geometric reasoning, this rapid growth in computational cost severely limits its practical applicability, motivating the exploration of alternative implementations—such as the quantum approach introduced in this work—that may better manage the combinatorial explosion inherent in algebraic geometry proving. As a simple illustrative example, we apply Wu’s method to prove the classical geometric fact that the diagonals of a rhombus are perpendicular. *[Error downloading image: .//fig-rhombus.pdf]* Figure S4: A rhombus. Let ABCD be a rhombus, that is, a quadrilateral with both pairs of opposite sides parallel and all sides of equal length. As shown in Fig. S4, we choose a coordinate system in which the four vertices have coordinates $\text{A}(0,0)$ , $\text{B}(u_{1},0)$ , $\text{C}(u_{2},x_{1})$ , and $\text{D}(x_{2},x_{1})$ . This choice reflects the assumptions that the sides AB and CD are parallel ( $\text{AB}\parallel\text{CD}$ ) and of equal length ( $\text{AB}=\text{CD}$ ). The remaining defining properties of a rhombus—namely $\text{AD}\parallel\text{BC}$ and $\text{AB}=\text{AD}$ —can then be translated into the following polynomial equations: $$ \displaystyle h_{1} \displaystyle=-x_{2}+(u_{2}-u_{1})=0, \displaystyle h_{2} \displaystyle=-(x_{1}^{2}+x_{2}^{2})+u_{1}^{2}=0. $$ The geometric conclusion to be proved is that the diagonals AC and BD are perpendicular, denoted $text{AC}\perp\text{BD}$ . In algebraic form, this condition can be expressed as $$ \displaystyle g_{1}=x_{1}^{2}+u_{2}(x_{2}-u_{1})=0. $$ The problem is thus reduced to deriving the polynomial equation $g_{1}=0$ from the hypotheses $h_{1}=0$ and $h_{2}=0$ using algebraic manipulations. Wu’s method provides a systematic procedure for carrying out this derivation through successive pseudo-divisions. Starting from the triangulated hypotheses in Eq. (S29), the first pseudo-division step yields $$ \displaystyle r_{1}=-g_{1}-h_{2}=x_{2}^{2}-u_{2}x_{2}+(u_{1}u_{2}-u_{1}^{2}). $$ The second pseudo-division eliminates the remaining quadratic term in $x_{2}$ : $$ \displaystyle r_{2}=-r_{1}-x_{2}h_{1}=u_{1}x_{2}+u_{1}u_{2}-u_{1}^{2}. $$ Finally, a third pseudo-division removes the remaining dependence on $x_{2}$ : $$ \displaystyle r_{3}=-r_{2}-u_{1}h_{1}=0. $$ The vanishing of the final pseudo-remainder $r_{3}$ completes the proof, establishing that the diagonals of any rhombus are perpendicular. III.2 State-based quantum pseudo-division In this section, we introduce a state-based approach for quantum pseudo-division of polynomials (QPP). In this setting, the QPP algorithm takes as input a quantum representation of two multivariate polynomials and outputs a quantum representation of their pseudo-remainder. In this subsection, the polynomials are represented by quantum states encoding their coefficients. The coefficients of the pseudo-remainder are extracted by measuring the output state in the Pauli- $Z$ basis. The measurement outcomes are then processed on a classical computer and re-encoded into quantum states for subsequent operations. Starting from two polynomials S and T defined in Eq. (S22), the first step of the algorithm is to encode the coefficients of S and T into a single quantum state: $$ \displaystyle\left|\psi\right\rangle={1\over c_{0}}\sum\limits_{{\bf{i}}}^{{\bf{I}}}\sum\limits_{{\bf{j}}}^{{\bf{J}}}\sum\limits_{d=0}^{{\text{D}_{\text{s}}}}\left|d\right\rangle\left|{{\bf{i}}}\right\rangle\left|{\text{s}\left({{\bf{i}},d}\right)}\right\rangle\left|{\text{s}\left({{\bf{i}},{\text{D}_{\text{s}}}}\right)}\right\rangle\left|{{\bf{j}}}\right\rangle\left|{\text{t}\left({{\bf{j}},d+{\text{D}_{\text{t}}}-{\text{D}_{\text{s}}}}\right)}\right\rangle\left|{\text{t}\left({{\bf{j}},{\text{D}_{\text{t}}}}\right)}\right\rangle. $$ Here $c_{0}$ is a normalization factor given by $c_{0}=2^{I_{1}+·s+I_{K}+J_{1}+·s+\text{D}_{\text{s}}}$ . The indices ${\bf i}$ and ${\bf j}$ label the degrees of variables other than $y$ , while $d$ denotes the degree of $y$ . The registers $\left|\text{s}({\bf i},d)\right\rangle$ and $\left|\text{t}({\bf j},d+\text{D}_{\text{t}}-\text{D}_{\text{s}})\right\rangle$ store the corresponding coefficients of S and T, respectively. The registers $\left|\text{s}({\bf i},\text{D}_{\text{s}})\right\rangle$ and $\left|\text{t}({\bf j},\text{D}_{\text{t}})\right\rangle$ encode the leading coefficients of S and T with respect to the variable $y$ , consistent with the classical pseudo-division procedure. The shifted index $d+\text{D}_{\text{t}}-\text{D}_{\text{s}}$ in the coefficients of T reflects the standard pseudo-division step, where the polynomial of lower degree in $y$ is multiplied by $y^{\text{D}_{\text{s}}-\text{D}_{\text{t}}}$ prior to subtraction. This adjustment is implemented here as a coherent shift of the coefficient indices in the quantum state. In the quantum pseudo-division procedure, the first step is to multiply the polynomial S by the leading coefficient of T with respect to the variable $y$ , and to multiply the polynomial T by the leading coefficient of S with respect to $y$ . We introduce additional qubits to store the results of these multiplications. The result quantum state is given by: $$ \displaystyle{1\over{{c_{0}}}}\sum\limits_{{\bf{i}}}^{{\bf{I}}}\sum\limits_{{\bf{j}}}^{{\bf{J}}}\sum\limits_{d=0}^{{\text{D}_{\text{s}}}}\left|d\right\rangle\left|{{\bf{i}}}\right\rangle\left|{\text{s}\left({{\bf{i}},d}\right)}\right\rangle\left|{\text{s}\left({{\bf{i}},{\text{D}_{\text{s}}}}\right)}\right\rangle\left|{{\bf{j}}}\right\rangle\left|{\text{t}\left({{\bf{j}},d+{\text{D}_{\text{t}}}-{\text{D}_{\text{s}}}}\right)}\right\rangle\left|{\text{t}\left({{\bf{j}},{\text{D}_{\text{t}}}}\right)}\right\rangle\left|{\text{s}\left({{\bf{i}},d}\right)\text{t}\left({{\bf{j}},{\text{D}_{\text{t}}}}\right)}\right\rangle\left|{\text{t}\left({{\bf{j}},d+{\text{D}_{\text{t}}}-{\text{D}_{\text{s}}}}\right)\text{s}\left({{\bf{i}},{\text{D}_{\text{s}}}}\right)}\right\rangle. $$ For fixed indices ${\bf i}$ , ${\bf j}$ , and $d$ , the last two registers encode the products $\text{s}({\bf i},d)\text{t}({\bf j},\text{D}_{\text{t}})$ and $\text{t}({\bf j},d+\text{D}_{\text{t}}-\text{D}_{\text{s}})\text{s}({\bf i},\text{D}_{\text{s}})$ , respectively. The next step is to perform the subtraction between the two products and calculate the powers of different variables by adding the corresponding indices $\bf{i}+\bf{j}$ . The result state is $$ \displaystyle{1\over{{c_{0}}}}\sum\limits_{\bf{i}}^{\bf{I}}{\sum\limits_{\bf{j}}^{\bf{J}}{\sum\limits_{d=0}^{{\text{D}_{\text{s}}}}{\left|d\right\rangle}}}\left|{\bf{i}}\right\rangle \displaystyle\left|{\text{s}\left({{\bf{i}},d}\right)}\right\rangle\left|{\text{s}\left({{\bf{i}},{\text{D}_{\text{s}}}}\right)}\right\rangle\left|{\bf{j}}\right\rangle\left|{\text{t}\left({{\bf{j}},d+{\text{D}_{\text{t}}}-{\text{D}_{\text{s}}}}\right)}\right\rangle\left|{\text{t}\left({{\bf{j}},{\text{D}_{\text{t}}}}\right)}\right\rangle \displaystyle\left|{\text{s}\left({{\bf{i}},d}\right)\text{t}\left({{\bf{j}},{\text{D}_{\text{t}}}}\right)-\text{t}\left({{\bf{j}},d+{\text{D}_{\text{t}}}-{\text{D}_{\text{s}}}}\right)\text{s}\left({{\bf{i}},{\text{D}_{\text{s}}}}\right)}\right\rangle\left|{\text{t}\left({{\bf{j}},d+{\text{D}_{\text{t}}}-{\text{D}_{\text{s}}}}\right)\text{s}\left({{\bf{i}},{\text{D}_{\text{s}}}}\right)}\right\rangle\left|{{\bf{i}}+{\bf{j}}}\right\rangle. $$ A classical description of the pseudo-remainder of S divided by T with respect to the variable $y$ is obtained by measuring the resulting state in the Pauli- $Z$ basis. The measurement outcomes of the registers $\left|{\bf i}+{\bf j}\right\rangle$ and $\left|d\right\rangle$ specify the powers of the variables, while the outcomes of the coefficient register yield the corresponding coefficients. However, for a fixed multi-index ${\bf i}+{\bf j}$ , the associated coefficients are stored in a superposition over different decompositions of ${\bf i}$ and ${\bf j}$ . Recovering the final coefficient therefore requires summing all contributions corresponding to the same monomial on a classical computer, which is equivalent to combining like terms in classical polynomial multiplication. Specifically, the state corresponding to ${\bf i}+{\bf j}={\bf I}_{0}$ is: $$ \displaystyle\sum\limits_{\bf{i}}^{{\bf{I}}_{0}}{\left|{\bf{i}}\right\rangle}\left|{\text{s}\left({{\bf{i}},d}\right)t\left({{{\bf{I}}_{0}}-{\bf{i}},{\text{D}_{\text{t}}}}\right)-t\left({{{\bf{I}}_{0}}-{\bf{i}},d+{\text{D}_{\text{t}}}-{\text{D}_{\text{s}}}}\right)\text{s}\left({{\bf{i}},{\text{D}_{\text{s}}}}\right)}\right\rangle, $$ where the normalization factor is omitted. The coefficient corresponding to $({\bf I}_{0},d)$ is obtained by measuring all terms in Eq. (S37) and summing them over different values of ${\bf i}$ . As a consequence, the state-based coefficient encoding requires measurement and classical post-processing to combine like terms after each polynomial multiplication. This measurement-induced collapse prevents coherent reuse of intermediate results and therefore would hardly offer any quantum advantage over classical pseudo-division. In this work, we will not use this state-based approach, but instead exploit a more convenient circuit-based approach. The state-based approach introduced here serves merely as a conceptual baseline for comparison. III.3 Circuit-based quantum pseudo-division We now introduce a circuit-based framework for quantum pseudo-division, designed to perform all algebraic operations required by Wu’s method using only a single encoding step at the beginning of the computation and a single measurement step at the end. In contrast to the state-based approach discussed above, polynomials in this framework are encoded directly into quantum circuits and manipulated coherently throughout the entire proof procedure. The construction is based on the point–value representation of polynomials and therefore avoids the explicit aggregation of like terms on classical hardware, which constitutes a fundamental bottleneck for state-based implementations. This subsection is organized as follows. We first describe how multivariate polynomials can be encoded as quantum circuits. We then explain how polynomial interpolation can be realized within the circuit model to extract coefficient polynomials with respect to a chosen variable. Finally, we show how these components are combined to implement quantum pseudo-division and to support the iterative variable-elimination steps required by Wu’s method. III.3.1 Encoding polynomials into quantum circuits We begin by describing how a multivariate polynomial can be represented by a quantum circuit. Taking the polynomial S in Eq. (S22) as an example, we represent S by a quantum circuit $U_{\text{S}}$ . The circuit takes the variables $\mathbf{x}$ and $y$ as inputs, each encoded as a binary string on quantum registers, together with an auxiliary register initialized in the state $\lvert\mathbf{0}\rangle$ . Here, $\mathbf{x}$ denotes the collection of variables $\{x_{k}\}$ , and $\lvert\mathbf{0}\rangle$ is a shorthand for the multi-qubit all-zero state $\lvert 00·s 0\rangle$ . The circuit evaluates the polynomial S and writes the result into the auxiliary register as a quantum state encoding the corresponding binary integer: $$ \displaystyle U_{\text{S}}\lvert\mathbf{x}\rangle\lvert y\rangle\lvert\mathbf{0}\rangle=\lvert\mathbf{x}\rangle\lvert y\rangle\lvert\text{S}(\mathbf{x},y)\rangle. $$ The circuit-based representation in Eq. (S38) is naturally compatible with the point–value representation of polynomials. In classical computation, the point–value representation is a standard technique for accelerating polynomial multiplication, reducing the time complexity from $\Theta(\text{D}^{2})$ to $\Theta(\text{D}\log\text{D})$ for degree- D univariate polynomials. In this representation, two degree- D polynomials $f$ and $h$ are specified by $\text{D}+1$ point–value pairs $(x_{d},f(x_{d}))$ and $(x_{d},h(x_{d}))$ . Their product $f· h$ , which has degree at most $2\text{D}$ , is uniquely determined by $2\text{D}{+}1$ point–value pairs $(x_{d},f(x_{d})h(x_{d}))$ . Polynomial multiplication is thereby reduced to a collection of independent pointwise multiplications, without ever forming or aggregating monomial coefficients. This feature is crucial for quantum computation. Combining like terms is an irreversible operation and therefore fundamentally incompatible with coherent quantum evolution. By working entirely within the point–value representation and constructing new circuit representations directly from existing ones, repeated pseudo-division steps can be carried out coherently, without intermediate measurements, classical post-processing, or re-encoding of polynomials. We adopt this perspective to encode polynomials into quantum circuits and consider two natural strategies for realizing a point–value circuit representation on a quantum device. The first strategy is arithmetic-based: the circuit explicitly implements the algebraic structure of the polynomial using quantum integer addition, subtraction, and multiplication, enabling evaluation on arbitrary integer inputs encoded as qubit strings. This approach follows directly from the symbolic expression of the polynomial and has been illustrated with concrete examples in the main text. The second strategy is data-driven: a sufficient set of input points is selected in advance, the corresponding polynomial values are classically computed, and these index–value pairs are embedded directly into a quantum circuit. The circuit then maps an index register labeling the sampled points to a register storing the associated polynomial values. Each strategy has distinct advantages. The arithmetic-based approach supports evaluation on arbitrary inputs and aligns closely with symbolic algebra, whereas the data-driven approach offers greater flexibility in the choice of sampling points and often leads to simpler circuit constructions. We now briefly analyze the circuit complexity associated with these two encoding strategies. For the arithmetic-based approach, the circuit cost is determined by the total cost of evaluating and accumulating all nonzero monomials in the polynomial. Each monomial is evaluated independently from qubit-string–encoded inputs using quantum integer multiplication, together with the necessary additions and shifts. Consequently, the overall gate count and circuit depth are obtained by summing the costs of the arithmetic subcircuits corresponding to each monomial, rather than by a single uniform per-term prefactor. The dominant cost arises from quantum integer multiplication. The best known ancilla-free constructions achieve an asymptotic gate complexity of $\mathcal{O}(n^{1+\epsilon})$ for multiplying $n$ -bit integers, for any $\epsilon>0$ , with practical constructions exhibiting scalings as low as $\mathcal{O}(n^{1.3})$ . For the data-driven strategy, the dominant cost arises from loading classical point–value data into a quantum circuit. Once the point values are computed classically, the quantum circuit needs only to implement a data-loading unitary that maps an index register to the corresponding stored value. Using a construction analogous to the $U_{\text{KB}}$ circuit introduced in the main text, such a unitary can be implemented with circuit depth scaling as $O(\text{D}\log\text{D})$ , where D is the number of point–value pairs used to represent the polynomial. Subsequent polynomial operations, including multiplication and repeated pseudo-division steps, can then be performed entirely within the point–value representation, without introducing additional overhead associated with combining like terms. III.3.2 Quantum polynomial interpolation To eliminate a specific variable $y$ in the QPP procedure, we introduce a quantum circuit $U_{\text{S},y}$ that outputs the coefficient of $y^{d}$ in the polynomial S, with the exponent $d$ provided as an input. The construction of $U_{\text{S},y}$ from the evaluation circuit $U_{\text{S}}$ is achieved via a quantum polynomial interpolation procedure, which we describe in detail below. The circuit implements the following transformation: $$ \displaystyle U_{\text{S},y}\lvert d\rangle\lvert\mathbf{x}\rangle\lvert\mathbf{0}\rangle=\lvert d\rangle\lvert\mathbf{x}\rangle\left|\sum_{\bf i}^{\bf I}\text{s}({\bf i},d)\prod_{k=1}^{\text{K}}x_{k}^{i_{k}}\right\rangle. $$ Here, $\sum_{\bf i}^{\bf I}\text{s}({\bf i},d)\prod_{k}^{\text{K}}x_{k}^{i_{k}}$ is precisely the coefficient of $y^{d}$ in S as defined in Eq. (S22). Importantly, this coefficient is itself a multivariate polynomial in the remaining variables $\mathbf{x}$ . As a simple illustration, the coefficient of $y^{2}$ ( $d=2$ ) in the polynomial $x_{1}^{2}y^{2}+x_{2}y^{2}-y^{2}+x_{1}y$ is the polynomial $x_{1}^{2}+x_{2}-1$ . A schematic representation of the circuit $U_{\text{S},y}$ is shown in Fig. S5 a. For clarity, the registers encoding the variables $\mathbf{x}$ are omitted, and the output state $\left|\sum_{\bf i}^{\bf I}\text{s}({\bf i},d)\prod_{k}\text{K}x_{k}^{i_{k}}\right\rangle$ is abbreviated as $\lvert\text{s}({\bf i},d)\rangle$ . Interpolation strategy. We now describe how to construct the circuit $U_{\text{S},y}$ from the evaluation circuit $U_{\text{S}}$ . This task can be viewed as a univariate polynomial interpolation problem in the variable $y$ , whose goal is to extract the coefficient polynomials associated with different powers of $y$ in $\text{S}(\mathbf{x},y)$ . If $\text{S}(\mathbf{x},y)$ has degree D in $y$ , then determining $U_{\text{S},y}$ amounts to recovering $D{+}1$ coefficient polynomials in the remaining variables $\mathbf{x}$ . Classically, this problem is typically solved by evaluating the polynomial at a suitable set of interpolation points $\{y_{d}\}$ and reconstructing the coefficients from these values. A common choice is Fourier-based interpolation, in which the points are chosen as the D -th roots of unity $y_{d}=\exp(2\pi id/\text{D})$ , enabling the use of fast Fourier transform algorithms. In the quantum setting, however, such approaches require complex-valued arithmetic and floating-point representations, which introduce substantial overhead. Kravchuk-based quantum interpolation. To avoid these complications, we adopt the Kravchuk polynomial basis [68] to perform interpolation entirely over integer-valued domains. This choice preserves real-valued arithmetic throughout the computation and is therefore directly compatible with our qubit-string encoding of integers, eliminating the need for complex-number manipulation on quantum hardware [63]. The Kravchuk polynomials are defined as $$ \displaystyle K_{d}(y,\text{D},q)=\sum_{j=0}^{d}(-1)^{j}(q-1)^{d-j}C(\text{D}-j,d-j)C(y,j), $$ where $C(·,·)$ denotes the binomial coefficient. In this work, we restrict ourselves to the simplest and most practical case $q=2$ . The Kravchuk polynomials satisfy the orthogonality relation: $$ \displaystyle\sum_{d=0}^{\text{D}}C(\text{D},d)\,K_{e}(d,\text{D},2)\,K_{f}(d,\text{D},2)=2^{\text{D}}C(\text{D},e)\,\delta_{e,f}. $$ From this orthogonality, the corresponding completeness relation follows: $$ \displaystyle\sum\limits_{e=0}^{\rm{D}}{{1\over{C({\rm{D}},e)}}{K_{e}}(d,{\rm{D}},2){\mkern 1.0mu}{K_{e}}(f,{\rm{D}},2)}={{{2^{\rm{D}}}}\over{C({\rm{D}},d){\mkern 1.0mu}}}{\delta_{d,f}}. $$ Given a univariate polynomial $\text{S}(y)$ evaluated at integer points $y=d$ , where the dependence on $\mathbf{x}$ is suppressed for clarity, the corresponding Kravchuk coefficients are given by $$ \displaystyle c_{e}=\sum_{d=0}^{\text{D}}C(\text{D},d)\,\text{S}(d)\,K_{e}(d,\text{D},2). $$ The polynomial $\text{S}(y)$ can then be reconstructed via the expansion $$ \displaystyle\text{S}(y)=\sum_{d=0}^{\text{D}}\frac{c_{d}}{2^{\text{D}}C(\text{D},d)}\,K_{d}(y,\text{D},2). $$ Quantum implementation. In the quantum setting, computing the Kravchuk coefficients $\lvert c_{d}\rangle$ —rather than the monomial-basis coefficients $\lvert\text{s}({\bf i},d)\rangle$ —can be decomposed into three coherent components: 1. preparing the integer weights $\lvert C(\text{D},y)K_{d}(y,\text{D},2)\rangle$ , 1. generating the point values $\lvert\text{S}(0)\rangle,\lvert\text{S}(1)\rangle,...,\lvert\text{S}(\text{D})\rangle$ using the evaluation circuit $U_{\text{S}}$ , and 1. applying a reversible arithmetic circuit to compute the weighted sum $\lvert\sum_{y=0}^{\text{D}}C(\text{D},y)\text{S}(y)K_{d}(y,\text{D},2)\rangle$ . Since the factors $C(\text{D},y)K_{d}(y,\text{D},2)$ are independent of the polynomial values $\text{S}(y)$ , they can be encoded using a fixed circuit $U_{CK}$ that prepares the corresponding integer data. This circuit is analogous to the data-loading procedure in Eq. (S8) and has depth $O(\text{D}\log\text{D})$ . Together with the evaluation circuit $U_{\text{S}}$ , this enables the coherent computation of the Kravchuk coefficients. Specifically, the circuit allocates $\text{D}{+}1$ value registers, each associated with one evaluation point $y∈{0,1,...,\text{D}}$ , and uses $U_{\text{S}}$ to populate these registers with the point values $\text{S}(0),S(1),...,S(\text{D})$ . It then applies a reversible interpolation transform that computes the Kravchuk coefficient indexed by $d$ via the weighted sum over the populated value registers. This transform serves as the quantum analogue of classical coefficient extraction and yields the coefficient polynomial in encoded form. As a result, the circuit $U_{\text{S},y}$ outputs the coefficient polynomial corresponding to the specified index $d$ in a single coherent procedure, without intermediate measurements. III.3.3 Quantum pseudo-division by constructing remainder circuit *[Error downloading image: .//fig-qp-unitary-detail.pdf]* Figure S5: The quantum circuit $U_{\text{R},y}$ representing the polynomial R obtained by pseudo-dividing S by T with respect to the variable $y$ , as defined in Eq. (S24). a, The quantum circuit of ${U_{\text{S},y}}$ in Eq. (S39). The qubits encoding the variables $\bf{x}$ are omitted for brevity, and the state $\left|{\sum\limits_{\bf{i}}^{\bf{I}}{\text{s}({\bf{i}},d)\prod\limits_{k}^{\text{K}}{x_{k}^{{i_{k}}}}}}\right\rangle$ is abbreviated as $\left|{\text{s}({\bf{i}},d)}\right\rangle$ . b, Constructing ${U_{\text{R},y}}$ with ${U_{\text{S},y}}$ , ${U_{\text{T},y}}$ , and basic arithmetic circuits. The circuits $U_{+}$ , $U_{-}$ , and $U_{×}$ implement addition, subtraction, and multiplication for the input states, respectively. The states in the red boxes are the input states and those in the green boxes are the output states of ${U_{\text{R},y}}$ . The remaining qubits are auxiliary qubits that are prepared onto the desired states (purple boxes) with one layer of single-qubit gates. These auxiliary qubits that end with states in blue boxes can be reset to $\left|{\bf{0}}\right\rangle$ by applying appropriate inverse circuits. c, Simplified representation of the quantum circuit $U_{\text{R},y}$ , serving as a compact abbreviation of the full construction shown in b. We use the two polynomials S and T defined in Eq. (S22) to illustrate the circuit-based quantum pseudo-division procedure. The polynomial R, obtained by pseudo-dividing S by T with respect to the variable $y$ , is represented by the quantum circuit $U_{\text{R},y}$ . As shown in Fig. S5 b, this circuit is assembled from $U_{\text{S},y}$ and $U_{\text{T},y}$ together with a set of basic arithmetic circuits. In Fig. S5 b, registers shown in red correspond to input states, while registers shown in green correspond to the output states of $U_{\text{R},y}$ . All remaining registers are initialized to predetermined auxiliary states, indicated by the purple boxes, which can be prepared using a single layer of single-qubit gates. For example, when $\text{D}_{\text{t}}=5$ , the state $\lvert\text{D}_{\text{t}}\rangle=\lvert 5\rangle=\lvert 101\rangle$ can be prepared from $\lvert 000\rangle$ using two Pauli- $X$ gates. Executing the circuit yields the coefficient of $y^{d}$ in R, namely $\sum\limits_{{\bf{i}},{\bf{j}}}^{{\bf{I}},{\bf{J}}}{\text{r}({\bf{i}},{\bf{j}},d)\prod\limits_{k}^{\text{K}}{x_{k}^{{i_{k}}+{j_{k}}}}}=\sum\limits_{{\bf{i}},{\bf{j}}}^{{\bf{I}},{\bf{J}}}{\left[{\text{s}({\bf{i}},d)\text{t}({\bf{j}},{\text{D}_{\text{t}}})-\text{t}({\bf{j}},d+{\text{D}_{\text{t}}}-{\text{D}_{\text{s}}})\text{s}({\bf{i}},{\text{D}_{\text{s}}})}\right]\prod\limits_{k}^{\text{K}}{x_{k}^{{i_{k}}+{j_{k}}}}}$ shown in the green box. *[Error downloading image: .//fig-reset-auxiliary-ury.pdf]* Figure S6: The quantum circuit that resets the auxiliary qubits in the construction of $U_{\text{R},y}$ shown in Fig. S5 b. The states in the blue boxes directly correspond to the terminal state of auxiliary qubits in Fig. S5 b. After the reset procedure, each multi-qubit auxiliary register represented by a single wire in this figure is in one of the states $\left|\bf{0}\right\rangle$ , $\left|{{\text{D}_{\text{s}}}}\right\rangle$ , and $\left|{{\text{D}_{\text{t}}}}\right\rangle$ . All of these states can be reset to $\left|\mathbf{0}\right\rangle$ using no more than one layer of single-qubit gates. The state $\left|d\right\rangle$ in the green boxes is the output state of $U_{\text{R},y}$ , which remain unchanged in this reset process. At this stage, the auxiliary qubits may be reset for subsequent operations, although such a reset is not strictly necessary. After the circuit in Fig. S5 b is executed, the auxiliary qubits are in the states $\left|{{\text{D}_{\text{s}}}}\right\rangle$ , $\left|{{\text{D}_{\text{t}}}}\right\rangle$ , $\left|{d+{\text{D}_{\text{t}}}-{\text{D}_{\text{s}}}}\right\rangle$ , $\left|{\text{s}\left({{\bf{i}},{\text{D}_{\text{s}}}}\right)}\right\rangle$ , $\left|{\text{t}\left({{\bf{j}},{\text{D}_{\text{t}}}}\right)}\right\rangle$ , $\left|{\text{s}\left({{\bf{i}},d}\right)}\right\rangle$ , $\left|{\text{t}\left({{\bf{j}},d+{\text{D}_{\text{t}}}-{\text{D}_{\text{s}}}}\right)}\right\rangle$ , and $\left|{\text{t}\left({{\bf{j}},d+{\text{D}_{\text{t}}}-{\text{D}_{\text{s}}}}\right)\text{s}\left({{\bf{i}},{\text{D}_{\text{s}}}}\right)}\right\rangle$ , as shown in the blue boxes in Fig. S5 b. These qubits can be reset to $\lvert\bf{0}\rangle$ using the unitaries already present in Fig. S5 b and their inverses. The explicit reset procedure is shown in Fig. S6. IV Polynomial identity testing on quantum computers Polynomial identity testing (PIT) is the problem of deciding whether a multivariate polynomial $\text{P}(x_{1},...,x_{n})$ over a field $\mathbf{F}$ is identically zero. In computational settings, P is typically specified implicitly, for example via an arithmetic circuit or a straight-line program, and the algorithm is allowed to evaluate P at chosen input points. The goal of PIT is to determine whether $\text{P}\equiv 0$ using as few evaluations as possible [18, 62, 80]. The algorithmic study of polynomial identity testing naturally splits into two distinct categories: randomized PIT and deterministic PIT. In the randomized setting, the algorithm is allowed to use randomness to select evaluation points and may err with small probability. This model leads to simple and efficient algorithms based on random sampling and underlies most practical PIT procedures. In contrast, deterministic PIT asks for a fixed, explicitly constructed set of evaluation points that certifies whether a given polynomial is identically zero, with no probability of error. Despite its conceptual simplicity, deterministic PIT is significantly more challenging and is closely connected to open problems in algebraic complexity theory [42]. The most widely used randomized algorithms for PIT are based on the Schwartz–Zippel lemma [62, 80, 18] and its variants, which guarantee correctness with high probability using only a small number of random evaluations. These algorithms run in polynomial time and achieve exponentially small error probabilities with minimal randomness. On the other hand, no general polynomial-time deterministic algorithm is known for PIT when the polynomial is given by an arithmetic circuit. Strong derandomization of PIT is known to imply circuit lower bounds [42]. In particular, a deterministic polynomial-time PIT algorithm for general arithmetic circuits would imply that either $NEXP\not⊂ P/poly$ or the permanent does not admit polynomial-size arithmetic circuits. The central tool underlying randomized polynomial identity testing is the Schwartz–Zippel lemma. Let $\text{P}(x_{1},...,x_{n})$ be a nonzero multivariate polynomial over a field $\mathbf{F}$ with total degree at most D, and let $\text{G}⊂eq\mathbf{F}$ be a finite subset. The Schwartz–Zippel lemma states that if a point $\mathbf{a}=(a_{1},...,a_{n})$ is sampled uniformly at random from G, then the probability that $\text{P}(\mathbf{a})=0$ is at most $\text{D}/|\text{G}|$ . This bound depends only on the total degree of the polynomial and the size of the sampling set, and is independent of the number of variables. The proof of the Schwartz–Zippel lemma proceeds by induction on the number of variables $n$ . In the base case $n=1$ , the statement reduces to the elementary fact that a nonzero univariate polynomial of degree at most D has at most D roots. Consequently, when sampling uniformly from G, the probability of evaluating to zero is at most $\text{D}/|\text{G}|$ . For the inductive step, we consider a nonzero polynomial $\text{P}(x_{1},...,x_{n})$ of total degree at most D, and regard it as a univariate polynomial in the variable $x_{n}$ . We write $\text{P}(x_{1},...,x_{n})=\sum_{k=0}^{d}\text{Q}_{k}(x_{1},...,x_{n-1})x_{n}^{k}$ , where $d≤\text{D}$ is the degree of P in $x_{n}$ , and the leading coefficient $\text{Q}_{d}$ is not identically zero. Each coefficient polynomial $\text{Q}_{k}$ depends only on the first $n-1$ variables. Now sample $(a_{1},...,a_{n-1})$ uniformly at random from G. By the induction hypothesis, the probability that $\text{Q}_{d}(a_{1},...,a_{n-1})=0$ is at most $(\text{D}-d)/|\text{G}|$ , since the total degree of $\text{Q}_{d}$ is at most $\text{D}-d$ . Conditioned on the event that $\text{Q}_{d}(a_{1},...,a_{n-1})≠ 0$ , the polynomial $\text{P}(a_{1},...,a_{n-1},x_{n})$ becomes a nonzero univariate polynomial in $x_{n}$ of degree $d$ , which therefore has at most $d$ roots. Sampling $a_{n}$ uniformly from G then yields $\text{P}(a_{1},...,a_{n})=0$ with probability at most $d/|\text{G}|$ . Combining these two cases gives an overall failure probability bounded by $\text{D}/|\text{G}|$ , completing the inductive proof. The Schwartz–Zippel lemma immediately yields an efficient randomized algorithm for PIT. One samples a point uniformly from G and evaluates P at that point. If the result is nonzero, one can conclude that P is not identically zero. Repeating this procedure independently $m$ times reduces the error probability to at most $(\text{D}/|\text{G}|)^{m}$ . Thus, by choosing $|\text{G}|$ sufficiently large and repeating the test a logarithmic number of times, one obtains an algorithm with exponentially small error probability using only a small number of evaluations. Despite the effectiveness of randomized algorithms, deterministic polynomial identity testing remains a fundamental open problem. In the deterministic setting, one must specify a fixed evaluation set that certifies nonzeroness for all nonzero polynomials in a given circuit class, equivalently an explicit hitting set. For general arithmetic circuits, no polynomial-time deterministic PIT algorithm is known. Moreover, deterministic PIT for general arithmetic circuits is widely believed to be computationally intractable, even in the presence of nondeterminism. Deterministic PIT has been achieved only for restricted circuit classes, such as sparse polynomials and depth-bounded circuits, where additional algebraic structures can be exploited to construct explicit hitting sets [65]. These results do not extend to general arithmetic circuits and highlight the sharp contrast between randomized and deterministic regimes. Polynomial identity testing on quantum computers can be formulated in a manner analogous to the classical randomized approach but with the evaluation procedure embedded coherently into a quantum circuit. Given a quantum circuit $U_{\text{P}}$ that evaluates a polynomial P on inputs from a finite set G, the task of PIT reduces to deciding whether there exists a point $\mathbf{a}∈ G$ such that $\text{P}(\mathbf{a})≠ 0$ . Although quantum algorithms can offer significant speedups for certain search and sampling tasks, they do not fundamentally alter the derandomization landscape of polynomial identity testing. The core obstacle in deterministic PIT lies in the explicit construction of hitting sets that certify nonzeroness for all nonzero polynomials in a given circuit class. This requirement is inherently combinatorial and algebraic, rather than algorithmic, and is not addressed by quantum algorithms [51]. In the randomized setting, PIT already admits highly efficient classical algorithms based on the Schwartz–Zippel lemma, achieving exponentially small error probabilities with only a constant number of evaluations. In this regime, quantum algorithms cannot provide an asymptotic improvement, since the classical query complexity is already minimal. On the other hand, in the deterministic setting, quantum computation does not circumvent the need for explicit hitting sets. Quantum search algorithms, such as the Grover algorithm, can only provide probabilistic guarantees and therefore cannot yield deterministic identity tests. Consequently, while quantum algorithms can yield a quadratic improvement in query complexity when searching for nonzero evaluations over a prescribed finite set, they do not resolve the central challenge of deterministic PIT. In particular, quantum computation does not bypass the structural barriers underlying derandomization, nor does it eliminate the complexity-theoretic consequences associated with deterministic polynomial identity testing.