{
  "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.",
  "abstract_shown": true,
  "affiliations": [],
  "article_type": null,
  "arxiv": "2609.14533",
  "author_total": 35,
  "authors": [
    {
      "name": "Ning Wang"
    },
    {
      "name": "Zheng-Zhi Sun"
    },
    {
      "name": "Zhengyi Cui"
    },
    {
      "name": "Yiren Zou"
    },
    {
      "name": "Aosai Zhang"
    },
    {
      "name": "Fanhao Shen"
    },
    {
      "name": "Jiarun Zhong"
    },
    {
      "name": "Zehang Bao"
    },
    {
      "name": "Zitian Zhu"
    },
    {
      "name": "Han Wang"
    },
    {
      "name": "Jia-Nan Yang"
    },
    {
      "name": "Jiayuan Shen"
    },
    {
      "name": "Gongyu Liu"
    },
    {
      "name": "Yanzhe Wang"
    },
    {
      "name": "Yihang Han"
    },
    {
      "name": "Yiyang He"
    },
    {
      "name": "Jiahua Huang"
    },
    {
      "name": "Sailang Zhou"
    },
    {
      "name": "Xinrong Zhang"
    },
    {
      "name": "Yaozu Wu"
    },
    {
      "name": "Zixuan Song"
    },
    {
      "name": "Jinfeng Deng"
    },
    {
      "name": "Hang Dong"
    },
    {
      "name": "Qi Ye"
    },
    {
      "name": "Weikang Li"
    },
    {
      "name": "Si Jiang"
    },
    {
      "name": "Yixuan Ma"
    },
    {
      "name": "Shuangyue Geng"
    },
    {
      "name": "Zhide Lu"
    },
    {
      "name": "Chao Song"
    },
    {
      "name": "Hekang Li"
    },
    {
      "name": "Pengfei Zhang"
    },
    {
      "name": "Qiujiang Guo"
    },
    {
      "name": "H. Wang"
    },
    {
      "name": "Dong-Ling Deng"
    }
  ],
  "bibtex": "https://research.draconitic.com/paper/eh8368vnxxpne.bib",
  "cited_by": 0,
  "doi": "10.48550/arxiv.2609.14533",
  "fulltext_url": null,
  "id": "eh8368vnxxpne",
  "issns": [],
  "landing_url": "https://arxiv.org/abs/2609.14533",
  "language": null,
  "licence": "LicenseRef-arXiv-nonexclusive-1.0",
  "licence_label": "arXiv licence",
  "licence_source": "article",
  "licence_url": "http://arxiv.org/licenses/nonexclusive-distrib/1.0/",
  "metadata_licence": "CC0-1.0",
  "native_subjects": [
    [
      "arxiv",
      "cs.AI"
    ],
    [
      "arxiv",
      "quant-ph"
    ]
  ],
  "openalex": null,
  "pdf_url": "https://arxiv.org/pdf/2609.14533",
  "pmcid": null,
  "pmid": null,
  "published": "2026-09-13",
  "publisher": null,
  "ris": "https://research.draconitic.com/paper/eh8368vnxxpne.ris",
  "sources": [
    {
      "first_seen": "2026-10-30T12:21:25Z",
      "native_id": "2609.14533",
      "source": "arxiv",
      "url": "https://arxiv.org/abs/2609.14533"
    }
  ],
  "subjects": [
    {
      "field": "physics",
      "origin": "arxiv:quant-ph",
      "subfield": "quantum"
    }
  ],
  "title": "Proving olympiad geometry theorems on a superconducting quantum processor",
  "title_text": "Proving olympiad geometry theorems on a superconducting quantum processor",
  "type": "preprint",
  "updated_at": "2026-10-30T12:21:25Z",
  "url": "https://research.draconitic.com/paper/eh8368vnxxpne",
  "venue": "arXiv",
  "versions": []
}