Organizations: School of Physics, ZJU-Hangzhou Global Scientific and Technological Innovation Center, and Zhejiang Key Laboratory of Micro-nano Quantum Chips and Quantum Control, Zhejiang University, Hangzhou, China · Center for Quantum Information, IIIS, Tsinghua University, Beijing 100084, China · Shanghai Qi Zhi Institute, Shanghai 200232, China · Hefei National Laboratory, Hefei 230088, China
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.
Figures & tables
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=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 At that transforms the proof state ∣St⟩ into a candidate output ∣St+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⟩ is used in the next reasoning round (see Supplementary Information Sec.2 for an in-depth discussion).
Fig. 2: Demonstration of quantum algebraic theorem proving with a square geometry problem . a , Coordinate representation of the square ABCD , with A=(0,0) , B=(x1,0) , C=(x3,x2) and D=(x5,x4) . b , Polynomial formulation of the theorem. The geometric hypotheses AB⊥AD , AB∥CD , AD∥BC and AB=BC are represented by the polynomials H1(x),…,H4(x) , and the conclusion AC⊥BD by the polynomial G(x) , where x=(x1,x2,…,x5) . c , Algebraic proof by successive pseudo-division. The variables x5 , x4 , x3 and x2 are eliminated sequentially using H1 , H2 , H3 and H4 , respectively. The resulting pseudo-remainder chain terminates at R4(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 Us for the subsequent second controlled UQ operation. Then we write four value registers by controlled unitary UP or UQ 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⟩ ( ∣x1⟩ ). 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.
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 , and the output register in ∣0⟩⊗5 . The input proof states are ∣00111⟩ , ∣00000⟩ and ∣01001⟩ in rounds 1, 2 and 3, respectively. The left gray box shows the parameterized single-qubit gate sequence on θj and θ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.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] , ∠[FD,DB] and −∠[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.
Name
Qubits
Value
Information
Action
Q1AQ2A
00
∠[HD,FD]=∠[FD,DB]
01
∠[HB,BA]=∠[HD,FD]
10
∠[FD,DB]=−∠[HB,CB]
State
Q1S
0
+
1
−
Q2SQ3S
00
HD
Table 1: Basis encoding of the action and state registers.
Appendix figures & tables19 assets
Supplementary material from the paper’s appendix.
Appendix
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.
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.
Table S1: Variables and polynomials used in the proof.
Table S2: The values of each variable in different reasoning steps.
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.
Figure S5: General quantum architecture for proof search. At reasoning round t , the current proof state ∣St⟩ together with the quantum knowledge base ∣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⟩ . 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.
Figure S6: Schematic illustration of the IMO 1978 geometry problem.
Figure S7: Quantum circuit implementing rule R9 . a , Reasoning circuit for the input state ∣±∠[ZX,YW]⟩ based on the rule equation ∠[CB,CA]=−∠[CB,BA] . The circuit first compares the input state ∣±∠[ZX,YW]⟩ with the premise of the rule equation. If the comparison yields the state ∣same⟩ , namely [ZX,YW]=[CB,CA] , the circuit UW outputs the conclusion ∣∓∠[CB,BA]⟩ ; otherwise, it leaves the input state unchanged. b , Circuit for comparing two n -qubit registers ∣x⟩ and ∣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⟩ and ∣y⟩ map each qubit in the ∣y⟩ register to ∣0⟩ when the corresponding qubits are the same and to ∣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 2n CX gates arranged in two parallel layers, 2n single-qubit X gates, and one n -controlled NOT gate. The latter can be implemented either with depth O(log2n) using O(n) auxiliary qubits, or directly using O(n) CX gates [ 4 ] . The ancillary output is ∣1⟩ when the two registers are the same and ∣0⟩ when they are different.
Figure S8: Quantum reasoning circuit for IMO example. a , Overall structure of the 12-qubit circuit. The first two qubits encode the action At , the next five qubits represent the proof state St+1 at reasoning round t+1 , and the final five qubits represent the proof state St at reasoning round t . The CNOT gates first copy the computational-basis encoding of St to the St+1 register, so that the state is preserved when no effective action is applied. Then the action-controlled unitary UA is performed on At and St+1 . b , Decomposition of UA 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.
Figure S9: The quantum circuit to measure P1 in Eq. ( S24 ). This circuit coherently compares the formulas at steps t and t+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⟩ , which represents the superposition of two reasoning processes: one in which the formula “00110”( +∠[HB,BC] ) remains unchanged, and another in which the formula “10100”( −∠[HB,FD] ) is derived from “00010” ( +∠[HD,BC] ). After this circuit, the state evolves to 3/5∣00000⟩⊗∣00110⟩−4/5∣10110⟩⊗∣10100⟩ . The ∣00000⟩ on the first five qubits indicates that the corresponding proof-state component is unchanged. Sampling the measurement outcomes yields P1=9/25 . By optimizing the action circuit to reduce this probability, the fraction of reasoning actions that produce no new formulas can be suppressed.
Figure S10: Variational circuit used to determine the action register At at reasoning round t . In the encoding of the proof state St , 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 St , 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.
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 T1 (blue line) and spin echo dephasing time T2SE (red line). Panels in the third column: Pauli errors of simultaneous single-qubit gates (purple line) and cycle Pauli errors of two-qubit CP gates (brown line). Panels in the fourth column: Readout errors of state ∣0⟩ (orange line) and ∣1⟩ (green line). Vertical dashed lines indicate the median values.
Figure S12: Patterns of parallel CP 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 CP gates. There are three types of CP 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.
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, β = arccos31 .
Figure S14: The original (a) and optimized (b) implementations of the CCX and CCCX gates. It should be noted that the decomposition of CCX and CCCX gates into sequences of U and CX gates is not unique. However, the minimal number of required CX gates is the same. For notational simplicity, we ignore the parameters of different U gates.
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 Q2 and Q3 for the third CP gate. e , A decomposition of SWAP gate.
Figure S16: Equivalent circuit illustrating the Pauli Twirling. Pi(i=1,2,3,4) is a Pauli gate chosen to leave the CP(π) gate invariant. For example, P1 = P3 = Y , P2 = I , P4 = Z .
Figure S17: The experimental quantum circuit of step 4 executed in the algebraic theorem proving.
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⟩ . In this step, x1,x3∈{0,1} and x2∈{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⟩ . In this step, x1 , x2∈{00,01,11} . Colors indicate the probability obtained from 2940 runs of measurements, with each run taking 3000 shots.
We report a machine-verified resolution of a problem open for over a decade in quantum optimization: the Farhi, Goldstone and Gutmann (FGG) conjecture that depth-p Quantum Approximate Optimization Algorithm (QAOA) on the ring of disagrees attains approximation ratio (2p+1)/(2p+2) exactly. We found the proof using a large language model, Claude Fable 5, and verified its correctness end-to-end by the Lean 4 proof assistant. Our methodology includes several ingredients: building on a substantial Lean library of quantum information, we formalized the QAOA components and the known parts of the problem, and reduced the conjecture to a single open mathematical statement. The model was then handed the library and our agentic toolkit, and tasked with closing that gap by constructing a proof in Lean. The resulting process is a feedback loop between the model's natural-language reasoning and Lean's mechanical verification, which converged to a machine-verified proof. Human verification is required only for the structural scaffolding - that the formal statement faithfully encodes the intended claim - while the proof itself is supplied by the model and certified mechanically by Lean. The proof is nevertheless striking - the model uncovered a hidden dynamical symmetry of the problem and exploited it, borrowing tools and machinery from an adjacent field to turn a hard existence problem into an explicit construction. This work paves the way for resolving open conjectures in quantum information science and beyond.
Uri Kol, Maor Ben-Shahar, Kfir Sulimany +1
Center of Mathematical Sciences and Applications, Harvard University, Cambridge, Massachusetts 02138, USA · MIT Center for Theoretical Physics - a Leinweber Institute, Cambridge, MA 02139, USA · Research Laboratory of Electronics, Massachusetts Institute of Technology, Cambridge, Massachusetts 02139, USA
Proprietary AI systems have recently demonstrated impressive capabilities on complex proof-based problems, with gold-level performance reported at the 2025 International Mathematical Olympiad (IMO). However, the training pipelines behind these systems remain largely undisclosed, and their reliance on large "internal" models and scaffolds makes them expensive to run, difficult to reproduce, and hard to study or improve upon. This raises a central question: can small, open models also be trained to achieve competitive reasoning performance on difficult Olympiad-level math? In this paper, we answer this question by building QED-Nano, a 4B model post-trained for Olympiad-level proofs. Our training recipe has three stages: (1) supervised fine-tuning to imbue good proof-writing styles by distilling from DeepSeek-Math-V2, (2) reinforcement learning (RL) with rubric-based rewards, and (3) expanding RL with a reasoning cache, which decomposes long proofs into iterative summarize-and-refine cycles and enables stronger test-time reasoning. QED-Nano surpasses the proof-generation performance of much larger open models, including Nomos-1 and GPT-OSS-120B, and approaches the performance of proprietary models like Gemini 3 Pro, at a fraction of the inference cost. To support further research on open mathematical reasoning, we release the full QED-Nano pipeline, including the QED-Nano and QED-Nano-SFT models, the FineProofs-SFT and FineProofs-RL datasets, and the training and evaluation code.
In this paper, we present SCALAR (Symbolic Conjecture and LLM-Assisted Reasoning), a neurosymbolic framework for automated conjecture generation in quantum circuit analysis built on top of the CUDA-Q open source framework. The system integrates quantum simulation, symbolic conjecture generation, and LLM-based interpretation. We evaluate SCALAR on 82 MaxCut instances from the MQLib benchmark dataset and extend the analysis to 2,000 randomly generated graphs across four topologies: regular, Erdos-Renyi, Barabasi-Albert, and Watts-Strogatz. The framework generates conjectured bounds relating optimal QAOA parameters to graph invariants, including known relationships such as periodicity constraints on the phase separation parameter γ. SCALAR also recovers previously reported parameter transfer phenomena across structurally similar instances. Additionally, the system identifies correlations between graph structural features and optimization landscape properties, which we characterize through invariant-based descriptors. Using CUDA-Q tensor network simulator, we scale experiments to instances of up to 77 qubits. We discuss the accuracy, generality, and limitations of the generated conjectures, including sensitivity to graph class and quantum circuit depth.
Sean Feeney, Pooja Rao, Andreas Klappenecker +5
Department of Computer Science, Texas A&M University, College Station, USA · NVIDIA Corporation, Santa Clara, USA · Computing and Artificial Intelligence Division (CAI-3), Los Alamos National Laboratory, Los Alamos, USA