# Proving olympiad geometry theorems on a superconducting quantum processor

arXiv: https://arxiv.org/abs/2609.14533 · HTML: https://mlsanity.com/paper/2609.14533/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 14 of its 71 references that are in the map.
- First posted on arXiv 13 Sep 2026.

## Builds on (most cited first, 14 of 14)

- [DeepSeek-R1: Incentivizing Reasoning Capability in LLMs via Reinforcement Learning](https://mlsanity.com/paper/2501.12948/) (2025)
- [Supervised learning with quantum enhanced feature spaces](https://mlsanity.com/paper/1804.11326/) (2018)
- [DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition](https://mlsanity.com/paper/2504.21801/) (2025)
- [A rigorous and robust quantum speed-up in supervised machine learning](https://mlsanity.com/paper/2010.02174/) (2020)
- [Challenges and Opportunities in Quantum Machine Learning](https://mlsanity.com/paper/2303.09491/) (2023)
- [Quantum advantage in learning from experiments](https://mlsanity.com/paper/2112.00778/) (2021)
- [Quantum machine learning beyond kernel methods](https://mlsanity.com/paper/2110.13162/) (2021)
- [DeepMath - Deep Sequence Models for Premise Selection](https://mlsanity.com/paper/1606.04442/) (2016)
- [Quantum-enhanced machine learning](https://mlsanity.com/paper/1610.08251/) (2016)
- [Evaluating Language Models for Mathematics through Interactions](https://mlsanity.com/paper/2306.01694/) (2023)
- [Reinforcement Learning of Theorem Proving](https://mlsanity.com/paper/1805.07563/) (2018)
- [Experimental quantum adversarial learning with programmable superconducting qubits](https://mlsanity.com/paper/2204.01738/) (2022)
- [Proposing and solving olympiad geometry with guided tree search](https://mlsanity.com/paper/2412.10673/) (2024)
- [Quantum automated theorem proving](https://mlsanity.com/paper/2601.07953/) (2026)

## Abstract (arXiv)

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.