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

quant-phSep 13, 2026

Proving olympiad geometry theorems on a superconducting quantum processor

Authors: Ning Wang, Zheng-Zhi Sun, Zhengyi Cui, Yiren Zou, Aosai Zhang, Fanhao Shen, Jiarun Zhong, Zehang Bao,

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

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.

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 $\mathcal{G}$ from a set of hypotheses $\mathcal{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 $H_{1}=0,H_{2}=0,\ldots,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 $A_{t}$ that transforms the proof state $\lvert S_{t}\rangle$ into a candidate output $\lvert S_{t+1}\rangle$ . 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 $\lvert S_{t+1}\rangle$ 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=(x_{1},0)$ , $C=(x_{3},x_{2})$ and $D=(x_{5},x_{4})$ . b , Polynomial formulation of the theorem. The geometric hypotheses $AB\perp AD$ , $AB\parallel CD$ , $AD\parallel BC$ and $AB=BC$ are represented by the polynomials $H_{1}(\bm{x}),\ldots,H_{4}(\bm{x})$ , and the conclusion $AC\perp BD$ by the polynomial $G(\bm{x})$ , where $\bm{x}=(x_{1},x_{2},\ldots,x_{5})$ . c , Algebraic proof by successive pseudo-division. The variables $x_{5}$ , $x_{4}$ , $x_{3}$ and $x_{2}$ are eliminated sequentially using $H_{1}$ , $H_{2}$ , $H_{3}$ and $H_{4}$ , respectively. The resulting pseudo-remainder chain terminates at $R_{4}(\bm{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 $|\mathbf{0}\rangle$ 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 $U_{s}$ for the subsequent second controlled $U_{Q}$ operation. Then we write four value registers by controlled unitary $U_{P}$ or $U_{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 $|x_{1}x_{2}x_{3}x_{4}\rangle$ ( $|x_{1}\rangle$ ). 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 $|\psi\rangle$ , and another five qubits encode the output proof state. The action register is initialized in $|0\rangle^{\otimes 2}$ , and the output register in $|0\rangle^{\otimes 5}$ . The input proof states are $|00111\rangle$ , $|00000\rangle$ and $|01001\rangle$ in rounds 1, 2 and 3, respectively. The left gray box shows the parameterized single-qubit gate sequence on $\theta_{j}$ and $\theta_{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 $\angle[HD,FD]$ , $\angle[FD,DB]$ and $-\angle[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	$Q^{A}_{1}Q^{A}_{2}$	00	$\angle[HD,FD]=\angle[FD,DB]$
		01	$\angle[HB,BA]=\angle[HD,FD]$
		10	$\angle[FD,DB]=-\angle[HB,CB]$
State	$Q^{S}_{1}$	0	$+$
	$Q^{S}_{1}$	1	$-$
	$Q^{S}_{2}Q^{S}_{3}$	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.

Panel of Table 7 — Table S1: Variables and polynomials used in the proof.

Panel of Table 8 — 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 $|S_{t}\rangle$ together with the quantum knowledge base $|\mathrm{KB}\rangle$ 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 $|S_{t+1}\rangle$ . 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

\left|\pm\angle[ZX,YW]\right\rangle

based on the rule equation

\angle[CB,CA]=-\angle[CB,BA]

. The circuit first compares the input state

\left|\pm\angle[ZX,YW]\right\rangle

with the premise of the rule equation. If the comparison yields the state

\left|{{\rm{same}}}\right\rangle

, namely

[ZX,YW]=[CB,CA]

, the circuit

U_{W}

outputs the conclusion

\left|\mp\angle[CB,BA]\right\rangle

; otherwise, it leaves the input state unchanged. b , Circuit for comparing two

n

-qubit registers

\left|x\right\rangle

and

\left|y\right\rangle

. In this illustration, each register contains two qubits. The circuit compares the two registers qubit by qubit. The CX gates between corresponding qubits of

\left|x\right\rangle

and

\left|y\right\rangle

map each qubit in the

\left|y\right\rangle

\left|0\right\rangle

when the corresponding qubits are the same and to

\left|1\right\rangle

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(\log_{2}n)

using

O(n)

auxiliary qubits, or directly using

O(n)

CX gates [ 4 ] . The ancillary output is

\left|1\right\rangle

when the two registers are the same and

\left|0\right\rangle

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 $A_{t}$ , the next five qubits represent the proof state $S_{t+1}$ at reasoning round $t+1$ , and the final five qubits represent the proof state $S_{t}$ at reasoning round $t$ . The CNOT gates first copy the computational-basis encoding of $S_{t}$ to the $S_{t+1}$ register, so that the state is preserved when no effective action is applied. Then the action-controlled unitary $U_{A}$ is performed on $A_{t}$ and $S_{t+1}$ . b , Decomposition of $U_{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.

Figure S9: The quantum circuit to measure $P_{1}$ 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\left|{00110}\right\rangle\otimes\left|{00110}\right\rangle-4/5\left|{00010}\right\rangle\otimes\left|{10100}\right\rangle$ , which represents the superposition of two reasoning processes: one in which the formula “00110”( $+\angle[HB,BC]$ ) remains unchanged, and another in which the formula “10100”( $-\angle[HB,FD]$ ) is derived from “00010” ( $+\angle[HD,BC]$ ). After this circuit, the state evolves to $3/5\left|{00000}\right\rangle\otimes\left|{00110}\right\rangle-4/5\left|{10110}\right\rangle\otimes\left|{10100}\right\rangle$ . The $\left|{00000}\right\rangle$ on the first five qubits indicates that the corresponding proof-state component is unchanged. Sampling the measurement outcomes yields $P_{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.

Figure S10: Variational circuit used to determine the action register $A_{t}$ at reasoning round $t$ . In the encoding of the proof state $S_{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 $S_{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.

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

T_{1}

(blue line) and spin echo dephasing time

T_{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

CP

gates (brown line). Panels in the fourth column: Readout errors of state

|0\rangle

(orange line) and

|1\rangle

(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,

\beta

\text{arccos}\ \frac{1}{3}

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

Q_{2}

and

Q_{3}

for the third

CP

gate. e , A decomposition of SWAP gate.

Figure S16: Equivalent circuit illustrating the Pauli Twirling.

P_{i}\ (i=1,2,3,4)

is a Pauli gate chosen to leave the

CP(\pi)

gate invariant. For example,

P_{1}

P_{3}

Y

P_{2}

I

P_{4}

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 $|x_{1}x_{2}x_{3}\rangle$ . In this step, $x_{1},x_{3}\in\{0,1\}$ and $x_{2}\in\{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 $|x_{1}x_{2}\rangle$ . In this step, $x_{1}$ , $x_{2}\in\{00,01,11\}$ . Colors indicate the probability obtained from 2940 runs of measurements, with each run taking 3000 shots.

Automated Theorem Proving

Automated theorem proving develops algorithms and AI systems that construct or check formal proofs in mathematics, logic, and software.

See all 160 papers

A Machine-Verified Proof of a Quantum-Optimization Conjecture
Jun 29, 2026Uri Kol, Maor Ben-Shahar, Kfir Sulimany +1Large Language Model-Guided Theorem Proving Quantum Approximate Optimization Algorithm
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
QED-Nano: Teaching a Tiny Model to Prove Hard Theorems
Apr 6, 2026LM-Provers, Yuxiao Qu, Amrith Setlur +6Mathematical Reasoning LLM Mathematical Reasoning
CMU · Hugging Face · ETH Zurich +1
SCALAR: A Neurosymbolic Framework for Automated Conjecture and Reasoning in Quantum Circuit Analysis
May 11, 2026Sean Feeney, Pooja Rao, Andreas Klappenecker +5AI-Assisted Scientific Research Neuro-Symbolic Reasoning
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

Jun 29, 2026J/K move · Enter open · S save

A Machine-Verified Proof of a Quantum-Optimization Conjecture

Uri Kol, Maor Ben-Shahar, Kfir Sulimany, Dirk Englund

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

Large Language Model-Guided Theorem Proving Quantum Approximate Optimization Algorithm

Open paper AskPDF arXiv

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.

Abstract

Automated Theorem Proving

Explore similar work

A Machine-Verified Proof of a Quantum-Optimization Conjecture

QED-Nano: Teaching a Tiny Model to Prove Hard Theorems

SCALAR: A Neurosymbolic Framework for Automated Conjecture and Reasoning in Quantum Circuit Analysis