Proving olympiad geometry theorems on a superconducting quantum processor

AI summary

Overview

Research area: Quantum computing applied to automated theorem proving (symbolic reasoning), specifically geometry theorem proving on superconducting quantum hardware.

Technical level: Advanced — the paper assumes familiarity with quantum circuits, gate fidelities, polynomial algebra (Wu's method), and the full-angle formalism for geometry proofs.

Scope: An experimental demonstration that a 121-qubit superconducting processor can execute two complementary quantum proof procedures — an algebraic elimination method and a strategy-guided symbolic proof search — to prove a square-perpendicularity theorem and Problem 4 of the 1978 International Mathematical Olympiad (IMO).

What This Paper Is About

Automated theorem proving systems, including recent neuro-symbolic systems such as AlphaGeometry and TongGeometry, are ultimately limited by classical hardware: intermediate expressions and candidate inference steps can grow rapidly with problem complexity, imposing unattainable time and memory costs. The authors ask whether a programmable quantum processor can carry out structured formal deduction itself, rather than merely have its output checked classically. They build two quantum proving frameworks and run both on real superconducting hardware, using geometry as the testbed.

Key Contributions

1. First experimental realization of quantum automated theorem proving. The paper states that experimental demonstration of quantum automated theorem proving "remains a notable challenge and has not been reported so far," and reports its realization on a fully programmable superconducting processor.
2. A quantum implementation of Wu's algebraic elimination method. The pseudo-division procedure is mapped onto quantum circuits using a point-value representation, with multivariate polynomials held in superposition states and the conclusion certified by a vanishing final pseudo-remainder.
3. A hybrid quantum strategy-guided symbolic proof search. A parameterized strategy circuit proposes inference actions in superposition, a fixed reasoning circuit enforces formally valid transitions between proof states, and an evaluation circuit defines the training loss — yielding a human-readable proof in the full-angle formalism.
4. Two concrete hardware proofs. The perpendicularity of a square's diagonals is proved algebraically (four quantum pseudo-division steps), and 1978 IMO Problem 4 is proved symbolically (three proof-search rounds).

Main Findings

• Hardware platform: Experiments use a two-dimensional flip-chip superconducting processor with 121 frequency-tunable transmon qubits in an 11 × 11 square lattice, with nearest-neighbour interactions mediated by 220 tunable couplers. Simultaneous fidelities are better than 99.9% for single-qubit gates, 99% for two-qubit gates, and 98% for measurement.
• Algebraic proof completed: For square ABCD with A = (0,0), B = (x₁,0), C = (x₃,x₂), D = (x₅,x₄), the hypotheses AB ⟂ AD, AB ∥ CD, AD ∥ BC and AB = BC are encoded as H₁(x), …, H₄(x), and the conclusion AC ⟂ BD as G(x). Four quantum pseudo-division steps eliminate x₅, x₄, x₃ and x₂ sequentially, terminating at R₄(x) = 0.
• Step-1 circuit scale: The first pseudo-division step is implemented on 21 qubits in 77 layers, containing 150 single-qubit gates and 89 two-qubit gates, for P(x) = x₃x₅ + (x₂x₄ − x₁x₃)x₅⁰ divided by Q(x) = x₅.
• Intermediate remainder reproduced: Measurement of seven qubits (shown as 2⁷ coloured squares, from 3000 runs of 3000 shots each) yields the expected output polynomial R₁(x) = x₂x₄ − x₁x₃, with the exponent-one coefficient vanishing at all sampled points.
• Final remainder vanishes: In the last step, the dominant probability for each of the three exponent sectors and all three sampling points lies in the value state encoding zero, so all reconstructed coefficients vanish and R₄(x) = 0, completing the algebraic proof.
• No quantum advantage demonstrated here: Although a quantum implementation of Wu's method can in principle achieve a quadratic reduction in query complexity, the authors state that hardware imperfections limit accessible circuit size and depth and that this advantage has not yet been demonstrated.
• Symbolic proof of IMO 1978 Problem 4: Starting from ∠[HB,BA], three rounds select actions |01⟩, |00⟩, |10⟩ and produce outputs ∠[HD,FD], ∠[FD,DB] and −∠[HB,CB], reconstructing the intended chain and establishing ∠[HB,BA] + ∠[HB,CB] = 0.
• Training behaviour: The loss (defined as L = P₁ + P₂) decreases in each of the three rounds; training stops when the standard deviation of the four most recent loss values falls below 0.005. Error bars are the standard error of the mean over 10 repeated runs of 1,000 shots each.
• Small-scale encoding: The symbolic experiments use two action qubits, five input-state qubits and five output-state qubits; the strategy circuit has 16 trainable parameters implemented as R_x and R_z rotation angles, optimized with Adam and gradients from the parameter-shift rule.

Methodology in Plain English

The authors translate each geometry problem into exact formal objects — polynomial equations for the algebraic route, directed angle relations for the symbolic route — and store those objects in quantum registers.

For the algebraic route they use Wu's method, which proves a conclusion by repeatedly dividing the goal polynomial by hypothesis polynomials until the remainder vanishes. Instead of tracking symbolic expressions term by term, they encode polynomials in "point-value" form: for each power of the variable being eliminated, the coefficient is evaluated at a set of sampling points and written into a value register by a controlled unitary. Each pseudo-division is then just aligned exponent shifting plus quantum multiplication and subtraction of those stored values. In this implementation the point values are precomputed classically and embedded in the controlled unitaries; the arithmetic itself runs on the quantum processor. After each step the output is measured, the intermediate remainder identified, and the next step prepared.

For the symbolic route they encode the current proof state (a signed full-angle, stored as a sign qubit plus two two-qubit line indices) and a two-qubit action register. A trainable strategy circuit, with every action qubit coupled to all four line-index qubits, proposes inference actions; a fixed reasoning circuit copies the input state to an output register and applies the rule selected by the action, leaving the state unchanged if the rule does not apply. An evaluation circuit computes the bitwise difference between input and output states, and the loss penalizes trivial (unchanged) transitions and the unused action state |11⟩. The dominant measured output in each round becomes the input to the next, so three rounds produce the proof chain.

Why This Matters

The work moves quantum computing beyond predominantly numerical tasks into structured, verifiable symbolic reasoning, and provides experimental evidence that formal deduction can be executed as a quantum process rather than only verified classically after the fact. It also gives a hardware-grounded baseline for the theoretical framework of quantum automated theorem proving, including an honest statement that the predicted quadratic speedup has not yet been observed.

Potential application areas (as motivated by the paper's framing; not demonstrated here):

• Formal verification of hardware and software, which the paper identifies as a crucial tool relying on automated theorem proving.
• Mathematical discovery and education, where machine-generated, human-readable geometry proofs can be checked step by step.
• Neuro-symbolic AI systems such as AlphaGeometry and TongGeometry, which could in principle use quantum subroutines for the symbolic search component.
• Quantum symbolic intelligence more broadly, extending quantum machine learning from pattern recognition toward rule-based deduction.

Industry relevance: Relevant to quantum hardware vendors and cloud quantum computing providers seeking non-numeric workloads, to chip-design and software-verification groups that depend on formal methods, and to AI research organizations building reasoning systems.

Future Directions

• Demonstrating the predicted speedup: the authors state that showing the quadratic reduction in query complexity requires larger, deeper circuits, higher-fidelity hardware, and potentially fault-tolerant operations.
• Coherent multi-step reasoning: currently the proof state is measured and re-prepared between rounds; passing the output proof state directly to the next round would preserve superpositions of inference actions and proof paths across an entire derivation.
• Scaling knowledge bases and rule sets: larger hypothesis sets and richer inference rules could be incorporated by extending state registers and compiling additional inference operations into the reasoning circuit.
• Broadening beyond geometry: extending the framework from polynomial instances of limited size and a restricted set of symbolic relations to more general mathematical and logical domains.

Target Audience

Quantum computing experimentalists interested in non-arithmetic applications and circuit-level demonstrations; researchers in automated theorem proving and neuro-symbolic reasoning who want to know what current quantum hardware can and cannot do; and graduate students or advanced readers in quantum information, symbolic AI, or formal methods seeking a concrete case study connecting the two fields. The paper is not suitable as an introduction to either quantum circuits or geometry theorem proving.

Authors’ 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.