# Quantum automated theorem proving

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

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 11 of its 81 references that are in the map.
- First posted on arXiv 12 Jan 2026.

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

- [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)
- [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)
- [Quantum-enhanced machine learning](https://mlsanity.com/paper/1610.08251/) (2016)
- [A formal proof of the Kepler conjecture](https://mlsanity.com/paper/1501.02155/) (2015)
- [Experimental quantum adversarial learning with programmable superconducting qubits](https://mlsanity.com/paper/2204.01738/) (2022)
- [Wu's Method can Boost Symbolic AI to Rival Silver Medalists and AlphaGeometry to Outperform Gold Medalists at IMO Geometry](https://mlsanity.com/paper/2404.06405/) (2024)
- [Efficient Floating Point Arithmetic for Quantum Computers](https://mlsanity.com/paper/2112.10537/) (2021)

## Built on by (most cited first, 1 of 1)

- [Proving olympiad geometry theorems on a superconducting quantum processor](https://mlsanity.com/paper/2609.14533/) (2026)

## Abstract (arXiv)

Automated theorem proving, or more broadly automated reasoning, aims at using computer programs to automatically prove or disprove mathematical theorems and logical statements. It takes on an essential role across a vast array of applications and the quest for enhanced theorem-proving capabilities remains a prominent pursuit in artificial intelligence. Here, we propose a generic framework for quantum automated theorem proving, where the intrinsic quantum superposition and entanglement features would lead to potential advantages. In particular, we introduce quantum representations of knowledge bases and propose corresponding reasoning algorithms for a variety of tasks. We show how automated reasoning can be achieved with quantum resolution in both propositional and first-order logic with quadratically reduced query complexity. In addition, we propose the quantum algebraic proving method for geometric theorems, extending Wu's algebraic approach beyond the classical setting. Through concrete examples, including geometry problems from the International Mathematical Olympiad, we demonstrate how a quantum computer may prove geometric theorems with quadratic better query complexity. Our results establish a primary approach towards building quantum automatic theorem provers, which would be crucial for practical applications of both near-term and future quantum technologies.