A research team from Zhejiang University, Tsinghua University and other institutions has run geometric proof procedures on a superconducting quantum processor. The targets were the theorem that the diagonals of a square are perpendicular, and a problem from the 1978 International Mathematical Olympiad (IMO). A preprint published on September 13, 2026 reports an experiment that runs automated theorem proving, long studied on conventional computers, on quantum circuits. It does not present a new mathematical truth or a speed record. Instead, it asks which proof operations quantum hardware can actually carry out.
Proving known geometry problems on a quantum circuit
The team, including Ning Wang and Zheng-Zhi Sun, used a superconducting processor with 121 qubits. The work is posted as arXiv:2609.14533, and as of now it has not been confirmed as a peer-reviewed paper. The experiments were also limited to two geometry problems of different character.
The span from 1978 to 2026 is 48 years, but the IMO problem used here was not an unsolved problem for 48 years. What the researchers tested was whether the proof steps leading to a known conclusion could be built into a quantum circuit, and whether real hardware could carry the reasoning forward.
In automated theorem proving, a conclusion is derived from premises and permitted rules rather than from a judgment that a figure "looks right." In geometry, facts such as equal sides or perpendicular lines are treated as relationships between formulas and symbols. When intermediate expressions become complicated and the number of candidate inferences grows, the required time and memory balloon.
The team therefore implemented two different routes. For the square, they used Wu's method, which converts a figure into polynomials. For the IMO problem, they tried a proof search that chains together angle relationships. The former simplifies expressions in a fixed order; the latter chooses which prepared rule to apply next.
Turning the square proof into polynomial computation
In the square experiment, the vertex coordinates were expressed as variables, and the parallel and perpendicular relationships and equal lengths of the sides were converted into four polynomials. The conclusion to be proved, that the diagonals are perpendicular, can also be written as a polynomial equal to zero. The geometric proof then becomes a computation: can the conclusion polynomial be eliminated using the premise polynomials?
The core operation is pseudo-division. It removes the highest-degree term of a polynomial by combining multiplication and subtraction, shrinking the expression without dividing by coefficients as in ordinary division. In this experiment, the team went through four steps and confirmed that the final remainder polynomial was zero. Under the conditions the method requires, such as the figure not being degenerate, the conclusion follows.
What was loaded onto the quantum circuit was not the text of the formulas themselves. For the polynomials representing the coefficients, values were prepared at enough points to determine each polynomial's form uniquely, and these were encoded into groups of qubits. With this representation, polynomial operations can be replaced by multiplication and subtraction of values at each point.
However, the values at those points were computed beforehand on a conventional computer and embedded in the quantum circuit. The quantum processor performed the arithmetic of pseudo-division using those values. The values at each point were read from the measured distributions, the intermediate polynomial was reconstructed, and the process moved on to the next step.
The "zero" here means something different from drawing several squares and observing that the angles come out right. The points chosen to determine the polynomials and the algebraic elimination procedure are what support the proof. At the same time, the device's output is a noisy measurement result, so the validity of the idealized algebraic operations and how accurately the device executed them must be evaluated separately.
Chaining angle relationships in the IMO problem
Problem 4 of the 1978 IMO concerns an isosceles triangle and circles. Take an isosceles triangle ABC, and consider a circle tangent to the equal sides AB and AC at F and G respectively, and internally tangent to the triangle's circumcircle. The task is to show that the midpoint H of segment FG is the incenter of triangle ABC, the center of the triangle's inscribed circle.
In the configuration treated in the paper, symmetry places H on the line bisecting the angle at vertex A. What remains is to show that the line through H also bisects the angle at vertex B. The team expressed this condition using directed angles, measured from one line to another. In this representation, rotating a line's direction by a half turn is treated as the same thing.
The quantum circuit combines a strategy circuit that proposes the next operation with an inference circuit that carries out a fixed transformation. An evaluation circuit then checks whether the applied operation changed the state. Using those measurement results, the classical side adjusts the strategy circuit's parameters. Because the permitted rules are fixed, the setup does not bring in arbitrary logic during the search.
The three angle equalities used in the experiment were derived classically from the premises in advance and built directly into the inference circuit. The quantum circuit ran three rounds of selecting and applying them, reaching the target equality. It did not read the problem statement and discover auxiliary lines or proof rules on its own.
Figure 3 of the paper shows distributions obtained by repeating 1,000 measurements ten times each. In each round, the expected operation and output appeared most strongly, and the chain of the proof was reconstructed from those results. After the output was measured, a representative result was re-prepared as the next input. This is distinct from an experiment that preserves a quantum state through multiple stages.
How the work was divided between quantum and classical computing
Both experiments involved preparation by classical computing. What the quantum circuit handled was polynomial arithmetic in the square case, and the selection and application of prepared relations in the IMO case.
Laying out the paper's sections on algebraic proof and symbolic proof search, along with the implementation conditions in its conclusion (September 13, 2026 version), step by step gives the following comparison.
| Step | Square diagonals | IMO geometry problem |
|---|---|---|
| Prepared in advance | Values at points representing the polynomials, computed classically | Three angle equalities derived from the premises, built into the circuit |
| Run by the quantum circuit | Multiplication and subtraction needed for pseudo-division | Proposing the next operation, applying relations, evaluating changes |
| Handoff between stages | Intermediate polynomial reconstructed from measurement results | Output measured, next input state re-prepared |
| Result reached | Final polynomial becomes zero after four elimination steps | Angle relationships chained in three rounds, showing the incenter condition |
Source: experimental description and conclusions of the main paper. This table compares how processing was divided within the same study; it does not indicate a ranking of the two approaches in speed or capability.
The table shows a design in which the quantum circuit handles concrete reasoning operations while classical processing remains for input preparation and for connecting the stages. The value of the study lies in putting both algebraic transformation and symbolic selection onto real hardware within this division of labor. It is not yet comparable to a general-purpose system that assembles entire proofs autonomously.
The scale of the device also needs careful reading. The 121 qubits is the total for the processor. According to Figure S11 in the supplementary material, each circuit used between 17 and 32 qubits, so the full set of qubits was not devoted to a single proof. Even the first square circuit described in the main text uses 21 qubits. The number of qubits on a device alone does not indicate how complex a proof it can handle.
Verifying quantum advantage is still ahead
In an earlier study in January 2026, Sun and colleagues proposed a theoretical framework for quantum automated theorem proving. One advantage they presented was a quadratic improvement in "query complexity." This concerns how the number of queries needed can be reduced as problems grow, and it does not mean the device's processing time is simply halved.
The new experimental paper also states that it has not yet demonstrated the theoretical advantage for the quantum implementation of Wu's method. Circuit size and depth are limited by hardware errors. In addition, a realistic assessment of practical speed would need to include precomputation, circuit preparation and repeated measurements. The fact that a quantum state can hold many candidates does not by itself support the conclusion that the whole proof process is faster.
Classical computing has already advanced automated geometry proving in a different direction. AlphaGeometry, reported in a 2024 Nature paper, combined a language model's proposals of auxiliary constructions with symbolic reasoning and solved 25 of 30 olympiad geometry benchmark problems. Because the scope of problems and the purpose of evaluation differ from the two examples here, placing those numbers side by side cannot decide a contest between the quantum and classical approaches. The question being asked is less whether the quantum approach beat existing AI than how far an experiment moving proof processing onto quantum computation can be made to work.
The authors look ahead to handling larger knowledge bases and richer sets of rules, and to passing intermediate quantum states directly into the next inference step. Achieving that will require larger circuits with fewer errors. The paper says data and analysis and numerical simulation code will be released on Zenodo at publication, and independent verification of reproducibility will be another factor in judging the work.
The open question is whether the field can move from running known proofs on quantum circuits to showing an advantage in proof searches with many candidates. If comparisons under matched conditions, including preprocessing and measurement, and the preservation of quantum states across stages can be achieved, it will become possible to identify concretely where quantum computing could help with mathematical reasoning.