Proving olympiad geometry theorems on a superconducting quantum processor
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.
Related
- Observation and Modulation of the Quantum Mpemba Effect on a Superconducting Quantum Processor
- Entangled logical qubits on a superconducting quantum processor
- Cryogenic Multiplexing Control Chip for Superconducting Quantum Processor
- Data and code for collision-model Dicke-state preparation: depth-fidelity frontiers, circuit costs, and superconducting-processor measurements
- Preparation of a Laughlin-like fractional Chern insulator on a superconducting quantum processor
BibTeX
@misc{wang2026proving,
title = {{Proving olympiad geometry theorems on a superconducting quantum processor}},
author = {Ning Wang and Zheng-Zhi Sun and Zhengyi Cui and Yiren Zou and Aosai Zhang and Fanhao Shen and Jiarun Zhong and Zehang Bao and Zitian Zhu and Han Wang and Jia-Nan Yang and Jiayuan Shen and Gongyu Liu and Yanzhe Wang and Yihang Han and Yiyang He and Jiahua Huang and Sailang Zhou and Xinrong Zhang and Yaozu Wu and Zixuan Song and Jinfeng Deng and Hang Dong and Qi Ye and Weikang Li and Si Jiang and Yixuan Ma and Shuangyue Geng and Zhide Lu and Chao Song and Hekang Li and Pengfei Zhang and Qiujiang Guo and H. Wang and Dong-Ling Deng},
howpublished = {arXiv},
year = {2026},
month = sep,
doi = {10.48550/arxiv.2609.14533},
eprint = {2609.14533},
archivePrefix = {arXiv},
url = {https://arxiv.org/abs/2609.14533},
}
RIS
TY - UNPB
TI - Proving olympiad geometry theorems on a superconducting quantum processor
AU - Ning Wang
AU - Zheng-Zhi Sun
AU - Zhengyi Cui
AU - Yiren Zou
AU - Aosai Zhang
AU - Fanhao Shen
AU - Jiarun Zhong
AU - Zehang Bao
AU - Zitian Zhu
AU - Han Wang
AU - Jia-Nan Yang
AU - Jiayuan Shen
AU - Gongyu Liu
AU - Yanzhe Wang
AU - Yihang Han
AU - Yiyang He
AU - Jiahua Huang
AU - Sailang Zhou
AU - Xinrong Zhang
AU - Yaozu Wu
AU - Zixuan Song
AU - Jinfeng Deng
AU - Hang Dong
AU - Qi Ye
AU - Weikang Li
AU - Si Jiang
AU - Yixuan Ma
AU - Shuangyue Geng
AU - Zhide Lu
AU - Chao Song
AU - Hekang Li
AU - Pengfei Zhang
AU - Qiujiang Guo
AU - H. Wang
AU - Dong-Ling Deng
PY - 2026
DA - 2026/09/13
PB - arXiv
DO - 10.48550/arxiv.2609.14533
UR - https://arxiv.org/abs/2609.14533
AB - 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.
ER -