Paper deep dive
Proving olympiad geometry theorems on a superconducting quantum processor
Ning Wang, Zheng-Zhi Sun, Zhengyi Cui, Yiren Zou, Aosai Zhang, Fanhao Shen, Jiarun Zhong, Zehang Bao, Zitian Zhu, Han Wang, Jia-Nan Yang, Jiayuan Shen, Gongyu Liu, Yanzhe Wang, Yihang Han, Yiyang He, Jiahua Huang, Sailang Zhou, Xinrong Zhang, Yaozu Wu, Zixuan Song, Jinfeng Deng, Hang Dong, Qi Ye, Weikang Li, Si Jiang, Yixuan Ma, Shuangyue Geng, Zhide Lu, Chao Song, Hekang Li, Pengfei Zhang, Qiujiang Guo, H. Wang, Dong-Ling Deng
Intelligence
Status: not_run | Model: - | Prompt: - | Confidence: 0%
Entities (0)
Relation Signals (0)
No relation signals yet.
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
Abstract:Automated theorem proving seeks to use computational systems to prove or disprove mathematical and logical statements [1, 2]. It underpins a wide range of applications, and enhancing theorem-proving capabilities remains a central objective in artificial intelligence [3]. Although recent neuro-symbolic systems have achieved remarkable progress [4-7], their operation is ultimately constrained by classical computational architectures. Quantum computing [8], by contrast, enables information encoding and coherent parallelism beyond classical limits [9-14], raising the possibility of accelerating structured symbolic deduction [15]. Here we report the experimental realization of automated geometry theorem proving on a fully programmable superconducting quantum processor. We develop two complementary quantum proving frameworks. The first implements Wu's algebraic elimination method using quantum pseudo-division, with multivariate polynomials represented in superposition states, enabling quantum algebraic theorem proving. The second implements the full-angle method as backward symbolic reasoning through a hybrid quantum strategy-guided architecture, demonstrating a general route toward quantum symbolic proof search. As illustrative examples, we prove two theorems on a superconducting quantum processor: the perpendicularity of the diagonals of a square and a 1978 International Mathematical Olympiad geometry problem. Our results establish, at the experimental level, automated logical reasoning as a viable task for near-term quantum processors and provide a concrete pathway toward quantum-enhanced symbolic intelligence.
Tags
Links
- Source: https://arxiv.org/abs/2609.14533v1
- Canonical: https://arxiv.org/abs/2609.14533v1
Trouble viewing inline? Open PDF directly →
Full Text
170,203 characters extracted from source content.
Expand or collapse full text
Proving olympiad geometry theorems on a superconducting quantum processor Ning Wang1 Thanks: These authors contributed equally to this work. Zheng-Zhi Sun2 Thanks: These authors contributed equally to this work. Zhengyi Cui1 Yiren Zou1 Aosai Zhang1 Fanhao Shen1 Jiarun Zhong1 Zehang Bao1 Zitian Zhu1 Han Wang1 Jia-Nan Yang1 Jiayuan Shen1 Gongyu Liu1 Yanzhe Wang1 Yihang Han1 Yiyang He1 Jiahua Huang1 Sailang Zhou1 Xinrong Zhang1 Yaozu Wu1 Zixuan Song1 Jinfeng Deng1 Hang Dong1 Qi Ye2 Weikang Li2 Si Jiang2 Yixuan Ma2 Shuangyue Geng2 Zhide Lu4 Chao Song1,3 Email: chaosong@zju.edu.cn Hekang Li1,3 Pengfei Zhang1,3 Qiujiang Guo1,3 H. Wang1,3 Email: hhwang@zju.edu.cn Dong-Ling Deng2,4,3 Email: dldeng@tsinghua.edu.cn Abstract Automated theorem proving seeks to use computational systems to prove or disprove mathematical and logical statements [19, 46]. It underpins a wide range of applications, and enhancing theorem-proving capabilities remains a central objective in artificial intelligence [29]. Although recent neuro-symbolic systems have achieved remarkable progress [62, 26, 33, 24], their operation is ultimately constrained by classical computational architectures. Quantum computing [53], by contrast, enables information encoding and coherent parallelism beyond classical limits [3, 65, 47, 69, 21, 39], raising the possibility of accelerating structured symbolic deduction [61]. Here we report the experimental realization of automated geometry theorem proving on a fully programmable superconducting quantum processor. We develop two complementary quantum proving frameworks. The first implements Wu’s algebraic elimination method using quantum pseudo-division, with multivariate polynomials represented in superposition states, enabling quantum algebraic theorem proving. The second implements the full-angle method as backward symbolic reasoning through a hybrid quantum strategy-guided architecture, demonstrating a general route toward quantum symbolic proof search. As illustrative examples, we prove two theorems on a superconducting quantum processor: the perpendicularity of the diagonals of a square and a 1978 International Mathematical Olympiad geometry problem. Our results establish, at the experimental level, automated logical reasoning as a viable task for near-term quantum processors and provide a concrete pathway toward quantum-enhanced symbolic intelligence. Automated theorem proving is a central challenge in artificial intelligence and a crucial tool for formal verification [29]. Geometry provides an intuitive yet demanding setting: its statements are readily visualized, but their proofs require precise representations and rigorous chains of deduction. Wu’s method translates geometric relations into polynomial equations and establishes conclusions by algebraic elimination under suitable non-degeneracy conditions [64]. The full-angle method instead constructs readable proofs by manipulating relations between angles [9]. Recent neuro-symbolic systems, such as AlphaGeometry [62] and TongGeometry [68], combine neural guidance with symbolic deduction to solve challenging International Mathematical Olympiad (IMO) geometry problems [62, 68], alongside broader advances in learning-based mathematical reasoning [26, 33]. Despite these advances, automated theorem proving in geometry may still face a fundamental scalability barrier: the size of intermediate expressions and the number of candidate inference steps can grow rapidly with problem complexity, imposing unattainable time and memory costs on classical computers. Quantum computing, grounded in the principles of quantum mechanics, provides a fundamentally different substrate for information processing [53]. By leveraging peculiar quantum features, such as superposition and entanglement, quantum processors would manipulate information in parallel in exponentially large Hilbert spaces, allowing unparalleled opportunity for addressing the scalability challenge in classical automated theorem proving. In recent years, exciting progress has been achieved across multiple quantum hardware platforms, including programmable superconducting circuits [3, 65, 40, 38, 66, 35], trapped ions [18, 50], photonic systems [69, 47], and Rydberg-atom arrays [17, 6]. These advances, together with developments in experiments exhibiting quantum computational advantage [3, 69, 65, 47] and demonstrating quantum error correction [23, 59, 52, 6, 27, 22, 63, 41], are steadily pushing quantum devices toward regimes where increasingly complex and noise-resilient computations become feasible. Parallel to these developments, the intersection of quantum computing and machine learning has given rise to a new research frontier of quantum machine learning [5, 15, 13, 7, 43]. A variety of quantum learning algorithms with potential advantages have been proposed [28, 45, 16, 20, 44, 34] and some of them have been demonstrated in proof-of-principle experiments [30, 31, 32, 54]. More recently, a theoretical framework for quantum automated theorem proving has been introduced, extending quantum computation beyond predominantly numerical tasks to structured symbolic reasoning [61]. Within this framework, generic reasoning problems admit a quadratic quantum speedup. Yet, experimental demonstration of quantum automated theorem proving remains a notable challenge and has not been reported so far. Fig. 1: The quantum processor and overview of quantum automated theorem proving. a, Superconducting quantum processor used in the experiments. The qubits marked in purple are selected to implement the quantum reasoning circuits. b, Overview of quantum automated theorem proving. Automated theorem proving seeks to derive a target conclusion G from a set of hypotheses ℋH through formally valid inference. The geometry configuration shown is taken from a problem of the 1978 IMO and serves as an illustrative example. The hypotheses and conclusion are translated into exact formal representations, including polynomial equations and full-angle relations, and subsequently encoded into quantum registers. Quantum circuits implement inference and evaluation, with the outcome classified as proved, disproved or undetermined according to the corresponding termination criterion. c, Deterministic algebraic reasoning based on Wu’s method. The hypotheses are represented by the polynomial knowledge base H1=0,H2=0,…,HN=0H_1=0,H_2=0,…,H_N=0, and the conclusion by the goal polynomial G. Successive quantum pseudo-division (QPD) operations reduce G through a sequence of pseudo-remainders, with a vanishing final pseudo-remainder establishing the conclusion (Supplementary Information Sec.1). d, Symbolic proof search. The strategy circuit generates an inference action AtA_t that transforms the proof state |St⟩ S_t into a candidate output |St+1⟩ S_t+1 . The action and candidate output are encoded as coherent superpositions of inference operations and proof states, respectively. We use an evaluation circuit to estimate the value function for the candidate output and iteratively optimize the strategy circuit. The resulting state |St+1⟩ S_t+1 is used in the next reasoning round (see Supplementary Information Sec.2 for an in-depth discussion). Here we report an experimental realization of quantum automated theorem proving on a programmable superconducting quantum processor (Fig. 1a), using geometry theorems serving as representative examples. We experimentally realize two complementary forms of quantum reasoning, spanning algebraic and symbolic deduction. For algebraic deduction, we map the pseudo-division procedure of Wu’s method onto quantum circuits and demonstrate the complete proof workflow using the perpendicularity of the diagonals of a square as a benchmark. For symbolic deduction, we combine the full-angle representation with a hybrid quantum-classical proof-search architecture. A parameterized quantum circuit proposes inference actions, while a fixed reasoning circuit implements the underlying formal rules. The resulting procedure constructs a human-readable proof of a geometry problem from the 1978 IMO. Together, these experiments demonstrate that programmable quantum processors can carry out structured formal reasoning and establish an experimental basis for quantum automated theorem proving and symbolic intelligence. Fig. 2: Demonstration of quantum algebraic theorem proving with a square geometry problem. a, Coordinate representation of the square ABCDABCD, with A=(0,0)A=(0,0), B=(x1,0)B=(x_1,0), C=(x3,x2)C=(x_3,x_2) and D=(x5,x4)D=(x_5,x_4). b, Polynomial formulation of the theorem. The geometric hypotheses AB⟂ADAB AD, AB|CDAB CD, AD|BCAD BC and AB=BCAB=BC are represented by the polynomials H1(),…,H4()H_1( x),…,H_4( x), and the conclusion AC⟂BDAC BD by the polynomial G()G( x), where =(x1,x2,…,x5) x=(x_1,x_2,…,x_5). c, Algebraic proof by successive pseudo-division. The variables x5x_5, x4x_4, x3x_3 and x2x_2 are eliminated sequentially using H1H_1, H2H_2, H3H_3 and H4H_4, respectively. The resulting pseudo-remainder chain terminates at R4()=0R_4( x)=0, establishing the conclusion. d, The conceptual quantum circuit for dividing polynomial P by Q. We partition all nine registers into three groups for storing different information of the two polynomials and have already initialized their states as annotated. The boldface label |⟩|0 denotes the all-zero state of the corresponding register, which may comprise multiple qubits. At the beginning, we modify the fourth exponent register by controlled UsU_s for the subsequent second controlled UQU_Q operation. Then we write four value registers by controlled unitary UPU_P or UQU_Q based on the shared point and corresponding exponent registers, and apply quantum arithmetic operations on two of them. Lastly, we measure the necessary registers to reconstruct the resulting polynomial. In the right gray box, we show the functions of all controlled unitary gates involved in the quantum circuit. e-f, The experimental point-value correspondence of the first and final step. As shown in e (f), these results are classified into two (three) sectors depending on the value of d and the x-axis labels the joint states of point qubits |x1x2x3x4⟩|x_1x_2x_3x_4 (|x1⟩|x_1 ). The joint states of the measured value register are depicted on the left side, with their corresponding encoded values shown on the right side. Colors indicate the probability obtained from 3000 runs of measurements, with each run taking 3000 shots. Framework and experimental setup Quantum automated theorem proving addresses problems defined by a set of hypotheses ℋ=ℋ1,ℋ2,…H=\H_1,H_2,…\ and a target conclusion G (Fig. 1b). The mathematical statements are first cast into exact formal representations suitable for quantum processing. The resulting knowledge, proof states and inference operations are encoded in quantum registers, allowing formal reasoning and evaluation to be implemented through quantum circuits. Depending on the reasoning procedure and its termination criterion, the computation may prove the conclusion, disprove it or return an undetermined outcome [61]. This framework supports two complementary approaches. In algebraic reasoning, mathematical statements that admit polynomial formulations are processed through quantum polynomial operations, with the final result certified by an algebraic termination criterion (Fig. 1c). In strategy-guided symbolic proof search, a quantum knowledge base and the current proof state are processed by strategy, reasoning and evaluation circuits to identify a sequence of formally valid inference steps (Fig. 1d). The resulting proof state can be passed directly to the subsequent reasoning step without extracting and re-encoding the intermediate statement. More generally, retaining knowledge and proof states in quantum form provides a route towards coherent proof search, in which superpositions of candidate actions and reasoning paths could be maintained and processed across multiple inference steps. The detailed representations and circuit constructions are introduced in the following sections. Our experiments are performed on a two-dimensional (2D) flip-chip superconducting quantum processor comprising 121 frequency-tunable transmon qubits arranged in an 11×1111× 11 square lattice (Fig. 1a). Nearest-neighbour interactions are mediated by 220 tunable couplers, and the processor supports arbitrary single-qubit rotations, two-qubit controlled-phase gates and frequency-multiplexed dispersive readout. Connected subsets of qubits are selected to implement the reasoning circuits, which are compiled into the native gate set with multi-qubit operations and qubit layouts optimized to reduce circuit depth. The fidelity performance of simultaneous single-qubit gates, two-qubit gates, and measurement gates are better than 99.9%99.9\%, 99%99\%, and 98%98\%, respectively. More detailed device parameters, calibration procedures and compilation methods are provided in the Supplementary Information Sec.3. Quantum algebraic theorem proving We present quantum algebraic theorem proving by mapping polynomial deduction onto a sequence of quantum pseudo-divisions (QPD) [61]. We implement Wu’s method on the superconducting quantum processor, using a proof of the perpendicularity of the diagonals of a square as an example (Fig. 2a). The coordinates of four corner points A-D are parameterized by the variables =(x1,x2,…,x5) x=(x_1,x_2,…,x_5), and the geometric hypotheses together with the target conclusion are translated into multivariate polynomial equations (Fig. 2b). The proof comprises four QPD steps, each of which reduces the current polynomial using one of the hypothesis polynomials and eliminates one variable (Fig. 2c). The vanishing of the final pseudo-remainder establishes the conclusion [61]. We encode each polynomial in the point-value form [61]. For a polynomial P whose leading variable is to be eliminated, the coefficient associated with each power of that variable is regarded as a polynomial in the remaining variables and evaluated at a set of sampling points sufficient to determine it uniquely. The exponent, sampling point and corresponding coefficient value are stored in separate quantum registers, with a controlled unitary UPU_P writing the coefficient value according to the exponent and point inputs. The divisor polynomial Q is encoded in the same manner. To perform pseudo-division, we shift the exponent of Q by the difference between the leading degrees of P and Q, aligning the terms to be eliminated. Quantum multiplication and subtraction are then applied to the matched coefficient values, canceling the leading term of P and producing the point-value representation of the pseudo-remainder (Fig. 2d). This construction reduces polynomial manipulation to arithmetic operations on pointwise values and avoids identifying and collecting like terms in a coefficient-based quantum representation. In the present implementation, the point values are precomputed classically and embedded into the controlled unitaries, whereas the arithmetic operations required for pseudo-division are executed on the quantum processor. For the experimental implementation, the controlled unitaries UPU_P and UQU_Q in each step are compiled into elementary single- and two-qubit gates according to the available qubit connectivity and the required input-output relations. Auxiliary registers are introduced to store duplicated intermediate information, allowing part of the controlled operations to be executed in parallel and thereby reducing the circuit depth. For step 1, the resulting circuit is implemented on 2121 qubits and contains 7777 layers, including 150150 single-qubit gates and 8989 two-qubit gates. In this step, the two polynomials are P()=x3x5+(x2x4−x1x3)x50P( x)=x_3x_5+(x_2x_4-x_1x_3)x_5^0 and Q()=x5Q( x)=x_5, with x5x_5 as the leading variable to be eliminated. Since the exponent of x5x_5 takes only the values 00 and 11, the exponent register is encoded by a single qubit. The point register uses four qubits to encode the N=24N=2^4 computational-basis states |x1x2x3x4⟩ x_1x_2x_3x_4 , where xi∈0,1x_i∈\0,1\. For each assignment, the controlled unitaries UPU_P and UQU_Q write the corresponding coefficient values of P()P( x) and Q()Q( x) into two two-qubit value registers, whose ranges cover all coefficient values occurring in this step. After encoding, pseudo-division is implemented through arithmetic multiplication and subtraction on the encoded coefficient values. This removes the highest-exponent term of P()P( x), so that the coefficient of the exponent-one term in the resulting polynomial becomes zero in the output. The updated coefficients are read out by joint measurement of the exponent, point, and value registers (Supplementary Information Sec. 1). The measurement outcomes of step 1 give the joint occupation probabilities of the seven measured qubits required to reconstruct the pseudo-remainder, shown as 272^7 coloured squares in Fig. 2e. The left and right groups correspond to the exponent qubit in states |0⟩|0 and |1⟩|1 , respectively, while the x- and y-axes label the joint states of the point and value registers. The coefficient value represented by each two-qubit value state is indicated along the right-hand side. For each point index, the coefficient is identified from the value state with the largest probability, since the polynomial assigns a unique output to each input point. In the |1⟩|1 sector, the values are zero for all sampled points, and the reconstructed coefficient is therefore zero, showing that the exponent-one term has been eliminated. In the |0⟩|0 sector, the reconstructed values yield the output polynomial R1()=x2x4−x1x3R_1( x)=x_2x_4-x_1x_3, consistent with the theoretical result of the pseudo-division step. The output polynomial is then reordered with a new leading variable and processed with the next geometric equation. Repeating this procedure with the remaining hypothesis polynomials yields the final measurement results shown in Fig. 2f. Additional results for steps 2 and 3 are provided in the Supplementary Information Sec.3. For each of the three exponent sectors and all three sampling points in the final step, the dominant probability is observed in the value state encoding zero, such that all reconstructed coefficients vanish and the final pseudo-remainder is R4()=0R_4( x)=0. Together, the four QPD circuits realize a complete algebraic deduction of the desired conclusion that diagonals of a square are perpendicular. We remark that a quantum implementation of Wu’s method can, in principle, achieve a quadratic reduction in query complexity [61]. In the present experiment, however, hardware imperfections limit the accessible circuit size and depth, and this advantage has not yet been demonstrated. Demonstrating the predicted scaling would require larger, deeper circuits supported by higher-fidelity quantum hardware and potentially fault-tolerant operations. We leave this for future study. Quantum symbolic proof search Fig. 3: Proving an IMO geometry theorem. a, Problem 4 of the 1978 IMO, together with its geometric configuration and a proof expressed in the full-angle formalism. b, Quantum circuit for a single proof-search round. The circuit consists of a parameterized strategy circuit, a fixed reasoning circuit and an evaluation circuit. Two action qubits encode the candidate inference operations, five qubits encode the input proof state |ψ⟩|ψ , and another five qubits encode the output proof state. The action register is initialized in |0⟩⊗2|0 2, and the output register in |0⟩⊗5|0 5. The input proof states are |00111⟩|00111 , |00000⟩|00000 and |01001⟩|01001 in rounds 1, 2 and 3, respectively. The left gray box shows the parameterized single-qubit gate sequence on θj _j and θj+1 _j+1 used in the strategy circuit. c, Experimental training trajectories of the loss in the three proof-search rounds. Training is terminated when the standard deviation of the four most recent loss values falls below 0.0050.005. Error bars denote the standard error of the mean over 10 repeated runs, each with 1,000 shots. The loss is obtained from measurements of the registers enclosed by the blue box in b. d, Experimental probability distributions of the action-register states in the three rounds. The dominant outcomes select the three successive transformations used in the proof. Probabilities are obtained from 10 repeated measurements of the action register, each with 1,000 shots. e, Experimental probability distributions of the output full-angle states in the three rounds. The horizontal and vertical axes label the encoded sign and first line, and the second line, respectively, with the corresponding geometric meanings indicated along the axes. The dominant outputs are ∠[HD,FD] [HD,FD], ∠[FD,DB] [FD,DB] and −∠[HB,CB]- [HB,CB] in rounds 1, 2 and 3, respectively. Colours denote probabilities obtained from 10 repeated measurements of the registers enclosed by the green box in b, each with 1,000 shots. The above algebraic elimination follows a prescribed reduction order. We now introduce quantum symbolic proof search, in which the sequence of inference steps is determined as reasoning proceeds rather than prescribed in advance. At reasoning round t, the current stage of the derivation is encoded as a quantum proof state |St⟩ S_t , and formal inference rules define the admissible transitions between proof states. Based on |St⟩ S_t , the parameterized strategy circuit generates an action state over candidate inference operations. The action state controls a fixed reasoning circuit that coherently applies the corresponding rules and produces the candidate output state |St+1⟩ S_t+1 . An evaluation circuit assesses the resulting transitions and defines the objective used to optimize the strategy circuit. The trainable strategy circuit enables flexible exploration of the proof space, whereas the fixed reasoning circuit restricts state transitions to those permitted by the formal inference rules. The quantum components operate coherently, preserving superpositions of inference operations and proof states throughout the reasoning process. Repeated reasoning steps generate a sequence of proof states that gives an explicit symbolic proof when the goal is reached (Fig. 1d and see Supplementary Information Sec. 2 for details). We demonstrate this procedure on Problem 4 of the 1978 IMO (Fig. 3a). For an isosceles triangle ABCABC with AB=ACAB=AC, a circle is tangent to the sides ABAB and ACAC at F and G and internally tangent to the circumcircle. The goal is to show that the midpoint H of FGFG is the incenter of ABCABC. Let D be the point of tangency of the two circles. A full-angle ∠[u,v] [u,v] is the directed angle from line u to line v, taken modulo π. In the non-degenerate configuration shown, H lies inside the triangle and, by symmetry, on the internal bisector at A. The remaining angle-bisector condition at B is therefore expressed as ∠[HB,BA]+∠[HB,CB]=0 [HB,BA]+ [HB,CB]=0. From the relations derived classically from the hypotheses, we retain three equalities: ∠[HD,FD]=∠[FD,DB] [HD,FD]= [FD,DB], ∠[HB,BA]=∠[HD,FD] [HB,BA]= [HD,FD] and ∠[FD,DB]=−∠[HB,CB] [FD,DB]=- [HB,CB]. The action states |00⟩ 00 , |01⟩ 01 and |10⟩ 10 encode these equalities, respectively. This leads to the proof sequence ∠[HB,BA]→|01⟩∠[HD,FD] [HB,BA] 01 [HD,FD] →|00⟩∠[FD,DB] 00 [FD,DB] (1) →|10⟩−∠[HB,CB]. 10 - [HB,CB]. The remaining basis state |11⟩ 11 of the two-qubit action register is unused. To reduce the circuit overhead, the three selected relations are compiled directly into the reasoning circuit. Each action implements the corresponding equality as a directed transformation from its left-hand side to its right-hand side. The input and output proof states are stored in two five-qubit registers. In each register, the first qubit encodes the sign, and two pairs of qubits encode the two lines defining the full-angle (Supplementary Information Sec. 2). Each proof-search round comprises a parameterized strategy circuit, a fixed reasoning circuit and an evaluation circuit (Fig. 3b). In the strategy circuit, every action qubit is coupled to all four line-index qubits in the input proof-state register, thereby correlating action selection with the current proof state. The reasoning circuit first copies the input proof state to the output register and then conditionally performs the transformation specified by the action state. If the selected rule is not applicable to the input proof state, the output remains unchanged. The evaluation circuit compares the input and output proof states, favouring actions that produce a non-trivial state update while suppressing population in the unused state |11⟩ 11 . Its output defines the loss used to optimize the strategy circuit. The proof search is initialized with ∠[HB,BA] [HB,BA]. In each round, the strategy circuit is optimized for the current proof state, after which the action and output registers are measured. The dominant output full-angle is used as the input to the subsequent round. Three rounds are sufficient to complete the proof. The loss decreases throughout each optimization process (Fig. 3c), while the measured action distributions are dominated by |01⟩ 01 , |00⟩ 00 and |10⟩ 10 in the three successive rounds (Fig. 3d). The corresponding output distributions exhibit dominant peaks at ∠[HD,FD] [HD,FD], ∠[FD,DB] [FD,DB] and −∠[HB,CB]- [HB,CB] (Fig. 3e). These results reconstruct the sequence in Eq. (1) and establish the target identity ∠[HB,BA]+∠[HB,CB]=0 [HB,BA]+ [HB,CB]=0. Conclusion and outlook We have experimentally demonstrated quantum automated theorem proving on a programmable superconducting processor through two complementary forms of formal reasoning. In the algebraic approach, polynomial deduction is mapped to quantum pseudo-division, and the conclusion is certified by the vanishing of the final pseudo-remainder. In the symbolic approach, proof states, inference actions and formal rules are encoded in quantum states and quantum circuits, allowing a proof path to be constructed through successive symbolic transformations. Using representative geometry problems, including a problem from the 1978 IMO, we implement both procedures on quantum hardware and obtain either an algebraic certificate or an explicit symbolic proof. These results show that structured mathematical reasoning can be formulated as an executable quantum process rather than merely verified through classical post-processing. The present experiments operate on polynomial instances of limited size and a restricted set of symbolic relations, with the proof state measured and re-prepared between successive reasoning rounds. These restrictions arise from the available hardware resources rather than from the structure of the framework itself. Larger knowledge bases and richer rule sets can be incorporated by extending the state registers and compiling additional inference operations into the reasoning circuit. Passing the output proof state directly to subsequent reasoning steps would preserve superpositions of inference actions and proof paths throughout a multi-step derivation, allowing increasingly complex spaces of formally valid deductions to be processed within the same quantum architecture. By extending quantum computing beyond numerical tasks to verifiable symbolic reasoning, our work makes a first experimental step towards quantum automated theorem proving and, more broadly, quantum symbolic intelligence. Methods Point-value representation and quantum pseudo-division For each elimination step, we partition the complete set of geometric variables as =(,y) x=( z,y), where y is the variable to be eliminated and z collects the remaining variables. The dividend P and divisor Q are expressed as univariate polynomials in y: P(,y) P( z,y) =∑d=0DPpd()yd, = _d=0^D_Pp_d( z)y^d, Q(,y) Q( z,y) =∑d=0DQqd()yd, = _d=0^D_Qq_d( z)y^d, (2) where DPD_P and DQD_Q are their respective degrees in y, and pd()p_d( z) and qd()q_d( z) are coefficient polynomials in the remaining variables. We represent these coefficient polynomials by reversible evaluation circuits [61]. The circuit associated with P implements UP,y|d⟩|⟩|⟩=|d⟩|⟩|pd()⟩, U_P,y d z 0 = d z p_d( z) , (3) for the computational-basis inputs supported by the corresponding registers. The circuit UQ,yU_Q,y is defined analogously. Thus, the exponent register selects the coefficient polynomial associated with a given power of y, while the point register specifies the input of this polynomial. When the exponent and point registers are prepared in superposition, the corresponding coefficient values are evaluated coherently and written into the value register. A pseudo-division reduction cancels the leading term of P without dividing by the leading coefficient of Q. Defining Δ=DP−DQ =D_P-D_Q, one reduction produces R(,y) R( z,y) =qDQ()P(,y)−pDP()yΔQ(,y) =q_D_Q( z)P( z,y)-p_D_P( z)y Q( z,y) =∑drd()yd, = _dr_d( z)y^d, (4) where rd()=qDQ()pd()−pDP()qd−Δ(), r_d( z)=q_D_Q( z)p_d( z)-p_D_P( z)q_d- ( z), (5) with qk()=0q_k( z)=0 for k<0k<0 or k>DQk>D_Q. In particular, the leading coefficient satisfies rDP()=0r_D_P( z)=0, and the degree of the resulting polynomial in y is reduced. The quantum pseudo-division circuit evaluates this relation coherently. An exponent-shift operation first aligns the powers of Q with those of P. The controlled circuits UP,yU_P,y and UQ,yU_Q,y then write the coefficient values pd()p_d( z), qDQ()q_D_Q( z), pDP()p_D_P( z) and qd−Δ()q_d- ( z) into separate value registers. Reversible multiplication and subtraction operations subsequently implement |d⟩|⟩|⟩⟼|d⟩|⟩|rd()⟩, d z 0 d z r_d( z) , (6) with auxiliary registers retaining the intermediate values required by the arithmetic operations. If the degree of the resulting polynomial remains no smaller than DQD_Q, the reduction can be repeated until the degree of the pseudo-remainder in y is lower than that of the divisor. For the polynomial system considered in this work, each variable-elimination step requires only one such reduction. The polynomial-dependent evaluation circuits are constructed from the corresponding coefficient functions, whereas the exponent alignment and reversible arithmetic required to obtain the pseudo-remainder are executed on the quantum processor. The resulting pseudo-remainder retains the same point-value representation and can therefore be processed by subsequent polynomial operations within the same circuit framework. In the present experiment, each elimination step is implemented separately, with the point register prepared over a finite set of inputs sufficient to determine the relevant coefficient polynomials. The measured outputs are used to identify the intermediate pseudo-remainder and prepare the representation required for the next elimination step. The polynomial pairs and input values used in the four elimination steps, together with representative theoretical and compiled circuits, are provided in the Supplementary Information Sec. 1. Quantum representation of full-angle formulas and inference actions A full-angle is specified by an ordered pair of lines [9]. In the experimental implementation, each proof state contains a signed full-angle and is represented as |S⟩=|s⟩|ℓ1⟩|ℓ2⟩, S = s _1 _2 , (7) where |s⟩ s encodes the sign of the full-angle, and |ℓ1⟩ _1 and |ℓ2⟩ _2 encode its first and second lines, respectively. The sign is stored in qubit Q1SQ^S_1, whereas the two lines are stored in the two-qubit registers Q2SQ3SQ^S_2Q^S_3 and Q4SQ5SQ^S_4Q^S_5. A separate two-qubit register Q1AQ2AQ^A_1Q^A_2 represents the inference action. The computational-basis encoding used in the experiment is summarized in Table 1. Name Qubits Value Information Action Q1AQ2AQ^A_1Q^A_2 00 ∠[HD,FD]=∠[FD,DB] [HD,FD]= [FD,DB] 01 ∠[HB,BA]=∠[HD,FD] [HB,BA]= [HD,FD] 10 ∠[FD,DB]=−∠[HB,CB] [FD,DB]=- [HB,CB] State Q1SQ^S_1 0 ++ 1 −- Q2SQ3SQ^S_2Q^S_3 00 HDHD 01 HBHB 10 FDFD Q4SQ5SQ^S_4Q^S_5 00 FDFD 01 DBDB 10 CBCB 11 BABA Table 1: Basis encoding of the action and state registers. The three valid action states encode full-angle equalities obtained from the geometric hypotheses and inference rules. In the reasoning circuit, each equality is implemented as a directed transformation from its left-hand side to its right-hand side. The remaining action state |11⟩ 11 is not assigned to an inference operation. For example, the initial proof state ∠[HB,BA] [HB,BA] is encoded as |S0⟩=|0⟩|01⟩|11⟩=|00111⟩. S_0 = 0 01 11 = 00111 . (8) This problem-specific encoding retains only the full-angles and inference actions required for the implemented proof, thereby reducing the number of qubits and the circuit depth. Quantum reasoning and evaluation circuits At reasoning round t, the strategy circuit prepares an action state |At⟩ A_t , which controls a fixed reasoning circuit acting on the input proof-state register |St⟩ S_t and a five-qubit output register initialized in |⟩ 0 . On computational-basis states, the reasoning operation is defined by UR|a⟩|St⟩|⟩=|a⟩|St⟩|S~t+1(a,St)⟩, U_R a S_t 0 = a S_t S_t+1(a,S_t) , (9) where |S~t+1(a,St)⟩ S_t+1(a,S_t) denotes the candidate proof state generated by action a. For each of the three valid actions, the corresponding full-angle equality in Table 1 is applied from left to right when the input proof state matches its left-hand side. Otherwise, the output proof state remains unchanged. By linearity, the same circuit acts coherently on superpositions of proof states and inference actions. The reasoning circuit uses two action qubits, five input-state qubits and five output-state qubits. Five CNOT gates first correlate the output register with the input register, such that each computational-basis component initially carries the same proof-state label. The action-conditioned unitary then updates the output register only when both the action and the input proof state match one of the compiled transformations. Its action can be summarized as S~t+1(a,St)=fa(St),if action a is applicable to St,St,otherwise, S_t+1(a,S_t)= casesf_a(S_t),&if action $a$ is applicable to $S_t$,\\ S_t,&otherwise, cases (10) where faf_a denotes the directed full-angle transformation associated with action a. The transformations on the remaining basis states are chosen to complete the unitary operation. This construction separates action selection from formal inference: the trainable strategy circuit determines the action amplitudes, whereas the fixed reasoning circuit implements the corresponding rule-consistent state transitions. The evaluation circuit assesses whether the candidate transition produces a new proof state and whether the selected action is valid. As shown in Fig. 3b, five CNOT gates are applied between the corresponding qubits of the input and output proof-state registers. These gates compute their bitwise difference in one of the registers, such that the measurement outcome 0000000000 occurs if and only if the two encoded proof states are identical. We define the loss function as L L =P1+P2, =P_1+P_2, (11) where P1P_1 and P2P_2 are probabilities estimated from repeated measurements of the corresponding registers. Specifically, P1 P_1 =Pr(St⊕S~t+1=00000), = \! (S_t S_t+1=00000 ), (12) P2 P_2 =Pr(At=11,St⊕S~t+1≠00000). = \! (A_t=11,S_t S_t+1≠ 00000 ). (13) The probability P1P_1 quantifies the total probability weight of same outcomes in the joint measurement of the two proof-state registers. The probability P2P_2 quantifies the probability of obtaining the unused action outcome 1111 together with unequal outcomes for the two proof-state registers, thereby excluding events already counted in P1P_1. Minimizing L therefore favours non-trivial proof-state transitions generated by the three valid actions. The resulting loss is used to optimize the parameters of the strategy circuit, while the candidate output obtained after optimization determines the proof state adopted for the subsequent reasoning round. Detailed action-conditioned transformations and gate-level constructions of the reasoning and evaluation circuits are provided in the Supplementary Information Sec. 2. Optimization of the strategy circuit The strategy circuit contains 16 trainable parameters implemented as rotation angles of RxR_x and RzR_z gates, as shown in Fig. 3b. In each reasoning round, the circuit parameters are optimized using the Adam optimizer. The gradient of the loss with respect to each parameter is evaluated using the parameter-shift rule [49], ∂L∂θj=L(θj+π/2)−L(θj−π/2)2. ∂ L∂ _j= L( _j+π/2)-L( _j-π/2)2. (14) Data availability The data presented in the figures and that support the other findings of this study will be made publicly available for download on Zenodo upon publication. Code availability The data analysis and numerical simulation codes will be made publicly available for download on Zenodo upon publication. Acknowledgements We are indebted to Vedran Dunjko for his invaluable comments and suggestions on the first version of the manuscript. We also thank Peter Zoller, Nobuyuki Yoshioka, Yasunobu Nakamura, Eric R. Anschuetz, and Haomu Yuan for discussions, and Jiachen Chen, Chuanyu Zhang, Yu Gao, Xuhao Zhu, and Feitong Jin for technical support. The device was fabricated at the Micro-Nano Fabrication Center of Zhejiang University. We acknowledge the support from the National Natural Science Foundation of China (grant nos. T2225008, 92565301, 12274368, 12404570, and 12404574), Quantum Science and Technology-National Science and Technology Major Project (grant nos. 2021ZD0300200 and 2021ZD0302203), Zhejiang Province Pioneer Plan (grant nos. 2025C01046, 2025C01019 and 2026C02A2004), and the Zhejiang Provincial Natural Science Foundation of China (grant no. LR24A040002). Z.-Z.S., Q.Y., S.J., W.L., Z.L., S.G., Y.M., and D.-L.D. acknowledge in addition support from the Tsinghua University Dushi Program and the Shanghai Qi Zhi Institute Innovation Program. Z.-Z. S. is additionally funded by China Postdoctoral Science Foundation (Certificated Number: 2025T180926). Author contributions N.W. carried out the experiments and analyzed the experimental data under the supervision of C.S. and H.Wang; Z.-Z.S., Q.Y., S.J., W.L., Y.M., S.G., Z.L., and D.-L.D. conducted the theoretical analysis; H.L. fabricated the device supervised by H.Wang; Z.-Z.S., N.W., C.S., H.Wang, and D.-L.D. co-wrote the manuscript; H.Wang, Q.G., C.S, P.Z., Z.C., Y.Z., A.Z., F.S., J.Z., Z.B., Z.Z., Han Wang, J.Y., J.S., G.L., Y.Wang, Y.-H.H., Y.-Y.H., J.H., S.Z., X.Z., Y.Wu, Z.-X.S., J.D., and H.D. contributed to experimental setup. All authors contributed to the discussions of the results. Competing interests All authors declare no competing interests. References [1] S. Aaronson and A. Ambainis (2014) The need for structure in quantum speedups. Theory of Computing 10 (6), p. 133–166. External Links: Document Cited by: §1. [2] A. A. Alemi, F. Chollet, N. Een, G. Irving, C. Szegedy, and J. Urban (2016) DeepMath—deep sequence models for premise selection. In Advances in Neural Information Processing Systems 29, p. 2235–2243. Cited by: §2. [3] 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) Quantum supremacy using a programmable superconducting processor. Nature 574 (7779), p. 505–510. External Links: Document Cited by: Abstract, Proving olympiad geometry theorems on a superconducting quantum processor. [4] A. Barenco, C. H. Bennett, R. Cleve, D. P. DiVincenzo, N. Margolus, P. Shor, T. Sleator, J. A. Smolin, and H. Weinfurter (1995) Elementary gates for quantum computation. Physical Review A 52 (5), p. 3457–3467. External Links: Document Cited by: Figure S7. [5] J. Biamonte, P. Wittek, N. Pancotti, P. Rebentrost, N. Wiebe, and S. Lloyd (2017) Quantum machine learning. Nature 549 (7671), p. 195–202. External Links: Document Cited by: Proving olympiad geometry theorems on a superconducting quantum processor. [6] 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), p. 58–65. External Links: Document Cited by: Proving olympiad geometry theorems on a superconducting quantum processor. [7] M. Cerezo, G. Verdon, H. Huang, L. Cincio, and P. J. Coles (2022) Challenges and opportunities in quantum machine learning. Nature Computational Science 2 (9), p. 567–576. External Links: Document Cited by: Proving olympiad geometry theorems on a superconducting quantum processor. [8] Z. Chen, J. Kelly, C. Quintana, R. Barends, B. Campbell, Y. Chen, B. Chiaro, A. Dunsworth, A. G. Fowler, E. Lucero, et al. (2016) Measuring and suppressing quantum state leakage in a superconducting qubit. Physical Review Letters 116 (2), p. 020501. External Links: Document Cited by: item -. [9] S. Chou, X. Gao, and J. Zhang (1996) Automated generation of readable proofs with geometric invariants: I. theorem proving with full-angles. Journal of Automated Reasoning 17 (3), p. 349–370. External Links: Document Cited by: §2.1, §2.1, §2.3, §2.3, §2, Proving olympiad geometry theorems on a superconducting quantum processor, Proving olympiad geometry theorems on a superconducting quantum processor. [10] S. Chou (1988) An introduction to Wu’s method for mechanical theorem proving in geometry. Journal of Automated Reasoning 4 (3), p. 237–267. External Links: Document Cited by: §1.1, §1, §1. [11] K. M. Collins, A. Q. Jiang, S. Frieder, L. Wong, M. Zilka, U. Bhatt, T. Lukasiewicz, Y. Wu, J. B. Tenenbaum, W. Hart, et al. (2024) Evaluating language models for mathematics through interactions. Proceedings of the National Academy of Sciences 121 (24), p. e2318124121. External Links: Document Cited by: §2. [12] D. Coppersmith (2002) An approximate Fourier transform useful in quantum factoring. Note: IBM Research Report RC 19642 External Links: quant-ph/0201067, Document, Link Cited by: §2.5. [13] S. Das Sarma, D. Deng, and L. Duan (2019) Machine learning meets quantum physics. Physics Today 72 (3), p. 48–54. External Links: Document Cited by: Proving olympiad geometry theorems on a superconducting quantum processor. [14] D. Deutsch and R. Jozsa (1992) Rapid solution of problems by quantum computation. Proceedings of the Royal Society of London. Series A: Mathematical and Physical Sciences 439 (1907), p. 553–558. External Links: Document Cited by: §2.5, §2.5. [15] V. Dunjko and H. J. Briegel (2018) Machine learning & artificial intelligence in the quantum domain: a review of recent progress. Reports on Progress in Physics 81 (7), p. 074001. External Links: Document Cited by: Proving olympiad geometry theorems on a superconducting quantum processor. [16] V. Dunjko, J. M. Taylor, and H. J. Briegel (2016) Quantum-enhanced machine learning. Physical Review Letters 117 (13), p. 130501. External Links: Document Cited by: Proving olympiad geometry theorems on a superconducting quantum processor. [17] 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) Quantum phases of matter on a 256-atom programmable quantum simulator. Nature 595 (7866), p. 227–232. External Links: Document Cited by: Proving olympiad geometry theorems on a superconducting quantum processor. [18] L. Egan, D. M. Debroy, C. Noel, A. Risinger, D. Zhu, D. Biswas, M. Newman, M. Li, K. R. Brown, M. Cetina, et al. (2021) Fault-tolerant control of an error-corrected qubit. Nature 598 (7880), p. 281–286. External Links: Document Cited by: Proving olympiad geometry theorems on a superconducting quantum processor. [19] M. Fitting (1996) First-order logic and automated theorem proving. 2 edition, Graduate Texts in Computer Science, Springer-Verlag, New York, NY. External Links: ISBN 978-0-387-94593-4, Document Cited by: Abstract. [20] X. Gao, Z. Zhang, and L. Duan (2018) A quantum machine learning algorithm based on generative models. Science Advances 4 (12), p. eaat9004. External Links: Document Cited by: Proving olympiad geometry theorems on a superconducting quantum processor. [21] Google Quantum AI and Collaborators (2025) Observation of constructive interference at the edge of quantum ergodicity. Nature 646 (8086), p. 825–830. External Links: Document Cited by: Abstract. [22] Google Quantum AI and Collaborators (2025) Quantum error correction below the surface code threshold. Nature 638 (8052), p. 920–926. External Links: Document Cited by: Proving olympiad geometry theorems on a superconducting quantum processor. [23] Google Quantum AI (2023) Suppressing quantum errors by scaling a surface code logical qubit. Nature 614 (7949), p. 676–681. External Links: Document Cited by: Proving olympiad geometry theorems on a superconducting quantum processor. [24] W. T. Gowers, B. Green, F. Manners, and T. Tao (2025) On a conjecture of Marton. Annals of Mathematics 201 (2), p. 515–549. External Links: Document Cited by: Abstract. [25] 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, New York, NY, p. 212–219. External Links: ISBN 978-0-89791-785-8, Document Cited by: §1. [26] 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), p. 633–638. External Links: Document Cited by: Abstract, Proving olympiad geometry theorems on a superconducting quantum processor. [27] 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), p. 259–263. External Links: Document Cited by: Proving olympiad geometry theorems on a superconducting quantum processor. [28] A. W. Harrow, A. Hassidim, and S. Lloyd (2009) Quantum algorithm for linear systems of equations. Physical Review Letters 103 (15), p. 150502. External Links: Document Cited by: Proving olympiad geometry theorems on a superconducting quantum processor. [29] O. Hasan and S. Tahar (2015) Formal verification methods. In Encyclopedia of Information Science and Technology, Third Edition, M. Khosrow-Pour (Ed.), p. 7162–7170. External Links: ISBN 978-1-4666-5888-2, Document Cited by: Abstract, Proving olympiad geometry theorems on a superconducting quantum processor. [30] V. Havlíček, A. D. Córcoles, K. Temme, A. W. Harrow, A. Kandala, J. M. Chow, and J. M. Gambetta (2019) Supervised learning with quantum-enhanced feature spaces. Nature 567 (7747), p. 209–212. External Links: Document Cited by: Proving olympiad geometry theorems on a superconducting quantum processor. [31] L. Hu, S. Wu, W. Cai, Y. Ma, X. Mu, Y. Xu, H. Wang, Y. Song, D. Deng, C. Zou, et al. (2019) Quantum generative adversarial learning in a superconducting quantum circuit. Science Advances 5 (1), p. eaav2761. External Links: Document Cited by: Proving olympiad geometry theorems on a superconducting quantum processor. [32] 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), p. 1182–1186. External Links: Document Cited by: Proving olympiad geometry theorems on a superconducting quantum processor. [33] 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. (2026) Olympiad-level formal mathematical reasoning with reinforcement learning. Nature 651 (8106), p. 607–613. External Links: Document Cited by: Abstract, §2, Proving olympiad geometry theorems on a superconducting quantum processor. [34] S. Jerbi, L. J. Fiderer, H. Poulsen Nautrup, J. M. Kübler, H. J. Briegel, and V. Dunjko (2023) Quantum machine learning beyond kernel methods. Nature Communications 14 (1), p. 517. External Links: Document Cited by: Proving olympiad geometry theorems on a superconducting quantum processor. [35] 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), p. 626–632. External Links: Document Cited by: item -, Proving olympiad geometry theorems on a superconducting quantum processor. [36] 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, New York, NY, p. 355–364. External Links: Document Cited by: §1. [37] C. Kaliszyk, J. Urban, H. Michalewski, and M. Olšák (2018) Reinforcement learning of theorem proving. In Advances in Neural Information Processing Systems 31, p. 8822–8833. Cited by: §2. [38] Y. Kim, A. Eddins, S. Anand, K. X. Wei, E. van den Berg, S. Rosenblatt, H. Nayfeh, Y. Wu, M. Zaletel, K. Temme, et al. (2023) Evidence for the utility of quantum computing before fault tolerance. Nature 618 (7965), p. 500–505. External Links: Document Cited by: Proving olympiad geometry theorems on a superconducting quantum processor. [39] A. D. King, A. Nocera, M. M. Rams, J. Dziarmaga, R. Wiersema, W. Bernoudy, J. Raymond, N. Kaushal, N. Heinsdorf, R. Harris, et al. (2025) Beyond-classical computation in quantum simulation. Science 388 (6743), p. 199–204. External Links: Document Cited by: Abstract. [40] S. Krinner, N. Lacroix, A. Remm, A. Di Paolo, E. Genois, C. Leroux, C. Hellings, S. Lazar, F. Swiadek, J. Herrmann, et al. (2022) Realizing repeated quantum error correction in a distance-three surface code. Nature 605 (7911), p. 669–674. External Links: Document Cited by: Proving olympiad geometry theorems on a superconducting quantum processor. [41] N. Lacroix, A. Bourassa, F. J. H. 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 colour code on a superconducting quantum processor. Nature 645 (8081), p. 614–619. External Links: Document Cited by: Proving olympiad geometry theorems on a superconducting quantum processor. [42] G. Li, Y. Ding, and Y. Xie (2019) Tackling the qubit mapping problem for NISQ-era quantum devices. In Proceedings of the Twenty-Fourth International Conference on Architectural Support for Programming Languages and Operating Systems, p. 1001–1014. External Links: Document Cited by: §3.2.2. [43] W. Li, Y. Ma, and D. Deng (2025) Pitfalls and prospects of quantum machine learning. Nature Computational Science 5 (12), p. 1095–1097. External Links: Document Cited by: Proving olympiad geometry theorems on a superconducting quantum processor. [44] Y. Liu, S. Arunachalam, and K. Temme (2021) A rigorous and robust quantum speed-up in supervised machine learning. Nature Physics 17 (9), p. 1013–1017. External Links: Document Cited by: Proving olympiad geometry theorems on a superconducting quantum processor. [45] S. Lloyd, M. Mohseni, and P. Rebentrost (2014) Quantum principal component analysis. Nature Physics 10 (9), p. 631–633. External Links: Document Cited by: Proving olympiad geometry theorems on a superconducting quantum processor. [46] D. W. Loveland (1978) Automated theorem proving: a logical basis. 1 edition, Fundamental Studies in Computer Science, Vol. 6, North-Holland Publishing Company, Amsterdam. External Links: ISBN 978-0-7204-0499-9 Cited by: Abstract. [47] L. S. Madsen, F. Laudenbach, M. F. Askarani, F. Rortais, T. Vincent, J. F. F. Bulmer, F. M. Miatto, L. Neuhaus, L. G. Helt, M. J. Collins, et al. (2022) Quantum computational advantage with a programmable photonic processor. Nature 606 (7912), p. 75–81. External Links: Document Cited by: Abstract, Proving olympiad geometry theorems on a superconducting quantum processor. [48] D. Maslov (2016) Advantages of using relative-phase Toffoli gates with an application to multiple control Toffoli optimization. Physical Review A 93 (2), p. 022311. External Links: Document Cited by: §3.2.1. [49] K. Mitarai, M. Negoro, M. Kitagawa, and K. Fujii (2018) Quantum circuit learning. Physical Review A 98, p. 032309. External Links: Document Cited by: Proving olympiad geometry theorems on a superconducting quantum processor. [50] 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) A race-track trapped-ion quantum processor. Physical Review X 13 (4), p. 041052. External Links: Document Cited by: Proving olympiad geometry theorems on a superconducting quantum processor. [51] A. J. Nevins (1975) Plane geometry theorem proving using forward chaining. Artificial Intelligence 6 (1), p. 1–23. External Links: Document Cited by: §2.3. [52] Z. Ni, S. Li, X. Deng, Y. Cai, L. Zhang, W. Wang, Z. Yang, H. Yu, F. Yan, S. Liu, et al. (2023) Beating the break-even point with a discrete-variable-encoded logical qubit. Nature 616 (7955), p. 56–60. External Links: Document Cited by: Proving olympiad geometry theorems on a superconducting quantum processor. [53] M. A. Nielsen and I. L. Chuang (2010) Quantum computation and quantum information. 10th Anniversary Edition edition, Cambridge University Press, Cambridge. External Links: ISBN 978-1-107-00217-3, Document Cited by: Abstract, Proving olympiad geometry theorems on a superconducting quantum processor. [54] W. Ren, W. Li, S. Xu, K. Wang, W. Jiang, F. Jin, X. Zhu, J. Chen, Z. Song, P. Zhang, et al. (2022) Experimental quantum adversarial learning with programmable superconducting qubits. Nature Computational Science 2 (11), p. 711–717. External Links: Document Cited by: Proving olympiad geometry theorems on a superconducting quantum processor. [55] Z. Z. Ren, Z. Shao, J. Song, H. Xin, H. Wang, W. Zhao, L. Zhang, Z. Fu, Q. Zhu, D. Yang, et al. (2025) DeepSeek-Prover-V2: advancing formal mathematical reasoning via reinforcement learning for subgoal decomposition. External Links: 2504.21801, Document, Link Cited by: §2. [56] L. Ruiz-Pérez and J. C. García-Escartín (2017) Quantum arithmetic with the quantum Fourier transform. Quantum Information Processing 16 (6), p. 152. External Links: Document Cited by: §1.3. [57] P. W. Shor (1994) Algorithms for quantum computation: discrete logarithms and factoring. In Proceedings of the 35th Annual Symposium on Foundations of Computer Science, p. 124–134. External Links: Document Cited by: §2.5. [58] D. R. Simon (1997) On the power of quantum computation. SIAM Journal on Computing 26 (5), p. 1474–1483. External Links: Document Cited by: §2.5. [59] 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) Real-time quantum error correction beyond break-even. Nature 616 (7955), p. 50–55. External Links: Document Cited by: Proving olympiad geometry theorems on a superconducting quantum processor. [60] D. Stahlke (2014) Quantum interference as a resource for quantum speedup. Physical Review A 90 (2), p. 022302. External Links: Document Cited by: §2.5. [61] Z. Sun, Q. Ye, and D. Deng (2026) Quantum automated theorem proving. External Links: 2601.07953, Document, Link Cited by: Abstract, §1.3, §1.3, §1, §1, §2.3, §2.3, §2.3, §2.3, §2.4, §2.4, §2, Proving olympiad geometry theorems on a superconducting quantum processor, Proving olympiad geometry theorems on a superconducting quantum processor, Proving olympiad geometry theorems on a superconducting quantum processor, Proving olympiad geometry theorems on a superconducting quantum processor, Proving olympiad geometry theorems on a superconducting quantum processor, Proving olympiad geometry theorems on a superconducting quantum processor. [62] T. H. Trinh, Y. Wu, Q. V. Le, H. He, and T. Luong (2024) Solving olympiad geometry without human demonstrations. Nature 625 (7995), p. 476–482. External Links: Document Cited by: Abstract, Proving olympiad geometry theorems on a superconducting quantum processor. [63] K. Wang, Z. Lu, C. Zhang, G. Liu, J. Chen, Y. Wang, Y. Wu, S. Xu, X. Zhu, F. Jin, et al. (2026) Demonstration of low-overhead quantum error correction codes. Nature Physics 22 (2), p. 308–314. External Links: Document Cited by: Proving olympiad geometry theorems on a superconducting quantum processor. [64] W. Wu (1978) On the decision problem and the mechanization of theorem-proving in elementary geometry. Scientia Sinica 21 (2), p. 159–172. Cited by: §1.1, §1, §1, Proving olympiad geometry theorems on a superconducting quantum processor. [65] Y. Wu, W. Bao, S. Cao, F. Chen, M. Chen, X. Chen, T. Chung, H. Deng, Y. Du, D. Fan, et al. (2021) Strong quantum computational advantage using a superconducting quantum processor. Physical Review Letters 127 (18), p. 180501. External Links: Document Cited by: Abstract, Proving olympiad geometry theorems on a superconducting quantum processor. [66] S. Xu, Z. Sun, K. Wang, H. Li, Z. Zhu, H. Dong, J. Deng, X. Zhang, J. Chen, Y. Wu, et al. (2024) Non-Abelian braiding of Fibonacci anyons with a superconducting processor. Nature Physics 20 (9), p. 1469–1475. External Links: Document Cited by: Proving olympiad geometry theorems on a superconducting quantum processor. [67] T. J. Yoder, G. H. Low, and I. L. Chuang (2014) Fixed-point quantum search with an optimal number of queries. Physical Review Letters 113 (21), p. 210501. External Links: Document Cited by: §1. [68] C. Zhang, J. Song, S. Li, Y. Liang, Y. Ma, W. Wang, Y. Zhu, and S. Zhu (2026) Proposing and solving olympiad geometry with guided tree search. Nature Machine Intelligence 8 (1), p. 84–95. External Links: Document Cited by: §2, Proving olympiad geometry theorems on a superconducting quantum processor. [69] H. Zhong, H. Wang, Y. Deng, M. Chen, L. Peng, Y. Luo, J. Qin, D. Wu, X. Ding, Y. Hu, et al. (2020) Quantum computational advantage using photons. Science 370 (6523), p. 1460–1463. External Links: Document Cited by: Abstract, Proving olympiad geometry theorems on a superconducting quantum processor. Supplementary Information: Proving olympiad geometry theorems on a superconducting quantum processor Contents References Supplementary Information: Proving olympiad geometry theorems on a superconducting quantum processor 1 Quantum algebraic theorem proving 1.1 Classical Wu’s method 1.2 The square example 1.3 Quantum implementation of Wu’s method 2 Quantum proof search 2.1 Preliminaries for the full-angle method 2.2 IMO example 2.3 State representation of formulas 2.4 Reasoning engine 2.5 Strategy engine and value function 2.6 Real circuit 2.6.1 Circuit of reasoning engine 2.6.2 Circuit for the value function 2.6.3 Circuit of strategy engine 3 Experiment 3.1 Device information 3.2 Circuit and layout 3.2.1 Multi-qubit gate optimization 3.2.2 Quantum circuit compilation 3.2.3 Experimental circuits 3.3 Additional results References 1 Quantum algebraic theorem proving We begin with Wu’s method as an algebraic realization of quantum automated theorem proving (QATP) [61]. Fig. S1 summarizes the underlying reasoning cycle. Given a set of hypotheses and a target statement, the hypotheses are encoded in a quantum knowledge base. Quantum reasoning then derives new formulas or transforms the symbolic expressions used in the proof. The result is checked against the criterion for establishing the target, and intermediate results are used to update the knowledge base when further reasoning is required. The mathematical representation, reasoning operations, and success criterion are specified by the chosen proving method. Figure S1: Schematic reasoning cycle in QATP. The hypotheses are encoded in a quantum knowledge base and processed by quantum reasoning. The “Goal found?” test checks whether the resulting derivation establishes the target statement. If so, the procedure terminates successfully. Otherwise, intermediate results are used to update the knowledge base for the next round. The cycle continues until the target is established or a prescribed stopping condition is met. Fig. S2 shows the corresponding classical–quantum workflow. A natural-language problem is first formalized: the hypotheses define a classical knowledge base, and the target is expressed in the same formal language. The expressions required for reasoning are encoded in quantum states or circuits, on which quantum operations generate the next symbolic result. Examples include quantum resolution for propositional or first-order formulas and quantum pseudo-division for polynomials representing geometric relations. Classical post-processing then updates the representation used in subsequent steps. The selected proof strategy and its termination rule determine when this iteration yields a proof. Depending on the procedure, the computation may also terminate by refuting the target, when no further progress can be made, or upon reaching a resource limit. Figure S2: An iterative QATP workflow with classical knowledge-base updates. A natural-language problem is formalized into a classical knowledge base, which is encoded as a quantum knowledge base. Quantum reasoning produces quantum representations of new knowledge. In this scheme, intermediate results are post-processed classically to update the knowledge base, which is then re-encoded for subsequent reasoning. The selected proof strategy and its termination rule determine when the target has been established and a proof is obtained. Proof by contradiction and polynomial identity testing are shown as examples. In Wu’s method, the symbolic expressions in this workflow are polynomials encoding the hypotheses and the target conclusion [64, 10]. The hypotheses supply polynomial constraints, and the target is represented by a conclusion polynomial to be reduced. The hypothesis system is first transformed into triangular form, after which successive pseudo-division reduces the conclusion polynomial. The pseudo-remainder produced at each step supplies the polynomial for the next reduction. In the implementation considered here, classical reconstruction and re-encoding connect successive reductions, following the update loop in Fig. S2. With the variable ordering and reduction rules fixed, these reductions follow a prescribed algebraic procedure. The goal test in Fig. S1 then checks whether the final pseudo-remainder vanishes identically, which establishes the conclusion under the relevant non-degeneracy conditions. This final zero test can be formulated as polynomial identity testing: one searches a suitable hitting set for an evaluation point at which the pseudo-remainder is nonzero [61]. This connects the algebraic procedure to the search-based validation tasks studied within QATP. A related task arises in the quantum resolution procedure discussed above, where valid resolvents must be identified among candidate inference results [61]. For these search-based validation tasks, Grover-type algorithms [25, 67] can provide a quadratic reduction in query complexity. This comparison concerns the respective search subroutines rather than the overall cost of theorem proving. Superpolynomial advantages in generic settings are constrained by the relevant no-go results and complexity-theoretic assumptions [36, 1]. For restricted problem classes with additional structure, such as particular families of logical formulas or geometric polynomials with specific symmetries, quantum algorithms may nevertheless admit superpolynomial speedups beyond the generic quadratic improvement. Geometry provides a useful setting for demonstrating these algebraic operations. Statements such as the perpendicularity of the diagonals of a square are readily understood, and coordinate representations give a direct formalization in terms of indexed variables. These features make small geometric examples suitable for noisy intermediate-scale quantum (NISQ) devices. In this section, we first review classical Wu’s method [64, 10], then present the square example, and finally describe its quantum implementation and the simplifications adopted in this work. 1.1 Classical Wu’s method Wu’s method [64, 10] is a deterministic algebraic framework for establishing consequences of polynomial equation systems. In geometry theorem proving, each point is assigned a pair of coordinate variables, and geometric relations, such as collinearity, parallelism, perpendicularity, and equality of angles, are translated into multivariate polynomial equations with integer coefficients. This converts the geometric statement into an algebraic problem. Let the hypotheses be represented by the finite polynomial set ℋ=H1,H2,…,HmH=\H_1,H_2,…,H_m\ and the conclusion by a polynomial G. The task is to determine whether G=0G=0 follows from the constraints in ℋH under generic geometric configurations. Elimination proceeds with a fixed variable ordering, typically chosen according to the order in which points are introduced in the geometric construction. The ordering reflects the constructive structure of the problem and determines the leading variable and leading coefficient of each polynomial. Successive pseudo-division steps reduce the polynomial system according to this ordering and yield a triangular set =f1,f2,…,fkT=\f_1,f_2,…,f_k\ whose leading variables are strictly increasing. Together with the prescribed reduction rules, the variable ordering specifies how the triangularization proceeds. Consider two polynomials P and Q over a coefficient ring, with the variable ordering fixed. Let y be the leading variable of Q, let DQ=degy(Q)D_Q= _y(Q), and denote the leading coefficient of Q with respect to y by L(Q)L(Q). For degy(P)=DP≥DQ _y(P)=D_P≥ D_Q, pseudo-division removes the highest power of y in P without dividing by L(Q)L(Q). Starting from P(0)=P^(0)=P and A(0)=0A^(0)=0, define di=degy(P(i−1))−DQd_i= _y(P^(i-1))-D_Q and ci=L(P(i−1))c_i=L (P^(i-1) ) at each iteration i=1,2,…,ti=1,2,…,t, where t=DP−DQ+1t=D_P-D_Q+1 and L(⋅)L(·) denotes the leading coefficient with respect to y. The reduction updates the current polynomial according to P(i)=L(Q)P(i−1)−ciydiQ, P^(i)=L(Q)P^(i-1)-c_iy^d_iQ, (S1) and accumulates the quotient through A(i)=L(Q)A(i−1)+ciydi. A^(i)=L(Q)A^(i-1)+c_iy^d_i. (S2) Each reduction cancels the current highest-degree term of P(i−1)P^(i-1) in y. The result either vanishes or has a strictly lower degree in y. After t iterations, set R=P(t)R=P^(t) and A=A(t)A=A^(t). The final pseudo-remainder satisfies R=0R=0 or degy(R)<degy(Q) _y(R)< _y(Q), and the pseudo-division identity reads L(Q)tP=AQ+R. L(Q)^tP=AQ+R. (S3) Multiplication by L(Q)L(Q) at each reduction step avoids rational coefficients and keeps all intermediate polynomials in the original coefficient ring. To make the cancellation explicit, separate the elimination variable y from the remaining variables and write P=∑,d,DPp(,d)∏k=1Kxkikyd, P=Σ _ i,d I,D_Pp( i,d)Π _k=1^Kx_k^i_ky^d, Q=∑,d,DQq(,d)∏k=1Kxkjkyd. Q=Σ _ j,d J,D_Qq( j,d)Π _k=1^Kx_k^j_ky^d. (S4) Here p(⋅)p(·) and q(⋅)q(·) are the coefficients of P and Q, respectively. The multi-indices =(i1,…,iK) i=(i_1,…,i_K) and =(j1,…,jK) j=(j_1,…,j_K) specify the degrees of the variables xkx_k, whose maximal degrees in P and Q are denoted by IkI_k and JkJ_k. The first reduction step gives P(1)=L(Q)P−L(P)yDP−DQQ=∑,,d,,DPp(,d)q(,DQ)∏k=1Kxkik+jkyd−∑,,d,,DQp(,DP)q(,d)∏k=1Kxkik+jkyd+DP−DQ. P^(1)=L(Q)P-L(P)y^D_P-D_QQ=Σ _ i, j,d I, J,D_Pp( i,d)q( j,D_Q)Π _k=1^Kx_k^i_k+j_ky^d-Σ _ i, j,d I, J,D_Qp( i,D_P)q( j,d)Π _k=1^Kx_k^i_k+j_ky^d+D_P-D_Q. (S5) The two contributions to the coefficient of yDPy^D_P in P(1)P^(1) cancel: ∑,,p(,DP)q(,DQ)∏k=1Kxkik+jk−∑,,p(,DP)q(,DQ)∏k=1Kxkik+jk=0, Σ _ i, j I, Jp( i,D_P)q( j,D_Q)Π _k=1^Kx_k^i_k+j_k-Σ _ i, j I, Jp( i,D_P)q( j,D_Q)Π _k=1^Kx_k^i_k+j_k=0, (S6) which cancels the highest-degree term of P(0)P^(0) in y. Thus, P(1)P^(1) either vanishes or has a lower degree in y than P(0)P^(0), ensuring progress of the reduction. Wu’s method applies pseudo-division repeatedly according to the chosen elimination ordering. The resulting pseudo-remainders reduce the rank of the system and are retained for use in subsequent eliminations. When no further elimination is possible, the resulting system forms the triangular set T. The conclusion polynomial G is then pseudo-divided successively by the polynomials in T according to the same ordering. If the final pseudo-remainder vanishes identically, G belongs to the ideal generated by ℋH up to factors arising from leading coefficients, establishing the geometric conclusion. The powers of leading coefficients introduced by pseudo-division generally impose non-degeneracy conditions requiring those coefficients to be nonzero. These conditions exclude degenerate configurations and must be handled explicitly in classical Wu’s method. Here they are assumed to hold implicitly and are not treated further, since our focus is the algebraic structure needed for the quantum implementation. 1.2 The square example We now illustrate Wu’s method by proving that the diagonals of a square are perpendicular. The example shows how successive pseudo-division reduces a target polynomial and how a vanishing final pseudo-remainder certifies the conclusion. We assume a non-degenerate square ABCDABCD and choose Cartesian coordinates with A at the origin and ABAB along the x-axis. The vertices are parameterized as A=(0,0)A=(0,0), B=(x1,0)B=(x_1,0), C=(x3,x2)C=(x_3,x_2), and D=(x5,x4)D=(x_5,x_4), where x1,…,x5x_1,…,x_5 are algebraic variables, as illustrated in Fig. S3. Figure S3: Coordinate representation of the square ABCDABCD used in Wu’s method. Point A is placed at the origin and side ABAB is aligned with the x-axis. The remaining vertices are parameterized by the algebraic variables x1,…,x5x_1,…,x_5. This coordinate choice is made without loss of generality. The defining properties of the square give four polynomial constraints. First, AB⟂ADAB AD gives x1x5=0x_1x_5=0. Excluding A=BA=B requires x1≠0x_1≠ 0, so H1:x5=0. H_1:x_5=0. (S7) Second, AB|CDAB CD gives x1(x4−x2)=0x_1(x_4-x_2)=0. Using x1≠0x_1≠ 0 again yields H2:x4−x2=0. H_2:x_4-x_2=0. (S8) Third, AD|BCAD BC gives x5x2−x4(x3−x1)=0x_5x_2-x_4(x_3-x_1)=0. Substituting H1H_1 reduces this condition to x4(x3−x1)=0x_4(x_3-x_1)=0, and excluding the degenerate case x4=0x_4=0 gives H3:x3−x1=0. H_3:x_3-x_1=0. (S9) Finally, |AB|=|BC| AB = BC implies x22+(x3−x1)2−x12=0x_2^2+(x_3-x_1)^2-x_1^2=0, which reduces under H3H_3 to H4:x22−x12=0. H_4:x_2^2-x_1^2=0. (S10) The hypothesis set is therefore ℋ=H1,H2,H3,H4. =\H_1,H_2,H_3,H_4\. (S11) The desired perpendicularity of ACAC and BDBD is encoded by G:x3(x5−x1)+x2x4=0. G:x_3(x_5-x_1)+x_2x_4=0. (S12) To prove G=0G=0 from ℋ=H1,H2,H3,H4H=\H_1,H_2,H_3,H_4\, we eliminate the variables in the order (x5,x4,x3,x2)(x_5,x_4,x_3,x_2). Starting from R0:=GR_0:=G, the successive pseudo-remainders are R1:=Prem(R0,H1,x5), R_1:=Prem(R_0,H_1,x_5), R2:=Prem(R1,H2,x4), R_2:=Prem(R_1,H_2,x_4), R3:=Prem(R2,H3,x3), R_3:=Prem(R_2,H_3,x_3), R4:=Prem(R3,H4,x2). R_4:=Prem(R_3,H_4,x_2). (S13) In the first step, we eliminate x5x_5 in G using H1:x5=0H_1:x_5=0 by subtracting x3H1x_3H_1: R1=G−x3H1=(x3(x5−x1)+x2x4)−x3x5=x2x4−x3x1. R_1=G-x_3H_1=(x_3(x_5-x_1)+x_2x_4)-x_3x_5=x_2x_4-x_3x_1. (S14) Next, subtracting x2H2x_2H_2 eliminates x4x_4 using H2:x4−x2=0H_2:x_4-x_2=0: R2=R1−x2H2=(x2x4−x3x1)−x2(x4−x2)=x22−x3x1. R_2=R_1-x_2H_2=(x_2x_4-x_3x_1)-x_2(x_4-x_2)=x_2^2-x_3x_1. (S15) The third step eliminates x3x_3 using H3:x3−x1=0H_3:x_3-x_1=0 by subtracting (−x1)H3(-x_1)H_3: R3=R2−(−x1)H3=(x22−x3x1)+x1(x3−x1)=x22−x12. R_3=R_2-(-x_1)H_3=(x_2^2-x_3x_1)+x_1(x_3-x_1)=x_2^2-x_1^2. (S16) The resulting polynomial R3R_3 coincides with H4:x22−x12=0H_4:x_2^2-x_1^2=0, so the final pseudo-remainder vanishes: R4=R3−H4=(x22−x12)−(x22−x12)=0. R_4=R_3-H_4=(x_2^2-x_1^2)-(x_2^2-x_1^2)=0. (S17) Since the final pseudo-remainder is identically zero, Wu’s method certifies that the conclusion polynomial G follows from ℋ=H1,H2,H3,H4H=\H_1,H_2,H_3,H_4\ under the non-degeneracy assumptions used to obtain the hypotheses. The diagonals of the square are therefore perpendicular. 1.3 Quantum implementation of Wu’s method Our quantum implementation represents each polynomial by a circuit encoding its point-value pairs. This avoids the need to merge like terms during polynomial multiplication, a central difficulty of coefficient-based quantum representations [61]. Polynomial values on a fixed evaluation set are computed classically and embedded into quantum circuits. The quantum computation acts on these pointwise values, whereas interpolation and coefficient reconstruction are performed classically. For a polynomial F()F( x) in variables =(x1,x2,…) x=(x_1,x_2,…), we choose a finite evaluation set m x_m and calculate F(m)F( x_m) at each point. A sufficient number of evaluation points uniquely determines F, allowing polynomial operations to be performed on pointwise data rather than monomial coefficients. The point-value pairs m,F(m) x_m,F( x_m) are encoded by a circuit implementing UF|⟩|⟩=|⟩|F()⟩, U_F | x_m | 0 = | x_m |F( x_m) , (S18) where |m⟩ | x_m and |F(m)⟩ |F( x_m) denote the binary encodings of the evaluation point and its polynomial value. In this representation, polynomial operations become pointwise reversible integer arithmetic and require neither term collection nor coefficient comparison. Circuits for polynomials defined on the same evaluation set can be composed, making the representation suitable for iterative pseudo-division. To use this representation for pseudo-division, we must additionally express the polynomial as a univariate polynomial in the variable to be eliminated, say y. The coefficients in this representation are themselves polynomials in the remaining variables. Although this transformation can in principle be performed by quantum interpolation [61], in the present implementation these coefficient polynomials are obtained classically. They are then encoded in a quantum circuit whose output is controlled by the exponent d of y. For a polynomial P, the resulting coefficient-evaluation circuit implements UP,y|d⟩|⟩|⟩=|d⟩|⟩|∑p(,d)∏k=1Kxkik⟩. U_P,y |d | x_m | 0 = |d | x_m |Σ _ i Ip( i,d)Π _k=1^Kx_k^i_k . (S19) Here ∑p(,d)∏k=1KxkikΣ _ i Ip( i,d)Π _k=1^Kx_k^i_k is the coefficient of ydy^d in P, regarded as a polynomial in the remaining variables x and evaluated at the point encoded in |m⟩ | x_m . For the corresponding representation of Q, we abbreviate the output state |∑q(,d)∏k=1Kxkjk⟩ |Σ _ j Jq( j,d)Π _k=1^Kx_k^j_k as |q(d)⟩ |q(d) when no ambiguity arises. These point-value circuits, defined with respect to the chosen elimination variable, are combined with standard arithmetic circuits [56] to construct the pseudo-remainder circuit illustrated in Fig. 2 of the main text. In the square example, each variable elimination requires only one pseudo-division step. As shown in the preceding subsection, the first three steps remove the dependence on x5x_5, x4x_4, and x3x_3, respectively, while the final step yields the zero polynomial. Table S1 lists the remaining variables z, the elimination variable y, and the dividend and divisor P and Q at each step. These assignments directly connect the algebraic proof to its quantum circuits. Variable or PolynomialStep 1 2 3 4 \ z\ (x1,x2,x3,x4)\ (x_1,x_2,x_3,x_4)\ (x1,x2,x3)\ (x_1,x_2,x_3)\ (x1,x2)\ (x_1,x_2)\ (x1)\ (x_1)\ y\ y\ x5\ x_5\ x4\ x_4\ x3\ x_3\ x2\ x_2\ P\ P\ G\ G\ x2x4−x3x1\ x_2x_4-x_3x_1\ x22−x3x1\ x_2^2-x_3x_1\ x22−x12\ x_2^2-x_1^2\ Q\ Q\ H1\ H_1\ H2\ H_2\ H3\ H_3\ H4\ H_4\ Table S1: Variables and polynomials used in the proof. We implement this four-step elimination on the superconducting quantum processor using point-value representations throughout. The evaluation set for each variable is chosen according to its maximal degree at the corresponding step. In steps 2–4, the highest degree of any individual variable is two. Where three evaluation values are required, we use 00, 11, and −1-1, as listed in Table S2. These small evaluation sets provide sufficient data to determine the relevant polynomials while limiting the encoding overhead. Together with the polynomial assignments in Table S1, they specify the point-value encoding at each elimination step. VariableStep 1 2 3 4 x1\ x_1\ 0,1\ \0,1\\ 0,1\ \0,1\\ 0,1,−1\ \0,1,-1\\ 0,1,−1\ \0,1,-1\\ x2\ x_2\ 0,1\ \0,1\\ 0,1,−1\ \0,1,-1\\ 0,1,−1\ \0,1,-1\\ −\ -\ x3\ x_3\ 0,1\ \0,1\\ 0,1\ \0,1\\ −\ -\ −\ -\ x4\ x_4\ 0,1\ \0,1\\ −\ -\ −\ -\ −\ -\ x5\ x_5\ −\ -\ −\ -\ −\ -\ −\ -\ Table S2: The values of each variable in different reasoning steps. In this algebraic realization, the variable ordering and reduction rules specify the successive reasoning operations. The following section develops a more general proof-search framework in which the selection of inference rules and supporting relations is itself part of the computation, while the corresponding symbolic transformations are implemented by quantum reasoning circuits. 2 Quantum proof search The preceding section considered a concrete algebraic realization of QATP, in which the sequence of reasoning operations is specified by the underlying algebraic procedure. We now turn to a more general setting: proof search, where the choice of which inference to perform is itself part of the computational task. Even when individual reasoning operations can be implemented efficiently, constructing a complete proof may still require exploring many possible intermediate statements and reasoning paths [61]. For example, quantum resolution may involve many rounds of reasoning and repeated searches for valid resolvents, while algebraic proving methods may generate increasingly complicated intermediate expressions. Moreover, a proof obtained through a long sequence of low-level symbolic operations may be difficult to interpret directly. We now turn to quantum proof search. In the full-angle method considered here, the proof is constructed through backward chaining: starting from the target statement, the prover searches for intermediate formulas and supporting relations that reduce the current proof state toward the hypotheses. At each step, one must determine which inference rule or transformation to apply and, when necessary, which supporting relations from the knowledge base should be used. The resulting state then becomes the input to subsequent reasoning rounds. Fig. S4 illustrates this general search loop. Figure S4: Schematic quantum proof-search loop. Starting from the goal, a proof state is constructed and processed by quantum proof search. If a proof or disproof is found, the procedure terminates. Otherwise, the proof state is updated and the search continues until a proof or disproof is obtained or a prescribed stopping condition is met. The selection of reasoning rounds is a central problem in automated theorem proving. Classical proof-search systems commonly use handcrafted heuristics or machine-learning-based strategies to guide this selection [2]. More recently, large language models have also been explored for generating proofs incrementally or producing complete proofs directly [11, 55, 33, 68]. Such guidance can reduce unproductive exploration and produce shorter or more interpretable proofs, although the resulting search procedure need not preserve the completeness of an exhaustive proving method [37]. Motivated by this perspective, we consider the general quantum proof-search architecture illustrated in Fig. S5. At reasoning round t, the current proof state |St⟩|S_t and the quantum knowledge base |KB⟩|KB provide the information used for action selection. A strategy engine produces an action state that specifies the inference operation and the supporting relations to be used. The reasoning engine then implements the corresponding formal symbolic transformation and produces the next proof state |St+1⟩|S_t+1 . An evaluation circuit assesses the resulting reasoning state and provides signals summarized by a value function. These signals can in turn be used to optimize the strategy engine. Figure S5: General quantum architecture for proof search. At reasoning round t, the current proof state |St⟩|S_t together with the quantum knowledge base |KB⟩|KB is supplied to the strategy engine, which generates an action state specifying the reasoning operation and supporting relations to be used. The reasoning engine implements the corresponding formal symbolic transformation and produces the next reasoning state |St+1⟩|S_t+1 . The resulting state and intermediate information are processed by an evaluation circuit, which provides signals summarized by the value function. In the variational implementation considered here, these signals are used to update the parameters of the strategy circuit. The ellipses indicate possible auxiliary qubits used by the strategy and evaluation circuits. This architecture separates two conceptually different aspects of proof search. The reasoning engine implements formally specified symbolic transformations, whereas the strategy engine determines which of these transformations should be attempted for the current proof state. The evaluation circuit provides information for improving this selection. The resulting proof can therefore be checked according to the formal inference rules independently of how the reasoning actions were chosen. A quantum implementation also allows symbolic information to remain in superposition during reasoning. In a fully coherent realization, the selected actions, supporting relations, and intermediate formulas need not be read out after every inference step. Instead, their quantum representations can be retained and processed by subsequent circuits, allowing different formulas and reasoning paths to coexist within the same quantum state. This coherent processing provides a basis for potential quantum advantages in proof search. In the present experimental implementation, however, the proof proceeds round-by-round: after each round, the output state is measured and the selected result is used to prepare the input state for the next round, as described in the main text. As a concrete realization of this architecture, we use the full-angle method [9] for automated geometry theorem proving. Full-angles provide a fixed symbolic representation of geometric relations, together with a finite set of inference rules and explicit control strategies for proof construction. These properties make the method suitable for demonstrating the main components of quantum proof search on current quantum hardware. We first introduce the full-angle method and the geometry problem used in the experiment. We then describe the quantum representation of formulas, the reasoning engine, and the strategy and evaluation components. Finally, we present the specific quantum circuits used in the experimental implementation. 2.1 Preliminaries for the full-angle method The full-angle method [9] is a symbolic approach to automated geometry theorem proving in which geometric relations are represented and manipulated through full-angles. Full-angles are treated as algebraic objects equipped with equality, addition, and sign operations, and geometric proofs are constructed by applying a finite set of inference rules to these objects. The method combines two complementary procedures. First, a geometry information base (GIB) is constructed from the hypotheses by deriving elementary geometric relations that can be used later in the proof. The target statement is then expressed in terms of full-angles and reduced by applying inference rules together with the relations stored in the GIB. A canonical representation and a ranking-based control strategy restrict the applicable transformations and guide the reduction toward simpler full-angle expressions. In the terminology of the classical full-angle method, these two procedures correspond to a forward construction of the GIB followed by a backward chaining proof process. We adopt the following conventions. Points are denoted by uppercase letters, and lines are denoted either by lowercase letters or by pairs of distinct points. The full-angle ∠[u,v] [u,v] is defined as the angle between the undirected lines u and v. Two full-angles ∠[l,m] [l,m] and ∠[u,v] [u,v] are equal if there exists a rotation K such that K(l)|uK(l) u and K(m)|vK(m) v. The addition of two full-angles is defined as ∠[u,v]+∠[l,m]=∠[u,K(m)] [u,v]+ [l,m]= [u,K(m)], where K is any rotation satisfying K(l)|vK(l) v. The full-angles defined as ordered pairs of lines satisfy the following rules [9]: R1 For all parallel lines AB|PQAB PQ, ∠[0]=∠[AB,PQ] [0]= [AB,PQ] is a constant. R2 For all perpendicular lines AB⟂PQAB PQ, ∠[1]=∠[AB,PQ] [1]= [AB,PQ] is a constant. R3 There is an operation “addition” between two full-angles which is commutative and associative. R4 ∠[1]+∠[1]=∠[0] [1]+ [1]= [0]. R5 ∠[u,v]+∠[0]=∠[u,v] [u,v]+ [0]= [u,v]. R6 If X is on line PQPQ, then ∠[AB,PX]=∠[AB,PQ] [AB,PX]= [AB,PQ]. R7 If PXPX is parallel to UVUV, then ∠[AB,PX]=∠[AB,UV] [AB,PX]= [AB,UV]. R8 If PXPX is perpendicular to UVUV, then ∠[AB,PX]=∠[1]+∠[AB,UV] [AB,PX]= [1]+ [AB,UV]. R9 If XA=XBXA=XB then ∠[AX,AB]=∠[AB,XB] [AX,AB]= [AB,XB]. R10 (The Inscribed Angle Theorem) If A,B,CA,B,C, and D are cyclic then ∠[AD,CD]=∠[AB,CB] [AD,CD]= [AB,CB]. R11 If O is the circumcenter of triangle ABCABC and M is the midpoint of ABAB then ∠[AO,OM]=∠[AC,BC] [AO,OM]= [AC,BC]. R12 If MA=MBMA=MB and A,B,P,MA,B,P,M are cyclic then ∠[PA,PM]=∠[PM,PB] [PA,PM]= [PM,PB]. R13 ∠[AB,CD]=−∠[CD,AB] [AB,CD]=- [CD,AB]. R14 For any line UVUV, ∠[AB,CD]=∠[AB,UV]+∠[UV,CD] [AB,CD]= [AB,UV]+ [UV,CD]. R15 If coll(A,X,U)coll(A,X,U), coll(P,X,R)coll(P,X,R), and cyclic(X,P,Q,U)cyclic(X,P,Q,U), then by R14, R6, and R10 ∠[AX,BC]=∠[AX,XP]+∠[XP,BC]=∠[QU,QP]+∠[PR,BC] [AX,BC]= [AX,XP]+ [XP,BC]= [QU,QP]+ [PR,BC]. R16 If coll(X,C,D)coll(X,C,D), coll(X,U,A)coll(X,U,A), coll(X,V,B)coll(X,V,B), cyclic(X,U,C,E)cyclic(X,U,C,E), and cyclic(X,V,D,F)cyclic(X,V,D,F), then by R14, R6, and R10 ∠[AX,BX]=∠[AX,XC]+∠[XD,XB]=∠[EU,EC]+∠[FD,FV] [AX,BX]= [AX,XC]+ [XD,XB]= [EU,EC]+ [FD,FV]. R17 If XA=XBXA=XB and coll(X,A,W)coll(X,A,W) then by R14 and R9 ∠[AX,BX]=∠[AX,AB]+∠[AB,XB]=2∠[AX,AB]=2∠[AW,AB] [AX,BX]= [AX,AB]+ [AB,XB]=2 [AX,AB]=2 [AW,AB]. R18 If XA=XBXA=XB, coll(X,A,W)coll(X,A,W), and coll(A,B,U)coll(A,B,U) then by R14, R6 and R9 ∠[BX,CD]=∠[BX,AB]+∠[AB,CD]=∠[AU,AW]+∠[AU,CD] [BX,CD]= [BX,AB]+ [AB,CD]= [AU,AW]+ [AU,CD]. R19 If circumcenter(O,A,B,C)circumcenter(O,A,B,C) and midpoint(M,A,B)midpoint(M,A,B) then by R14, R6 and R11 ∠[AO,AB]=∠[AO,OM]+∠[OM,AB]=∠[AC,CB]+∠[1] [AO,AB]= [AO,OM]+ [OM,AB]= [AC,CB]+ [1]. R20 If cyclic(X,W,U,V)cyclic(X,W,U,V), coll(X,U,A)coll(X,U,A), and perp(X,V,P,Q)perp(X,V,P,Q) then ∠[AX,BC]=∠[AX,VX]+∠[VX,BC]=∠[WU,WV]+∠[PQ,BC]+∠[1] [AX,BC]= [AX,VX]+ [VX,BC]= [WU,WV]+ [PQ,BC]+ [1]. R21 If in-center(I,A,B,C)in-center(I,A,B,C) then we have ∠[AI,AB]+∠[BI,BC]+∠[CI,CA]=∠[1] [AI,AB]+ [BI,BC]+ [CI,CA]= [1]. To organize the application of these rules, the full-angle method introduces a ranking system. We assume a total order on the points, denoted by “<<”. A full-angle ∠[AB,CD] [AB,CD] is in canonical form if A>BA>B, C≥DC≥ D, and either A>CA>C or (A=CA=C and B>DB>D). In the following, all full-angles are assumed to be written in canonical form. The ranking between two full-angles is defined lexicographically. We write ∠[AB,CD]<∠[PQ,RS] [AB,CD]< [PQ,RS] if one of the following conditions holds: (1) A<PA<P; (2) A=PA=P and B<QB<Q; (3) A=PA=P, B=QB=Q, and C<RC<R; or (4) A=PA=P, B=QB=Q, C=RC=R, and D<SD<S. Based on this ranking, two control strategies restrict the application of inference rules: Control Strategy 1: A rule ℛR can be applied to ∠[AB,CD] [AB,CD] only if rank(∠[AB,CD])>rank(ℛ(∠[AB,CD]))rank( [AB,CD])>rank(R( [AB,CD])). Control Strategy 2: Rule R14 (line splitting) can be applied to ∠[AB,CD] [AB,CD] only if the resulting two full-angles can both be further reduced to lower rank. The first strategy requires each accepted transformation to lower the rank of the full-angle being reduced. The second places an additional restriction on R14, which introduces an intermediate line and replaces one full-angle by two. It permits this splitting operation only when both resulting terms admit further reductions. Together, these conditions suppress unproductive transformations and limit unnecessary growth of the proof-search space. Before the goal-directed proof begins, the prover constructs the GIB from the hypotheses. The GIB stores elementary geometric facts that can subsequently be used to instantiate and simplify the full-angle inference rules. For the problem considered below, the GIB is generated as follows: 1. Initialization: Add the hypotheses to the GIB: 2. Apply forward chaining rules to derive new information: • F1: If l1|l2l_1 l_2 and l1|l3l_1 l_3 then l2|l3l_2 l_3. • F2: If l1⟂l2l_1 l_2 then l1⟂l3l_1 l_3 iff l2|l3l_2 l_3. • F3: ABAB is the mediator of XYXY if and only if AX=AYAX=AY and BX=BYBX=BY. • F4: If midpoint(O,C,A)midpoint(O,C,A) then AB⟂BCAB BC iff circumcenter(O,A,B,C)circumcenter(O,A,B,C). • F5: If PA⟂PBPA PB then QA⟂QBQA QB iff cyclic(A,B,P,Q)cyclic(A,B,P,Q). • F6: If M and N are the midpoints of AB and AC then MN|BCMN BC. • F7: If ∠[OU,OP]=∠[OP,OV]≠∠[0] [OU,OP]= [OP,OV]≠ [0], OU⟂PUOU PU, and OV⟂PVOV PV then OU=OVOU=OV and PU=PVPU=PV. • F8: If AB|ACAB AC then coll(A,B,C).coll(A,B,C). 3. Iterate: Continue applying the forward chaining rules to the newly derived information until no new facts can be added to the GIB. 4. Final GIB: The GIB now contains the original hypotheses and the newly deduced information. This will be used by the prover during the backward chaining process to simplify and eliminate full-angles. For problems that require additional geometric information, the following auxiliary rules can also be used: • K1: l1|l2l_1 l_2 iff there is another line l3l_3 such that ∠[l1,l3]=∠[l2,l3] [l_1,l_3]= [l_2,l_3]. • K2: If l1⟂l2l_1 l_2 and l3⟂l4l_3 l_4 then ∠[l1,l3]=∠[l2,l4] [l_1,l_3]= [l_2,l_4]. • K3: A,B,C,A,B,C, and D are cyclic iff ∠[AB,AC]=∠[DB,DC] [AB,AC]= [DB,DC]. (The non-degenerate condition is ¬coll(A,B,C,D) (A,B,C,D).) • K4: OA=OBOA=OB iff ∠[OA,AB]=∠[AB,OB] [OA,AB]= [AB,OB]. (The non-degenerate condition is ¬coll(O,A,B) (O,A,B).) • K5: If MA=MBMA=MB and A,B,P,MA,B,P,M are cyclic then ∠[PA,PM]=∠[PM,PB] [PA,PM]= [PM,PB]. 2.2 IMO example We use the following geometry problem as a concrete instance for the quantum proof-search demonstration. In triangle ABCABC, AB=ACAB=AC. A circle is tangent to the circumcircle of triangle ABCABC and is tangent to ABAB and ACAC at points F and G, respectively. Show that the midpoint of segment FGFG is the incenter of triangle ABCABC. The geometric configuration is shown in Fig. S6. Figure S6: Schematic illustration of the IMO 1978 geometry problem. Point Order: A,B,C,D,E,F,G,HA,B,C,D,E,F,G,H Hypotheses: • cyclic(A,B,C,D)cyclic(A,B,C,D) (Points A,B,C,DA,B,C,D lie on a circle) • cong(A,B,A,C)cong(A,B,A,C) (AB=ACAB=AC) • circumcenter(O,A,B,C)circumcenter(O,A,B,C) (Point O is circumcenter of ABCABC) • foot(F,E,A,B)foot(F,E,A,B) (EF⟂ABEF AB) • foot(G,E,A,C)foot(G,E,A,C) (EG⟂ACEG AC) • cong(E,F,E,G)cong(E,F,E,G) (EF=EGEF=EG) • cong(E,F,E,D)cong(E,F,E,D) (EF=EDEF=ED) • coll(E,O,D)coll(E,O,D) (Points E,O,DE,O,D collinear) • cong(F,H,H,G)cong(F,H,H,G) (FH=HGFH=HG) • coll(F,G,H)coll(F,G,H) (Points F,G,HF,G,H collinear) Conclusion: • ∠HBA+∠HBC HBA+ HBC = 0 (Line BHBH bisects angle ABCABC) Before performing the full-angle proof search, we construct the GIB by deriving additional geometric relations from the hypotheses. For the present problem, the following relations are obtained: • cyclic(A,E,F,G)cyclic(A,E,F,G). Proof: EF⟂FAEF FA, EG⟂GAEG GA (F5). • AF=AGAF=AG. Proof: EF=EG→∠FAE=∠EAG→∠GEA=∠AEF→AF=AGEF=EG→ FAE= EAG→ GEA= AEF→ AF=AG (reverse of K5). • coll(A,H,E)coll(A,H,E), AE⟂FGAE FG. Proof: AF=AGAF=AG, EF=EGEF=EG (F3). • BD=CDBD=CD. Proof: ∠BAD=∠DAC BAD= DAC (reverse of K5). • BI=ICBI=IC, AD⟂BCAD BC. Proof: AB=ACAB=AC, BD=CDBD=CD (F3). • AO⟂BCAO BC. Proof: AB=ACAB=AC, BO=COBO=CO (F3). • coll(A,O,E)coll(A,O,E). Proof: AO⟂BCAO BC, AD⟂BCAD BC (F2, F8). • FG|BCFG BC. Proof: ∠[AD,BC]=∠[1]=∠[AD,FG] [AD,BC]= [1]= [AD,FG]. (F2). • EF|BDEF BD. Proof: ∠BDA=∠BCA=∠FGA=∠FEA BDA= BCA= FGA= FEA. (K1, K5). • AB⟂BDAB BD. Proof: EF|BDEF BD, EF⟂ABEF AB. (F2). • cyclic(F,H,D,B)cyclic(F,H,D,B). Proof: FH⟂HDFH HD, FB⟂BDFB BD. (F5). Together with the original hypotheses, these derived relations form the geometric information used in the subsequent full-angle reasoning. To simplify the GIB representation, parallel, collinear, and perpendicular relations are used to replace equivalent line representations by those with lower rank. The relevant geometric relations in this problem are CB|GFCB GF, FE|DBFE DB, coll(A,O,H,E,I,D)coll(A,O,H,E,I,D), coll(F,G,H)coll(F,G,H), coll(B,C,I)coll(B,C,I), EF⟂ABEF AB, EG⟂ACEG AC, AD⟂BCAD BC, and AB⟂BDAB BD. This simplification allows equivalent full-angles to be represented in lower-ranked forms. For example, ∠[HG,FE] [HG,FE] is written as ∠[HG,DB] [HG,DB] because FE|DBFE DB and coll(F,G,H)coll(F,G,H). Similarly, ∠[HG,FE] [HG,FE] can be expressed as ∠[HG,BA]+∠[1] [HG,BA]+ [1] using EF⟂ABEF AB. For this example, we use the basic rules R9, R10, and R12 to establish the angle relations. The corresponding geometric relations are: 1. R9: AB=ACAB=AC, EF=EGEF=EG, EF=EDEF=ED, AF=AGAF=AG, BD=CDBD=CD. 2. R10: cyclic(A,B,C,D)cyclic(A,B,C,D); cyclic(A,E,F,G)cyclic(A,E,F,G); cyclic(F,H,D,B)cyclic(F,H,D,B). 3. R12: AB=ACAB=AC and cyclic(A,B,C,D)cyclic(A,B,C,D); EF=EGEF=EG and cyclic(A,E,F,G)cyclic(A,E,F,G); AF=AGAF=AG and cyclic(A,E,F,G)cyclic(A,E,F,G); BD=CDBD=CD and cyclic(A,B,C,D)cyclic(A,B,C,D). The corresponding angle relations are: 1. R9: ∠ABC=∠BCA ABC= BCA, ∠EFG=∠FGE EFG= FGE, ∠EFD=∠FDE EFD= FDE, ∠AFG=∠FGA AFG= FGA, ∠DBC=∠BCD DBC= BCD. 2. R10: ∠ACB=∠ADB ACB= ADB, ∠ABC=∠ADC ABC= ADC, ∠ABD=∠ACD ABD= ACD, ∠BAC=∠BDC BAC= BDC, ∠BAD=∠BCD BAD= BCD, ∠CAD=∠CBD CAD= CBD; ∠AFE=∠AGE AFE= AGE, ∠AEF=∠AGF AEF= AGF, ∠AEG=∠AFG AEG= AFG, ∠EAF=∠EGF EAF= EGF, ∠EAG=∠EFG EAG= EFG, ∠FAG=∠FEG FAG= FEG; ∠FDH=∠FBH FDH= FBH, ∠FHD=∠FBD FHD= FBD, ∠FHB=∠FDB FHB= FDB, ∠HFD=∠HBD HFD= HBD, ∠HFB=∠HDB HFB= HDB, ∠DFB=∠DHB DFB= DHB. 3. R12: ∠ADB=∠CDA ADB= CDA, ∠EAF=∠GAE EAF= GAE,∠AEF=∠GEA AEF= GEA, ∠DAB=∠CAD DAB= CAD. These relations provide the geometric information from which the proof-search actions used later are constructed. In the following subsections, we describe how the corresponding formulas and proof states are represented on a quantum computer and how the reasoning operations act on them. 2.3 State representation of formulas The quantum proof-search framework operates on quantum representations of symbolic formulas. Two types of states play distinct roles. The proof state |St⟩|S_t represents the formula, or superposition of formulas, being processed at reasoning round t, whereas the knowledge-base state stores the hypotheses and other relations that may be used to support subsequent inferences. In our previous work [61], we showed that a knowledge base in conjunctive normal form (CNF) for propositional logic can be encoded as a quantum superposition in which each basis state represents a clause. Other symbolic objects can be represented in a similar manner. In the full-angle method considered here, the relevant formulas are full-angles [9]. At the beginning of the goal-directed search, the target formula is encoded as the initial proof state. For a classically specified target, this state can be prepared directly as a computational-basis product state. Each subsequent reasoning operation acts on |St⟩|S_t and produces the state |St+1⟩|S_t+1 . When successive reasoning circuits are composed coherently, the circuit depth required to prepare |St⟩|S_t increases linearly with the number of reasoning rounds t, provided that the depth of each reasoning operation is bounded as discussed below. The knowledge base provides the hypotheses and supporting relations used by these reasoning operations. If the knowledge base is specified classically, it can be loaded onto a quantum computer using an index register, following the encoding introduced in Ref. [61]. The situation is more general when new formulas derived during reasoning are also incorporated into the knowledge base. In that case, the updated knowledge base may either be constructed classically and re-encoded, or generated directly as a quantum state. For simple instances in which only a small number of formulas are added, classical updating is sufficient. For larger instances, one may instead retain the derived formulas coherently. Consider an extreme case in which every result produced at a reasoning round is new. If a knowledge base containing M formulas is combined with another copy of itself, pairwise reasoning produces up to M2M^2 derived formulas. If this enlarged knowledge base is used in the same way at the next step, the number of represented formulas can grow to M4M^4. Continuing this construction for t reasoning rounds gives a state representing up to M2tM^2^t formulas, while the circuit depth of the composed reasoning operations grows linearly with t. Alternatively, the initial knowledge base |KB0⟩ | KB_0 containing M formulas can be combined at every step with the current knowledge-base state |KBt⟩ | KB_t to produce |KBt+1⟩ | KB_t+1 . Under the corresponding counting assumption, the number of represented formulas then grows as MtM^t rather than M2tM^2^t. The circuit depth remains linear in t, while the number of index qubits required to label the formulas changes from 2tlog2M2^t _2M in the first construction to tlog2Mt _2M in the second. These estimates concern the number of formulas represented within a quantum state rather than the number of formulas extracted as classical outputs. Explicitly storing or reasoning over M2tM^2^t or MtM^t formulas as separate classical records would require correspondingly large classical memory. A quantum state, by contrast, can retain these formula labels in superposition. This does not imply an exponential quantum advantage for producing the same formulas explicitly in classical form. As discussed in Ref. [61], extracting a large knowledge base by measurement and sampling removes this representational separation. The distinction is therefore between maintaining a coherent quantum representation for subsequent reasoning and materializing the entire set of formulas as a classical data structure. The knowledge base used in the full-angle implementation is the geometry information base (GIB). It contains elementary and easily derived geometric relations [9]. In the present experiment, the GIB is constructed classically using the geometric rules introduced above and is then encoded for use by the quantum reasoning circuits. This classical preprocessing substantially simplifies the subsequent backward proof search [51]. More general implementations could instead generate or update parts of the supporting knowledge coherently, without reading out all intermediate formulas. To address formulas coherently within a large knowledge base, each formula is associated with an index register. For a knowledge base loaded directly from classical data, the encoding can be written as UKB|i⟩|⟩=|i⟩|Fi⟩, U_KB |i | 0 = |i |F_i , (S20) where UKBU_KB denotes the knowledge-base encoding unitary, i is the formula index, |⟩ | 0 is the initial state of the data register, and FiF_i is the i-th formula in the knowledge base. If a formula is generated coherently from two indexed premises, its index can be formed from the premise indices themselves. A reasoning operation can be written as UR|i⟩|j⟩|Fi⟩|Fj⟩|⟩=|i⟩|j⟩|Fi⟩|Fj⟩|R(Fi,Fj)⟩, U_ R |i |j |F_i |F_j | 0 = |i |j |F_i |F_j |R(F_i,F_j) , (S21) where URU_ R denotes the forward chaining reasoning circuit, and the pair (i,j)(i,j) serves as the index of the derived formula R(Fi,Fj)R(F_i,F_j). When formulas are generated under action selection, their indices can similarly incorporate both the index of the supporting formula and the selected action. The exact index structure depends on the architecture of the strategy engine. For example, the strategy engine may process |St⟩⊗|KBt⟩|S_t |KB_t or, when two supporting relations are required, |St⟩⊗|KBt⟩⊗|KBt⟩|S_t |KB_t |KB_t . Different choices change the information available for action selection and lead to different requirements for circuit design and optimization. A systematic analysis of these alternatives is beyond the scope of the present work. The index register specifies which formula is being addressed, while a separate data register encodes the formula itself. The number of index qubits grows logarithmically with the number of represented formulas. The cost of the data register instead depends on the complexity of an individual formula. In the representation used here, a formula with N variables requires N qudits, with each qudit having a local value set of cardinality |V||V|. A qubit implementation therefore requires Nlog2|V|N _2|V| qubits for the formula data. For example, the CNF encoding introduced in Ref. [61] uses two qubits for each propositional variable. The four basis states |00⟩|00 , |01⟩|01 , |10⟩|10 , and |11⟩|11 represent absence, positive, negative, and resolved status, respectively. In the full-angle representation used here, a formula ±∠[DB,CA]± [DB,CA] is encoded as |±⟩|D⟩|B⟩|C⟩|A⟩ |± |D |B |C |A . The first register represents the sign, while the remaining registers encode the point indices. For instance, −∠[DB,CA]- [DB,CA] is represented by the basis state |13120⟩ |13120 , where the first digit denotes the negative sign and the remaining digits encode the ranks of D, B, C, and A, respectively. With these representations, the proof state, supporting knowledge, and formula indices can all be processed directly by quantum circuits. The next subsection describes the reasoning engine that implements the formal transformations between such encoded formulas. 2.4 Reasoning engine The reasoning engine shown in Fig. S5 serves as the logical inference module in the QATP framework. It implements the formal inference rules of the underlying logic system and transforms the formulas at one reasoning round into those at the next step according to the selected inference rule. The reasoning circuit takes three types of input: (i) the quantum state representing the formulas at the current reasoning round, (i) an action state specifying which inference rule is applied and which hypotheses from the knowledge base are used, and (i) the quantum-encoded knowledge base containing the available hypotheses. The structure of the reasoning engine directly reflects the inference rules of the logic system, and its concrete implementation depends on the chosen encoding of symbolic formulas. A key feature of the quantum proof-search framework is that the reasoning engine can operate coherently on formulas represented in superposition. Quantum parallelism allows the same inference procedure to act simultaneously on the different formulas encoded in the input state. For the examples considered below, the corresponding reasoning circuits have constant depth or a depth that grows only mildly with the cardinality of the local value set. Consequently, even when the proof state represents a superposition of many formulas, the inference operation can be carried out without processing these formulas one by one. We first recall the quantum resolution circuit introduced in Ref. [61]. Each propositional variable can take one of four local values: absence, positive, negative, and resolved. The resolution circuit acts on all propositional variables in parallel and resolves literals with opposite polarity in the two premise clauses. As a result, the circuit depth of the resolution operation itself does not increase with the number of propositional variables. As a second example, we consider rule R9 of the full-angle method. This example illustrates how a full-angle inference rule can be implemented as a quantum reasoning circuit. We assume that the strategy engine has selected rule R9 and specified the hypotheses to be used. Under this assumption, the reasoning engine applies the corresponding inference to the input formula state. Consider a knowledge base containing three indexed geometric relations: 00:AC=ABAC=AB, 01:FE=FDFE=FD, and 10:GF=GAGF=GA. In the full-angle method, this knowledge base, or geometry information base (GIB), is encoded as a unitary operation that loads the corresponding full-angle representations into the data register conditioned on the action state: UKB|00⟩|⟩=|00⟩|−∠[CB,BA]⟩|∠[CB,CA]⟩, U_ KB |00 | 0 = |00 |- [CB,BA] | [CB,CA] , UKB|01⟩|⟩=|01⟩|−∠[FD,ED]⟩|∠[FE,ED]⟩, U_ KB |01 | 0 = |01 |- [FD,ED] | [FE,ED] , UKB|10⟩|⟩=|10⟩|−∠[GA,FA]⟩|∠[GF,FA]⟩. U_ KB |10 | 0 = |10 |- [GA,FA] | [GF,FA] . (S22) The first line corresponds to the equation ∠[CB,CA]=−∠[CB,BA] [CB,CA]=- [CB,BA], which encodes the geometric relation AC=ABAC=AB under rule R9. Here we consider only the forward application of the rule, since the control strategy requires that the rank of the formula be reduced during inference; analogous considerations apply to the other relations. The unitary UKBU_ KB can be obtained by direct encoding, brute-force forward chaining, or forward chaining guided by the strategy engine. The translation between geometric relations (e.g., AC=ABAC=AB) and full-angle relations (e.g., ∠[CB,CA]=−∠[CB,BA] [CB,CA]=- [CB,BA]) under a given rule is straightforward and is not the focus here. The reasoning task is to reason on an unknown input state |±∠[ZX,YW]⟩ |± [ZX,YW] , where points Z,X,Y,WZ,X,Y,W may coincide. We first consider the case in which the action state is |00⟩ |00 , corresponding to the relation AC=ABAC=AB. The circuit shown in Fig. S7a compares the input state |±∠[ZX,YW]⟩ |± [ZX,YW] with the state |∠[CB,CA]⟩ | [CB,CA] using auxiliary qubits. If the comparison indicates equality, the output register is prepared in the state |∓∠[CB,BA]⟩ |∓ [CB,BA] ; otherwise, the original input state |±∠[ZX,YW]⟩ |± [ZX,YW] is preserved. After the operation, all auxiliary qubits are reset. The unitary UWU_W shown in Fig. S7 implements a controlled copy operation conditioned on the comparison outcome. When the outcome is “same”, UWU_W writes the conclusion state to the output register and flips the sign qubit accordingly; when the outcome is “different”, it copies the original input state to the output register. Figure S7: Quantum circuit implementing rule R9. a, Reasoning circuit for the input state |±∠[ZX,YW]⟩ |± [ZX,YW] based on the rule equation ∠[CB,CA]=−∠[CB,BA] [CB,CA]=- [CB,BA]. The circuit first compares the input state |±∠[ZX,YW]⟩ |± [ZX,YW] with the premise of the rule equation. If the comparison yields the state |same⟩ | same , namely [ZX,YW]=[CB,CA][ZX,YW]=[CB,CA], the circuit UWU_W outputs the conclusion |∓∠[CB,BA]⟩ |∓ [CB,BA] ; otherwise, it leaves the input state unchanged. b, Circuit for comparing two n-qubit registers |x⟩ |x and |y⟩ |y . In this illustration, each register contains two qubits. The circuit compares the two registers qubit by qubit. The CX gates between corresponding qubits of |x⟩ |x and |y⟩ |y map each qubit in the |y⟩ |y register to |0⟩ |0 when the corresponding qubits are the same and to |1⟩ |1 when they are different. The following X gates convert the equality condition into controls for an n-controlled NOT gate, which writes the comparison result to an ancillary qubit. The final gates uncompute the comparison operation and restore the input registers. For two n-qubit registers, the circuit contains 2n2n CX gates arranged in two parallel layers, 2n2n single-qubit X gates, and one n-controlled NOT gate. The latter can be implemented either with depth O(log2n)O( _2n) using O(n)O(n) auxiliary qubits, or directly using O(n)O(n) CX gates [4]. The ancillary output is |1⟩ |1 when the two registers are the same and |0⟩ |0 when they are different. If the action state is instead a superposition of |00⟩ |00 , |01⟩ |01 , and |10⟩ |10 , the same reasoning circuit remains valid. In this case, the output state becomes entangled with the action index, such that inference is performed with AC=ABAC=AB, FE=FDFE=FD, and GF=GAGF=GA conditioned on the respective action states. Moreover, if the input formula state is itself a superposition, the output is a superposition of the corresponding inference results. In other words, the reasoning circuit implements rule R9 simultaneously for all input formulas and all geometric relations in the GIB by exploiting quantum parallelism. Circuits for other inference rules can be constructed in a similar manner. Consequently, the action state produced by the strategy engine naturally contains two indices: one specifying which inference rule is applied, and the other specifying which hypothesis from the knowledge base is used. The circuit depth of the reasoning engine scales as O(|R|log|V|)O(|R| |V|), where |R||R| is the number of inference rules and |V||V| is the cardinality of the value set of variables. The linear dependence on |R||R| arises because inference rules are applied sequentially, while the logarithmic dependence on |V||V| follows from the decomposition of multi-qubit controlled operations, as illustrated in Fig. S7b and in the quantum resolution circuit of Ref. [61]. For the full-angle method considered here, |R|=21|R|=21, corresponding to the 21 classical full-angle inference rules, and |V|=8|V|=8, corresponding to the eight possible points A,B,…,HA,B,…,H in the example of Fig. S6. For propositional QATP in Ref. [61], |R|=1|R|=1 (resolution) and |V|=4|V|=4, corresponding to the four possible literal states: absence, positive, negative, and resolved. More broadly, this construction reflects a general pattern in symbolic reasoning: an inference step typically consists of checking whether the input matches the applicability pattern of a rule, and then performing the prescribed transformation once the match is confirmed. For this reason, the circuit design presented here is not limited to resolution in propositional logic or to the full-angle method, but applies more generally to a broad class of rule-based reasoning systems, thereby illustrating the generality of the QATP framework. Finally, we emphasize that the number of variables N—or, in the full-angle setting, the number of points or full-angles appearing in a formula—does not affect the depth of the reasoning circuit. This is because inference on different variables can be performed in parallel. Tasks such as verifying whether a reasoning result is valid (e.g., checking that exactly one variable is resolved in quantum resolution) are not handled by the reasoning engine itself. Instead, these tasks are delegated to the strategy engine and the value function evaluation, which together guide the selection of inference rules and hypotheses and enforce the validity of the reasoning process. 2.5 Strategy engine and value function Within the proof-search framework, the strategy engine determines the reasoning actions to be considered, while the evaluation circuit assesses the resulting reasoning states and provides information for improving action selection. In the implementation considered here, the strategy engine is realized as a variational quantum circuit whose parameters determine the distribution over candidate actions. The evaluation circuit provides signals that are used to optimize these parameters. We do not attempt to give a comprehensive analysis of the expressive power of the strategy engine, the optimization landscape, or the complexity of circuit compilation. Instead, we present two heuristic scenarios to illustrate how quantum superposition and interference may be useful for action selection and strategy evaluation. These examples are intended as illustrative constructions rather than formal complexity-theoretic guarantees. More general training schemes, including reinforcement-learning-based optimization over multi-step proof trajectories, are left for future work. The first scenario considers a simple setting with three possible formulas, F1:|00⟩F_1: |00 , F2:|01⟩F_2: |01 , and F3:|10⟩F_3: |10 , together with two available reasoning actions. Action |0⟩ |0 derives F3F_3 from either F1F_1 or F2F_2, whereas action |1⟩ |1 maps F1F_1 to F2F_2 and F2F_2 to F1F_1. For the input formula F1F_1, both actions are reasonable, since action |0⟩ |0 produces the new formula F3F_3 and action |1⟩ |1 produces the new formula F2F_2. The same holds for the input formula F2F_2. It is therefore natural for the strategy engine to assign equal weight to the two actions in both cases. A Hadamard gate acting on the second qubit realizes exactly this behavior: it prepares the action state (|0⟩+|1⟩)/2( |0 + |1 )/ 2 for F1F_1 and (|0⟩−|1⟩)/2( |0 - |1 )/ 2 for F2F_2. The same gate also yields appropriate behavior for superposed inputs. In particular, when the input is (|F1⟩+|F2⟩)/2( |F_1 + |F_2 )/ 2, the amplitude of action |1⟩ |1 vanishes by destructive interference, so that only action |0⟩ |0 remains. This is desirable because action 11 merely exchanges F1F_1 and F2F_2 and therefore produces no new formula for this superposed input, whereas action 00 generates the new formula F3F_3. More generally, a single Hadamard gate already provides a suitable strategy for the three relevant inputs F1F_1, F2F_2, and (|F1⟩+|F2⟩)/2( |F_1 + |F_2 )/ 2. This example illustrates that even a very simple quantum strategy engine can adapt coherently to different reasoning states and automatically suppress actions that are unproductive for the current superposed input. By contrast, a classical strategy engine would generally need to query the input formulas separately in order to determine which formulas are present and whether a given action can generate new information. The second scenario is inspired by the Deutsch-Jozsa algorithm [14]. Suppose that we need to evaluate the performance of two strategy engines. The first is completely ineffective: under the actions generated by this strategy, every reasoning output coincides with its input. For an input state ∑m=1M|Fm⟩/MΣ _m=1^M |F_m / M, the resulting output state is ∑m=1M|Fm⟩|Fm⟩/MΣ _m=1^M |F_m |F_m / M. The second strategy engine is more effective: for half of the possible inputs, the reasoning result differs from the input. For the same input superposition, the output state becomes ∑m=1M|Fm⟩|Ff(m)⟩/MΣ _m=1^M |F_m |F_f(m) / M, where f(m)=mf(m)=m holds for exactly half of the values of m. After applying a comparison circuit between the input and output registers and storing the comparison result in an auxiliary qubit, where the comparison circuit is of the type shown in Fig. S7b, distinguishing these two cases reduces to a task analogous to that addressed by the Deutsch-Jozsa algorithm. In this sense, the value-evaluation circuit can exploit quantum parallelism to assess whether a strategy engine is entirely unproductive or generates genuinely new reasoning outcomes for half of the all possible input formulas. We emphasize that these scenarios are deliberately constructed examples and may not reflect the typical situations encountered during the actual learning process of the quantum proof-search system. We also acknowledge that a classical algorithm could efficiently solve these tasks if granted direct access to the relevant oracle information. The purpose of these examples is therefore not to claim a rigorously established exponential quantum advantage in a standard classical input-output setting, but rather to illustrate the possibility that certain tasks within QATP may benefit from quantum strategy engines and quantum value-evaluation circuits. In particular, when quantum states or quantum circuits are provided as inputs and coherent quantum states are retained throughout the computation, superposition states can represent exponentially many formulas and action paths simultaneously, and quantum interference between different reasoning paths can be exploited [60]. This suggests that, in suitably structured instances of quantum automated theorem proving, quantum advantages analogous to those found in algorithms based on the quantum Fourier transform (QFT) [12, 57], the Deutsch-Jozsa algorithm [14], and Simon’s algorithm [58] may also emerge. 2.6 Real circuit 2.6.1 Circuit of reasoning engine In our experiment, we encode lines rather than points in order to reduce the number of qubits required to represent full-angles on a quantum computer. To further reduce the qubit cost and circuit depth, we exclude parallel and collinear lines from the encoding. Under this convention, the first component of a full-angle involves three possible lines, encoded as HD:00, HB:01, and FD:10, while the second component involves four possible lines, encoded as FD:00, DB:01, BC:10, and BA:11. At the level of circuit design, there is a tradeoff between generality and implementation overhead. Following the general construction of the reasoning circuit introduced above, one may regard each inference rule, such as R9, R10, or R12, as a distinct strategy, and then build a reasoning circuit that matches the input formula against both the selected inference rule and the geometric relation in the GIB to which the rule is applied. An advantage of this approach is that the circuit depth does not increase with the number of geometric relations stored in the GIB, since the matching can be carried out coherently in parallel. However, for the present experiment on superconducting processors, such a construction introduces substantial overhead and is difficult to implement reliably. We therefore adopt a more concrete compilation scheme. Instead of treating an entire inference rule as a single strategy, we treat each explicit equality between full-angles obtained from applying an inference rule to a specific geometric relation in the GIB as an independent strategy. Under this scheme, the corresponding circuits are much easier to design and implement. The cost is that the number of available actions increases with the number of explicit equalities included in the compiled reasoning scheme, and the circuit depth grows accordingly. Nevertheless, when both the GIB and the set of inference rules are small, this overhead remains acceptable for near-term devices. Importantly, this simplification preserves the coherent action of the reasoning circuit on superposed proof states and action states. For a superposition of candidate inputs, the compiled circuit applies the corresponding symbolic transformations coherently to all components to which the selected actions are applicable. If multiple reasoning rounds are composed coherently without intermediate measurements, the proof state can in principle contain a rapidly growing number of reasoning branches, potentially representing an exponentially large space of reasoning paths. In the present experiment, however, the proof search is implemented round by round: the output is measured after each round and the selected result is used to prepare the input state for the next round. Thus, the experiment does not directly realize coherent multi-round growth of the proof-path superposition. We nevertheless adopt the compiled scheme because it retains the coherent symbolic reasoning within each quantum circuit while substantially reducing the hardware overhead. The relevant equalities used in the present proof are listed below: 1. R9: ∠[HD,FD]=∠[FD,DB] [HD,FD]= [FD,DB] 2. R10: ∠[HB,BA]=∠[HD,FD] [HB,BA]= [HD,FD], ∠[FD,DB]=−∠[HB,BC] [FD,DB]=- [HB,BC] In the line-index representation, these relations become 1. R9: ∠[00,00]=∠[10,01] [00,00]= [10,01] 2. R10: ∠[01,11]=∠[00,00] [01,11]= [00,00], ∠[10,01]=−∠[01,10] [10,01]=- [01,10] For convenience, we also write the proof sequence explicitly: ∠[HB,BA]+∠[HB,CB]=∠[HD,FD]+∠[HB,CB]=∠[FD,DB]+∠[HB,CB]=−∠[HB,CB]+∠[HB,CB]=∠0 [HB,BA]+ [HB,CB]= [HD,FD]+ [HB,CB]= [FD,DB]+ [HB,CB]=- [HB,CB]+ [HB,CB]= 0. In the line-index representation, this proof sequence becomes ∠[1,3]=∠[0,0]=∠[2,1]=−∠[1,2] [1,3]= [0,0]= [2,1]=- [1,2]. Figure S8: Quantum reasoning circuit for IMO example. a, Overall structure of the 12-qubit circuit. The first two qubits encode the action AtA_t, the next five qubits represent the proof state St+1S_t+1 at reasoning round t+1t+1, and the final five qubits represent the proof state StS_t at reasoning round t. The CNOT gates first copy the computational-basis encoding of StS_t to the St+1S_t+1 register, so that the state is preserved when no effective action is applied. Then the action-controlled unitary UAU_A is performed on AtA_t and St+1S_t+1. b, Decomposition of UAU_A into action-conditioned mapping blocks. Each block implements the angle-state transformation associated with one action, including both positive and negative versions of the relevant full-angle relation. The terms explicitly shown correspond to the transitions used in the present proof, while the omitted terms complete the unitary on the remaining basis states and leave unchanged those states to which no effective action applies. The core part of each reasoning round uses 12 qubits as shown in Fig. S8. The first two qubits encode the action index, the next five qubits represent the proof state St+1S_t+1 at reasoning round t+1t+1, and the final five qubits represent the proof state StS_t at reasoning round t. Before applying the reasoning operation, we first copy the proof state StS_t to the middle five qubits. This initialization ensures that the state remains unchanged when no effective action is applied. We then implement the unitary UAU_A, shown in Fig. S8b, which performs an action-controlled update of the state St+1S_t+1 conditioned on both the action index and the matched component of StS_t: UA= U_A= |00⟩⟨00|⊗I⊗|1001⟩⟨0000|⊗I⊗|0000⟩⟨0000| |00 00 | I |1001 0000 | I |0000 0000 | + + |01⟩⟨01|⊗I⊗|0000⟩⟨0111|⊗I⊗|0111⟩⟨0111| |01 01 | I |0000 0111 | I |0111 0111 | + + |10⟩⟨10|⊗X⊗|0110⟩⟨1001|⊗I⊗|1001⟩⟨1001| |10 10 | X |0110 1001 | I |1001 1001 | + + ⋯. ·s. (S23) More specifically, when the action qubits are fixed to a given basis state, UAU_A updates the St+1S_t+1 register according to the selected action, provided that the corresponding component in StS_t matches the required input relation. For example, when the action register is |00⟩ |00 , the unitary maps the component |0000⟩ |0000 in St+1S_t+1 to |1001⟩ |1001 , conditioned on the matched component |0000⟩ |0000 in StS_t, thereby implementing the transition ∠[HD,FD]→∠[FD,DB] [HD,FD]→ [FD,DB]. The terms shown in Eq. (S23) are the transitions used in the present proof, while the omitted terms complete the unitary on the remaining basis states and leave unchanged those states to which no effective action applies. 2.6.2 Circuit for the value function In the general proof-search framework, the evaluation circuit provides signals that characterize the result of a reasoning action and can be used to guide the optimization of the strategy engine. In the present implementation, we use a simple evaluation criterion based on a coherent comparison between the proof states at two consecutive reasoning rounds, t and t+1t+1. This criterion favors actions that produce a nontrivial update of the proof state and suppresses an unused action state in the two-qubit action register. More general evaluation functions, including those that account for longer reasoning trajectories, are left for future work. The loss function used in the experiment is constructed from two measurement-derived contributions, L=P1+P2. L=P_1+P_2. (S24) Both terms are extracted from the joint measurement statistics according to P1 P_1 =Pr!(St⊕S~t+1=00000),P2 = ! (S_t St+1=00000 ),\ P_2 =Pr!(At=11,St⊕S~t+1≠00000). = ! (A_t=11,S_t St+1≠ 00000 ). (S25) The first contribution collects the total probability of joint measurement events in which the two proof-state registers return the same outcome. As illustrated in Fig. S9, five CNOT gates map the bitwise difference of the two proof-state outcomes onto the comparison register, for which the outcome “00000” corresponds to equal results. The second contribution collects events associated with the unused action outcome “11” only when the two proof-state measurement outcomes are different, so that events already included in P1P_1 are not counted again. The remaining three action outcomes, 00”, 01”, and “10”, correspond to the three implemented reasoning actions. Figure S9: The quantum circuit to measure P1P_1 in Eq. (S24). This circuit coherently compares the formulas at steps t and t+1t+1. The measurement result is “00000” when the corresponding components in the two proof states are identical. As an example, consider the input state 3/5|00110⟩⊗|00110⟩−4/5|00010⟩⊗|10100⟩3/5 |00110 |00110 -4/5 |00010 |10100 , which represents the superposition of two reasoning processes: one in which the formula “00110”(+∠[HB,BC]+ [HB,BC]) remains unchanged, and another in which the formula “10100”(−∠[HB,FD]- [HB,FD]) is derived from “00010” (+∠[HD,BC]+ [HD,BC]). After this circuit, the state evolves to 3/5|00000⟩⊗|00110⟩−4/5|10110⟩⊗|10100⟩3/5 |00000 |00110 -4/5 |10110 |10100 . The |00000⟩ |00000 on the first five qubits indicates that the corresponding proof-state component is unchanged. Sampling the measurement outcomes yields P1=9/25P_1=9/25. By optimizing the action circuit to reduce this probability, the fraction of reasoning actions that produce no new formulas can be suppressed. 2.6.3 Circuit of strategy engine Figure S10: Variational circuit used to determine the action register AtA_t at reasoning round t. In the encoding of the proof state StS_t, the first qubit represents the sign and the remaining four qubits encode the indices of the two lines in the full-angle. Each qubit in the action register is entangled with the line-index qubits in StS_t, while single-qubit rotation gates are inserted before and after the two-qubit entangling gates to enhance the expressive power of the circuit. The circuit contains 16 variational parameters. We use a variational circuit to determine the action index at each reasoning round. In this work, the action at the t-th step, denoted by AtA_t, is determined solely by the proof state at the same step, StS_t. The circuit is designed so that each qubit in the action register interacts with the qubits in StS_t that encode the geometric content relevant for action selection. To enhance the expressive power of the ansatz, each two-qubit entangling gate is accompanied by single-qubit rotation gates. This hardware-efficient design allows the circuit to represent a rich family of action-selection policies. In future extensions, more expressive circuits may be employed to decide actions based on multiple copies of formulas in the current proof state as well as information stored in the GIB. 3 Experiment 3.1 Device information The superconducting quantum processor utilized in this work employs an 11×11 array of frequency-tunable transmon qubits arranged on a two-dimensional square lattice. In addition, the processor includes 220 couplers mediating nearest-neighbor interaction and 121 resonators for qubit state readout. All quantum reasoning circuits are realized through single-qubit, two-qubit, and measurement gates. - Single-qubit gates. Arbitrary single-qubit gates are implemented through a combination of microwave XYXY rotations and virtual Z rotations. All microwave pulses employ Gaussian envelopes with a duration of 24 ns and utilize DRAG modulation to mitigate leakage errors during fast gate operations [8]. We assess single-qubit gate errors via simultaneous cross-entropy benchmarking (XEB). A summary of single-qubit parameters, such as the energy relaxation times T1T_1, the spin-echo dephasing times T2SET_2^SE and gate errors, is displayed in the second and third columns of Fig. S11. It should be noted that all coherence times are measured simultaneously at the qubit idle frequencies. - Two-qubit gates. The specific two-qubit gate employed in the experiments is the controlled-phase (CPCP) gate. The CPCP gate with a control phase ϕφ can be defined as CP(ϕ)=(100001000010000eiϕ). CP(φ)= pmatrix1&0&0&0\\ 0&1&0&0\\ 0&0&1&0\\ 0&0&0&e^iφ\\ pmatrix. (S26) The realization of the CPCP gate relies on tuning the states |11⟩|11 and |20⟩|20 (or |02⟩|02 ) near resonance and activating qubit-qubit coupling to accumulate a ϕφ (where ϕ∈π2,π,3π2φ∈\ π2,π, 3π2\ in this work) phase shift. This process completes in 44 ns. The detailed calibration methods can be found in ref. [35]. As shown in Fig. S12, we perform parallel CPCP gates based on a variety of distinct patterns. We assess gate errors by performing simultaneous XEB, in which we execute circuits comprising multiple cycles; each cycle consists of two random single-qubit π/2π/2 rotations on both qubits followed by one CPCP gate. The XEB cycle errors are shown in the third column of Fig. S11. - Measurement gates. Our quantum processor utilizes a frequency multiplexed dispersive readout scheme. There are 16 readout lines each of which couples to multiple qubit-resonator pairs. Measurement gates are implemented through microwave pulses with custom-designed envelopes. We optimize the readout pulse power, readout pulse length, and qubit frequency during readout to maximize measurement performance. Furthermore, to enhance readout fidelity, we apply an additional microwave pulse to drive the transition of |1⟩↔|2⟩|1 |2 prior to the readout pulse. Readout errors, displayed in the fourth column of Fig. S11, are quantified by preparing random bitstring quantum states and calculating the probability of misclassified states. Figure S11: Device layout and performance for different quantum circuits. a-e, Device layout and integrated histograms of device parameters. Panels in the first column: Blue dots (bars) denote active qubits (couplers) which are selected for different quantum circuits. The numbers of qubits are 21, 32, 28, 28, 17, respectively. Panels in the second column: Cumulative distributions of qubit energy relaxation time T1T_1 (blue line) and spin echo dephasing time T2SET_2^SE (red line). Panels in the third column: Pauli errors of simultaneous single-qubit gates (purple line) and cycle Pauli errors of two-qubit CPCP gates (brown line). Panels in the fourth column: Readout errors of state |0⟩|0 (orange line) and |1⟩|1 (green line). Vertical dashed lines indicate the median values. Figure S12: Patterns of parallel CPCP gates. The gray chip layout is shown as a visual reference, while colored circles and lines indicate the active qubits and couplers, respectively, involved in implementing the CPCP gates. There are three types of CPCP gates parameterized by different control phases. We group them into separate patterns according to whether they can be executed without conflicts. The gate count and type may vary across different patterns. In this work, the total number of patterns is 201. 3.2 Circuit and layout In this section, we introduce details associated with the quantum circuits executed in our experiments. To execute the theoretical circuits with our quantum processor, we apply two pre-processing procedures including multi-qubit gate optimization and quantum circuit compilation. Figure S13: The theoretical quantum circuit of step 4 executed in the algebraic theorem proving. This circuit involves 28 logical qubits, multiple types of quantum gates and 6 necessary Z basis measurement gates for the result extraction. Here, β = arccos13arccos\ 13. 3.2.1 Multi-qubit gate optimization Multi-qubit controlled gates are important building blocks of quantum circuits, enabling complex conditional operations. Unlike single-qubit rotations and several two-qubit gates, however, direct and high-fidelity implementations of multi-qubit controlled gates remain challenging on most quantum processors, particularly for arbitrary groups of qubits. Therefore, high-level multi-qubit operations must be decomposed into sequences of single- and two-qubit gates for execution on quantum processors. Such decompositions must carefully account for the noise and hardware constraints of noisy intermediate-scale quantum (NISQ) devices. As an example, the theoretical quantum circuit shown in Fig. S13 contains several multi-qubit gates, such as controlled-controlled-X (CCXCCX) and controlled-controlled-controlled-X (CCCXCCCX) gates. Decomposing them into the universal gate set U,CX\U,CX\ generates long gate sequences (see Fig. S14a). The arbitrary single-qubit U and two-qubit CXCX gates can be expressed as U(θ,φ,λ)=(cosθ2−eiλsinθ2eiφsinθ2ei(φ+λ)cosθ2) U(θ, ,λ)= pmatrixcos\ θ2&-e^iλsin\ θ2\\ e^i sin\ θ2&e^i( +λ)cos\ θ2\\ pmatrix (S27) and CX=(1000010000010010). CX= pmatrix1&0&0&0\\ 0&1&0&0\\ 0&0&0&1\\ 0&0&1&0\\ pmatrix. (S28) Such sequences not only increase circuit overhead, but also exacerbate decoherence effects, which degrade the fidelity of circuit results. To maximally suppress these detrimental impacts while preserving circuit validity, we adopt optimized implementations of the CCXCCX and CCCXCCCX gates up to a relative phase [48]. As shown in Fig. S14b, we achieve an approximate 50%\% reduction in both quantum gate count and circuit depth relative to the original implementation. We remark that reduction in the number of gates, especially error-prone two-qubit gates, is particularly valuable as they are one of the most significant error sources in current NISQ devices. Figure S14: The original (a) and optimized (b) implementations of the CCXCCX and CCCXCCCX gates. It should be noted that the decomposition of CCXCCX and CCCXCCCX gates into sequences of U and CXCX gates is not unique. However, the minimal number of required CXCX gates is the same. For notational simplicity, we ignore the parameters of different U gates. 3.2.2 Quantum circuit compilation Quantum circuit compilation is the critical translation layer that bridges theoretical quantum circuits and physical hardware. This process involves mapping and routing qubits for limited connectivity, transpiling circuit with native gate set and scheduling gates to minimize idle times and crosstalk. With several two-qubit gates requiring long range interactions, the theoretical quantum circuits after optimization can still not be executed with our superconducting quantum processor featuring the nearest-neighbor coupling architecture. To address this constraint, we adopt SWAP-based bidirectional heuristic algorithm (SABRE) to dynamically map logical qubits in the theoretical circuits to physical qubits on the quantum processor based on actual coupling layout [42]. We prioritize assignments that minimize long-range two-qubit gates and use SWAP gates for unavoidable non-adjacent interactions. For instance, a theoretical circuit piece (Fig. S15a) needed to be executed utilizing three physical qubits Q1,Q2,Q3Q_1,Q_2,Q_3 on our superconducting quantum processor. The coupling layout for these physical qubits is depicted in Fig. S15b. Suppose that we map logical and physical qubits according to the relations listed in the Table (Fig. S15c). The first two CPCP gates can be executed directly. But for the third, we must insert a SWAP gate to route the states of Q2Q_2 and Q3Q_3, which enables the necessary interactions. The transformed circuit is shown in Fig. S15d. Figure S15: A simple example for qubit mapping and routing. a, A piece of the theoretical quantum circuit shown in Fig. S13. b, A coupling layout for a chain consisting of three physical qubits. c, The table of qubit mapping relations. d, The transformed circuit corresponds to the circuit in a. We insert a SWAP gate to reposition Q2Q_2 and Q3Q_3 for the third CPCP gate. e, A decomposition of SWAP gate. Following the initial transformation, the circuits are transpiled into our quantum processor’s native gate set U,CP\U,CP\. During this, we also apply a gate fusion optimization: whenever a few single-qubit gates act consecutively on the same qubit, we merge them into one equivalent gate through unitary matrix multiplication. This fusion step further reduces the total gate count and shortens the circuit depth. Next, we schedule the single-qubit and CPCP gates into separate, temporally isolated layers to minimize the effect of crosstalk. Furthermore, we rearrange them as close in time as possible to minimize qubit idle times between dependent gate operations, which suppresses the impact of decoherence. 3.2.3 Experimental circuits Beyond the pre-processing procedures described above, we additionally apply Pauli Twirling to four experimental circuits executed in the algebraic theorem proving. The Pauli twirling technique can suppress gate-dependent errors (e.g. coherent over-rotation or dephasing) by sandwiching the CP(π)CP(π) gates with 16 random Pauli gate combinations (see Fig. S16), leaving the overall function invariant. Figure S16: Equivalent circuit illustrating the Pauli Twirling. Pi(i=1,2,3,4)P_i\ (i=1,2,3,4) is a Pauli gate chosen to leave the CP(π)CP(π) gate invariant. For example, P1P_1 = P3P_3 = Y, P2P_2 = I, P4P_4 = Z. Figure S17: The experimental quantum circuit of step 4 executed in the algebraic theorem proving. As an example, we present the diagrams of the experimental quantum circuits corresponding to the theoretical quantum circuit shown in Fig. S13. As depicted in Fig. S17, this circuit comprises 28 physical qubits that are represented by blue dots in Fig. S11d. On the left, we annotate these physical qubits with their coordinates in the (row index, column index) format. In total, there are 202 single-qubit gates, 116 CPCP gates and 6 necessary Z basis measurement gates. The depth of this circuit is 80. 3.3 Additional results The measurement outcomes of step 2 and step 3 are shown in Fig. S18a and b, respectively. In both steps, one qubit is used for the exponent register because d only takes 00 or 11, and two qubits are used for the value register. For the point register, in step 2, depending on the specific values of each variable, we use 1, 2, 1 qubits to encode x1,x2,x3x_1,x_2,x_3, respectively. Similarly, in step 3, we use 2, 2 qubits to encode x1,x2x_1,x_2, respectively. In Fig. S18a and b, the x- and y-axes label the joint states of the point and value registers. The coefficient value represented by each two-qubit value state is indicated along the right-hand side. Figure S18: The experimental point-value correspondence of step 2 (a) and step 3 (b). a, The results of step 2 are classified into two sectors depending on the value of d and the x-axis labels the joint states of point qubits |x1x2x3⟩|x_1x_2x_3 . In this step, x1,x3∈0,1x_1,x_3∈\0,1\ and x2∈00,01,11x_2∈\00,01,11\. Colors indicate the probability obtained from 3000 runs of measurements, with each run taking 3000 shots. b, The results of step 3 are classified into two sectors depending on the value of d and the x-axis labels the joint states of point qubits |x1x2⟩|x_1x_2 . In this step, x1x_1, x2∈00,01,11x_2∈\00,01,11\. Colors indicate the probability obtained from 2940 runs of measurements, with each run taking 3000 shots. References [1] S. Aaronson and A. Ambainis (2014) The need for structure in quantum speedups. Theory of Computing 10 (6), p. 133–166. External Links: Document Cited by: §1. [2] A. A. Alemi, F. Chollet, N. Een, G. Irving, C. Szegedy, and J. Urban (2016) DeepMath—deep sequence models for premise selection. In Advances in Neural Information Processing Systems 29, p. 2235–2243. Cited by: §2. [3] 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) Quantum supremacy using a programmable superconducting processor. Nature 574 (7779), p. 505–510. External Links: Document Cited by: Abstract, Proving olympiad geometry theorems on a superconducting quantum processor. [4] A. Barenco, C. H. Bennett, R. Cleve, D. P. DiVincenzo, N. Margolus, P. Shor, T. Sleator, J. A. Smolin, and H. Weinfurter (1995) Elementary gates for quantum computation. Physical Review A 52 (5), p. 3457–3467. External Links: Document Cited by: Figure S7. [5] J. Biamonte, P. Wittek, N. Pancotti, P. Rebentrost, N. Wiebe, and S. Lloyd (2017) Quantum machine learning. Nature 549 (7671), p. 195–202. External Links: Document Cited by: Proving olympiad geometry theorems on a superconducting quantum processor. [6] 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), p. 58–65. External Links: Document Cited by: Proving olympiad geometry theorems on a superconducting quantum processor. [7] M. Cerezo, G. Verdon, H. Huang, L. Cincio, and P. J. Coles (2022) Challenges and opportunities in quantum machine learning. Nature Computational Science 2 (9), p. 567–576. External Links: Document Cited by: Proving olympiad geometry theorems on a superconducting quantum processor. [8] Z. Chen, J. Kelly, C. Quintana, R. Barends, B. Campbell, Y. Chen, B. Chiaro, A. Dunsworth, A. G. Fowler, E. Lucero, et al. (2016) Measuring and suppressing quantum state leakage in a superconducting qubit. Physical Review Letters 116 (2), p. 020501. External Links: Document Cited by: item -. [9] S. Chou, X. Gao, and J. Zhang (1996) Automated generation of readable proofs with geometric invariants: I. theorem proving with full-angles. Journal of Automated Reasoning 17 (3), p. 349–370. External Links: Document Cited by: §2.1, §2.1, §2.3, §2.3, §2, Proving olympiad geometry theorems on a superconducting quantum processor, Proving olympiad geometry theorems on a superconducting quantum processor. [10] S. Chou (1988) An introduction to Wu’s method for mechanical theorem proving in geometry. Journal of Automated Reasoning 4 (3), p. 237–267. External Links: Document Cited by: §1.1, §1, §1. [11] K. M. Collins, A. Q. Jiang, S. Frieder, L. Wong, M. Zilka, U. Bhatt, T. Lukasiewicz, Y. Wu, J. B. Tenenbaum, W. Hart, et al. (2024) Evaluating language models for mathematics through interactions. Proceedings of the National Academy of Sciences 121 (24), p. e2318124121. External Links: Document Cited by: §2. [12] D. Coppersmith (2002) An approximate Fourier transform useful in quantum factoring. Note: IBM Research Report RC 19642 External Links: quant-ph/0201067, Document, Link Cited by: §2.5. [13] S. Das Sarma, D. Deng, and L. Duan (2019) Machine learning meets quantum physics. Physics Today 72 (3), p. 48–54. External Links: Document Cited by: Proving olympiad geometry theorems on a superconducting quantum processor. [14] D. Deutsch and R. Jozsa (1992) Rapid solution of problems by quantum computation. Proceedings of the Royal Society of London. Series A: Mathematical and Physical Sciences 439 (1907), p. 553–558. External Links: Document Cited by: §2.5, §2.5. [15] V. Dunjko and H. J. Briegel (2018) Machine learning & artificial intelligence in the quantum domain: a review of recent progress. Reports on Progress in Physics 81 (7), p. 074001. External Links: Document Cited by: Proving olympiad geometry theorems on a superconducting quantum processor. [16] V. Dunjko, J. M. Taylor, and H. J. Briegel (2016) Quantum-enhanced machine learning. Physical Review Letters 117 (13), p. 130501. External Links: Document Cited by: Proving olympiad geometry theorems on a superconducting quantum processor. [17] 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) Quantum phases of matter on a 256-atom programmable quantum simulator. Nature 595 (7866), p. 227–232. External Links: Document Cited by: Proving olympiad geometry theorems on a superconducting quantum processor. [18] L. Egan, D. M. Debroy, C. Noel, A. Risinger, D. Zhu, D. Biswas, M. Newman, M. Li, K. R. Brown, M. Cetina, et al. (2021) Fault-tolerant control of an error-corrected qubit. Nature 598 (7880), p. 281–286. External Links: Document Cited by: Proving olympiad geometry theorems on a superconducting quantum processor. [19] M. Fitting (1996) First-order logic and automated theorem proving. 2 edition, Graduate Texts in Computer Science, Springer-Verlag, New York, NY. External Links: ISBN 978-0-387-94593-4, Document Cited by: Abstract. [20] X. Gao, Z. Zhang, and L. Duan (2018) A quantum machine learning algorithm based on generative models. Science Advances 4 (12), p. eaat9004. External Links: Document Cited by: Proving olympiad geometry theorems on a superconducting quantum processor. [21] Google Quantum AI and Collaborators (2025) Observation of constructive interference at the edge of quantum ergodicity. Nature 646 (8086), p. 825–830. External Links: Document Cited by: Abstract. [22] Google Quantum AI and Collaborators (2025) Quantum error correction below the surface code threshold. Nature 638 (8052), p. 920–926. External Links: Document Cited by: Proving olympiad geometry theorems on a superconducting quantum processor. [23] Google Quantum AI (2023) Suppressing quantum errors by scaling a surface code logical qubit. Nature 614 (7949), p. 676–681. External Links: Document Cited by: Proving olympiad geometry theorems on a superconducting quantum processor. [24] W. T. Gowers, B. Green, F. Manners, and T. Tao (2025) On a conjecture of Marton. Annals of Mathematics 201 (2), p. 515–549. External Links: Document Cited by: Abstract. [25] 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, New York, NY, p. 212–219. External Links: ISBN 978-0-89791-785-8, Document Cited by: §1. [26] 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), p. 633–638. External Links: Document Cited by: Abstract, Proving olympiad geometry theorems on a superconducting quantum processor. [27] 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), p. 259–263. External Links: Document Cited by: Proving olympiad geometry theorems on a superconducting quantum processor. [28] A. W. Harrow, A. Hassidim, and S. Lloyd (2009) Quantum algorithm for linear systems of equations. Physical Review Letters 103 (15), p. 150502. External Links: Document Cited by: Proving olympiad geometry theorems on a superconducting quantum processor. [29] O. Hasan and S. Tahar (2015) Formal verification methods. In Encyclopedia of Information Science and Technology, Third Edition, M. Khosrow-Pour (Ed.), p. 7162–7170. External Links: ISBN 978-1-4666-5888-2, Document Cited by: Abstract, Proving olympiad geometry theorems on a superconducting quantum processor. [30] V. Havlíček, A. D. Córcoles, K. Temme, A. W. Harrow, A. Kandala, J. M. Chow, and J. M. Gambetta (2019) Supervised learning with quantum-enhanced feature spaces. Nature 567 (7747), p. 209–212. External Links: Document Cited by: Proving olympiad geometry theorems on a superconducting quantum processor. [31] L. Hu, S. Wu, W. Cai, Y. Ma, X. Mu, Y. Xu, H. Wang, Y. Song, D. Deng, C. Zou, et al. (2019) Quantum generative adversarial learning in a superconducting quantum circuit. Science Advances 5 (1), p. eaav2761. External Links: Document Cited by: Proving olympiad geometry theorems on a superconducting quantum processor. [32] 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), p. 1182–1186. External Links: Document Cited by: Proving olympiad geometry theorems on a superconducting quantum processor. [33] 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. (2026) Olympiad-level formal mathematical reasoning with reinforcement learning. Nature 651 (8106), p. 607–613. External Links: Document Cited by: Abstract, §2, Proving olympiad geometry theorems on a superconducting quantum processor. [34] S. Jerbi, L. J. Fiderer, H. Poulsen Nautrup, J. M. Kübler, H. J. Briegel, and V. Dunjko (2023) Quantum machine learning beyond kernel methods. Nature Communications 14 (1), p. 517. External Links: Document Cited by: Proving olympiad geometry theorems on a superconducting quantum processor. [35] 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), p. 626–632. External Links: Document Cited by: item -, Proving olympiad geometry theorems on a superconducting quantum processor. [36] 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, New York, NY, p. 355–364. External Links: Document Cited by: §1. [37] C. Kaliszyk, J. Urban, H. Michalewski, and M. Olšák (2018) Reinforcement learning of theorem proving. In Advances in Neural Information Processing Systems 31, p. 8822–8833. Cited by: §2. [38] Y. Kim, A. Eddins, S. Anand, K. X. Wei, E. van den Berg, S. Rosenblatt, H. Nayfeh, Y. Wu, M. Zaletel, K. Temme, et al. (2023) Evidence for the utility of quantum computing before fault tolerance. Nature 618 (7965), p. 500–505. External Links: Document Cited by: Proving olympiad geometry theorems on a superconducting quantum processor. [39] A. D. King, A. Nocera, M. M. Rams, J. Dziarmaga, R. Wiersema, W. Bernoudy, J. Raymond, N. Kaushal, N. Heinsdorf, R. Harris, et al. (2025) Beyond-classical computation in quantum simulation. Science 388 (6743), p. 199–204. External Links: Document Cited by: Abstract. [40] S. Krinner, N. Lacroix, A. Remm, A. Di Paolo, E. Genois, C. Leroux, C. Hellings, S. Lazar, F. Swiadek, J. Herrmann, et al. (2022) Realizing repeated quantum error correction in a distance-three surface code. Nature 605 (7911), p. 669–674. External Links: Document Cited by: Proving olympiad geometry theorems on a superconducting quantum processor. [41] N. Lacroix, A. Bourassa, F. J. H. 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 colour code on a superconducting quantum processor. Nature 645 (8081), p. 614–619. External Links: Document Cited by: Proving olympiad geometry theorems on a superconducting quantum processor. [42] G. Li, Y. Ding, and Y. Xie (2019) Tackling the qubit mapping problem for NISQ-era quantum devices. In Proceedings of the Twenty-Fourth International Conference on Architectural Support for Programming Languages and Operating Systems, p. 1001–1014. External Links: Document Cited by: §3.2.2. [43] W. Li, Y. Ma, and D. Deng (2025) Pitfalls and prospects of quantum machine learning. Nature Computational Science 5 (12), p. 1095–1097. External Links: Document Cited by: Proving olympiad geometry theorems on a superconducting quantum processor. [44] Y. Liu, S. Arunachalam, and K. Temme (2021) A rigorous and robust quantum speed-up in supervised machine learning. Nature Physics 17 (9), p. 1013–1017. External Links: Document Cited by: Proving olympiad geometry theorems on a superconducting quantum processor. [45] S. Lloyd, M. Mohseni, and P. Rebentrost (2014) Quantum principal component analysis. Nature Physics 10 (9), p. 631–633. External Links: Document Cited by: Proving olympiad geometry theorems on a superconducting quantum processor. [46] D. W. Loveland (1978) Automated theorem proving: a logical basis. 1 edition, Fundamental Studies in Computer Science, Vol. 6, North-Holland Publishing Company, Amsterdam. External Links: ISBN 978-0-7204-0499-9 Cited by: Abstract. [47] L. S. Madsen, F. Laudenbach, M. F. Askarani, F. Rortais, T. Vincent, J. F. F. Bulmer, F. M. Miatto, L. Neuhaus, L. G. Helt, M. J. Collins, et al. (2022) Quantum computational advantage with a programmable photonic processor. Nature 606 (7912), p. 75–81. External Links: Document Cited by: Abstract, Proving olympiad geometry theorems on a superconducting quantum processor. [48] D. Maslov (2016) Advantages of using relative-phase Toffoli gates with an application to multiple control Toffoli optimization. Physical Review A 93 (2), p. 022311. External Links: Document Cited by: §3.2.1. [49] K. Mitarai, M. Negoro, M. Kitagawa, and K. Fujii (2018) Quantum circuit learning. Physical Review A 98, p. 032309. External Links: Document Cited by: Proving olympiad geometry theorems on a superconducting quantum processor. [50] 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) A race-track trapped-ion quantum processor. Physical Review X 13 (4), p. 041052. External Links: Document Cited by: Proving olympiad geometry theorems on a superconducting quantum processor. [51] A. J. Nevins (1975) Plane geometry theorem proving using forward chaining. Artificial Intelligence 6 (1), p. 1–23. External Links: Document Cited by: §2.3. [52] Z. Ni, S. Li, X. Deng, Y. Cai, L. Zhang, W. Wang, Z. Yang, H. Yu, F. Yan, S. Liu, et al. (2023) Beating the break-even point with a discrete-variable-encoded logical qubit. Nature 616 (7955), p. 56–60. External Links: Document Cited by: Proving olympiad geometry theorems on a superconducting quantum processor. [53] M. A. Nielsen and I. L. Chuang (2010) Quantum computation and quantum information. 10th Anniversary Edition edition, Cambridge University Press, Cambridge. External Links: ISBN 978-1-107-00217-3, Document Cited by: Abstract, Proving olympiad geometry theorems on a superconducting quantum processor. [54] W. Ren, W. Li, S. Xu, K. Wang, W. Jiang, F. Jin, X. Zhu, J. Chen, Z. Song, P. Zhang, et al. (2022) Experimental quantum adversarial learning with programmable superconducting qubits. Nature Computational Science 2 (11), p. 711–717. External Links: Document Cited by: Proving olympiad geometry theorems on a superconducting quantum processor. [55] Z. Z. Ren, Z. Shao, J. Song, H. Xin, H. Wang, W. Zhao, L. Zhang, Z. Fu, Q. Zhu, D. Yang, et al. (2025) DeepSeek-Prover-V2: advancing formal mathematical reasoning via reinforcement learning for subgoal decomposition. External Links: 2504.21801, Document, Link Cited by: §2. [56] L. Ruiz-Pérez and J. C. García-Escartín (2017) Quantum arithmetic with the quantum Fourier transform. Quantum Information Processing 16 (6), p. 152. External Links: Document Cited by: §1.3. [57] P. W. Shor (1994) Algorithms for quantum computation: discrete logarithms and factoring. In Proceedings of the 35th Annual Symposium on Foundations of Computer Science, p. 124–134. External Links: Document Cited by: §2.5. [58] D. R. Simon (1997) On the power of quantum computation. SIAM Journal on Computing 26 (5), p. 1474–1483. External Links: Document Cited by: §2.5. [59] 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) Real-time quantum error correction beyond break-even. Nature 616 (7955), p. 50–55. External Links: Document Cited by: Proving olympiad geometry theorems on a superconducting quantum processor. [60] D. Stahlke (2014) Quantum interference as a resource for quantum speedup. Physical Review A 90 (2), p. 022302. External Links: Document Cited by: §2.5. [61] Z. Sun, Q. Ye, and D. Deng (2026) Quantum automated theorem proving. External Links: 2601.07953, Document, Link Cited by: Abstract, §1.3, §1.3, §1, §1, §2.3, §2.3, §2.3, §2.3, §2.4, §2.4, §2, Proving olympiad geometry theorems on a superconducting quantum processor, Proving olympiad geometry theorems on a superconducting quantum processor, Proving olympiad geometry theorems on a superconducting quantum processor, Proving olympiad geometry theorems on a superconducting quantum processor, Proving olympiad geometry theorems on a superconducting quantum processor, Proving olympiad geometry theorems on a superconducting quantum processor. [62] T. H. Trinh, Y. Wu, Q. V. Le, H. He, and T. Luong (2024) Solving olympiad geometry without human demonstrations. Nature 625 (7995), p. 476–482. External Links: Document Cited by: Abstract, Proving olympiad geometry theorems on a superconducting quantum processor. [63] K. Wang, Z. Lu, C. Zhang, G. Liu, J. Chen, Y. Wang, Y. Wu, S. Xu, X. Zhu, F. Jin, et al. (2026) Demonstration of low-overhead quantum error correction codes. Nature Physics 22 (2), p. 308–314. External Links: Document Cited by: Proving olympiad geometry theorems on a superconducting quantum processor. [64] W. Wu (1978) On the decision problem and the mechanization of theorem-proving in elementary geometry. Scientia Sinica 21 (2), p. 159–172. Cited by: §1.1, §1, §1, Proving olympiad geometry theorems on a superconducting quantum processor. [65] Y. Wu, W. Bao, S. Cao, F. Chen, M. Chen, X. Chen, T. Chung, H. Deng, Y. Du, D. Fan, et al. (2021) Strong quantum computational advantage using a superconducting quantum processor. Physical Review Letters 127 (18), p. 180501. External Links: Document Cited by: Abstract, Proving olympiad geometry theorems on a superconducting quantum processor. [66] S. Xu, Z. Sun, K. Wang, H. Li, Z. Zhu, H. Dong, J. Deng, X. Zhang, J. Chen, Y. Wu, et al. (2024) Non-Abelian braiding of Fibonacci anyons with a superconducting processor. Nature Physics 20 (9), p. 1469–1475. External Links: Document Cited by: Proving olympiad geometry theorems on a superconducting quantum processor. [67] T. J. Yoder, G. H. Low, and I. L. Chuang (2014) Fixed-point quantum search with an optimal number of queries. Physical Review Letters 113 (21), p. 210501. External Links: Document Cited by: §1. [68] C. Zhang, J. Song, S. Li, Y. Liang, Y. Ma, W. Wang, Y. Zhu, and S. Zhu (2026) Proposing and solving olympiad geometry with guided tree search. Nature Machine Intelligence 8 (1), p. 84–95. External Links: Document Cited by: §2, Proving olympiad geometry theorems on a superconducting quantum processor. [69] H. Zhong, H. Wang, Y. Deng, M. Chen, L. Peng, Y. Luo, J. Qin, D. Wu, X. Ding, Y. Hu, et al. (2020) Quantum computational advantage using photons. Science 370 (6523), p. 1460–1463. External Links: Document Cited by: Abstract, Proving olympiad geometry theorems on a superconducting quantum processor.