Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Log inSign up
Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Blog
Job Board
Q3AS

© 2026 Aqora Quantum S.A.S.

TermsPrivacyLegal Notice

Cambridge University Press eBooks

Quantomatic

Bob Coecke, Aleks Kissinger

Published Mar 16, 2017• 0 citations
Publisher

Abstract

We will encourage you to develop the three great virtues of a programmer: laziness, impatience, and hubris. – Larry Wall, Programming Perl, 1st edition So there you have it. Hundreds of pages and more than 3000 diagrams later, we've told you (pretty much) everything we know about quantum theory and diagrammatic reasoning. So, where to now? Is it time for everyone to start covering blackboards and filling papers with diagrams? Of course! But even better, what if someone else did all the diagrammatic proving for you while you sit back, relax, and have a beer? That's even better! The fact that the diagrams we use are essentially made up of a finite number of ingredients (namely, spiders) means they are particularly well suited to automated reasoning . In this subfield of artificial intelligence, one develops software that allows a computer to do a whole range of things often associated with human mathematicians: from simply checking mathematical proofs for correctness to automatically searching for new proofs or even new and interesting conjectures to then try and prove automatically. In the past, automated reasoning has typically concerned traditional, formula-based mathematics built on formal logics and set-based algebraic structures, and there it has been very successful. It has provided us with tools called proof assistants , which allow us to automatically construct proofs of mind-bending results, such as Gödel's incompleteness theorems, and rigorously check proofs that are way too big for a human mathematician to get totally correct, like Kepler's conjecture, the four-colour theorem, and the Feit– Thompson theorem (famously massive proofs in geometry, graph theory, and group theory, respectively). In addition to serving essentially as ‘robot teaching assistants’, which tirelessly check the work of human mathematicians, techniques from automated reasoning can actually tell us something new, via conjecture synthesis . Much as a human mathematician would discover features and behaviours of an unfamiliar mathematical creature by ‘poking at it’ (i.e. making educated guesses about how it will behave and trying to prove them), there exist automated techniques that do this at high speed. When it succeeds in a proof, the result is a freshly minted theorem that no human has ever seen or even thought to ask about.

DOI
10.1017/9781316219317.015

Related papers

Diagrammatic Reasoning with Control as a Constructor, Applications to Quantum Circuits

Noé Delorme, Simon Perdrix

arXiv:2508.21756•Lecture notes in computer science•Jan 1, 2026•1 citation

Symbolic Specification and Reasoning for Quantum Data and Operations

Mingsheng Ying

In quantum information and computation research, symbolic methods have been widely used for human specification and reasoning about quantum states and operations. At the same time, they are essential for ensuring the scalability and efficiency of automated reasoning and verification tools for quantum algorithms and programs. However, a formal theory for symbolic specification and reasoning about quantum data and operations is still lacking, which significantly limits the practical applicability of automated verification techniques in quantum computing. In this paper, we present a general logical framework, called Symbolic Operator Logic $\mathbf{SOL}$, which enables symbolic specification and reasoning about quantum data and operations. Within this framework, a classical first-order logical language is embedded into a language of formal operators used to specify quantum data and operations, including their recursive definitions. This embedding allows reasoning about their properties modulo a chosen theory of the underlying classical data (e.g., Boolean algebra or group theory), thereby leveraging existing automated verification tools developed for classical computing. It should be emphasised that this embedding of classical first-order logic into $\mathbf{SOL}$ is precisely what makes the symbolic method possible. We envision that this framework can provide a conceptual foundation for the formal verification and automated theorem proving of quantum computation and information in proof assistants such as Lean, Coq, and related systems.

cs.PLCross-listedarXiv:2512.22383•Dec 30, 2025•0 citations

Synthesising Graphical Theories

Aleks Kissinger

In recent years, diagrammatic languages have been shown to be a powerful and expressive tool for reasoning about physical, logical, and semantic processes represented as morphisms in a monoidal category. In particular, categorical quantum mechanics, or "Quantum Picturalism", aims to turn concrete features of quantum theory into abstract structural properties, expressed in the form of diagrammatic identities. One way we search for these properties is to start with a concrete model (e.g. a set of linear maps or finite relations) and start composing generators into diagrams and looking for graphical identities. Naively, we could automate this procedure by enumerating all diagrams up to a given size and check for equalities, but this is intractable in practice because it produces far too many equations. Luckily, many of these identities are not primitive, but rather derivable from simpler ones. In 2010, Johansson, Dixon, and Bundy developed a technique called conjecture synthesis for automatically generating conjectured term equations to feed into an inductive theorem prover. In this extended abstract, we adapt this technique to diagrammatic theories, expressed as graph rewrite systems, and demonstrate its application by synthesising a graphical theory for studying entangled quantum states.

arXiv:1202.6079•EPiC series in computing•Jan 23, 2018•4 citations

Quantum automated theorem proving

Zheng-Zhi Sun, Qi Ye, Dong-Ling Deng

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.

quant-pharXiv:2601.07953•Jan 14, 2026•0 citations

Graphical reasoning in compact closed categories for quantum computation

Lucas Dixon, Ross Duncan

arXiv:0902.0514•Annals of Mathematics and Artificial Intelligence•May 1, 2009•43 citations

Machines, Logic and Quantum Physics

David Deutsch, ARTUR K. EKERT, Rossella Lupacchini

Though the truths of logic and pure mathematics are objective and independent of any contingent facts or laws of nature, our knowledge of these truths depends entirely on our knowledge of the laws of physics. Recent progress in the quantum theory of computation has provided practical instances of this, and forces us to abandon the classical view that computation, and hence mathematical proof, are purely logical notions independent of that of computation as a physical process. Henceforward, a proof must be regarded not as an abstract object or process but as a physical process, a species of computation, whose scope and reliability depend on our knowledge of the physics of the computer concerned.

arXiv:math/9911150•Nov 19, 1999•4 citations
We will encourage you to develop the three great virtues of a programmer: laziness, impatience, and hubris. – Larry Wall, Programming Perl, 1st edition So there you have it. Hundreds of pages and more than 3000 diagrams later, we've told you (pretty much) everything we know about quantum theory and diagrammatic reasoning. So, where to now? Is it time for everyone to start covering blackboards and filling papers with diagrams? Of course! But even better, what if someone else did all the diagrammatic proving for you while you sit back, relax, and have a beer? That's even better! The fact that the diagrams we use are essentially made up of a finite number of ingredients (namely, spiders) means they are particularly well suited to automated reasoning . In this subfield of artificial intelligence, one develops software that allows a computer to do a whole range of things often associated with human mathematicians: from simply checking mathematical proofs for correctness to automatically searching for new proofs or even new and interesting conjectures to then try and prove automatically. In the past, automated reasoning has typically concerned traditional, formula-based mathematics built on formal logics and set-based algebraic structures, and there it has been very successful. It has provided us with tools called proof assistants , which allow us to automatically construct proofs of mind-bending results, such as Gödel's incompleteness theorems, and rigorously check proofs that are way too big for a human mathematician to get totally correct, like Kepler's conjecture, the four-colour theorem, and the Feit– Thompson theorem (famously massive proofs in geometry, graph theory, and group theory, respectively). In addition to serving essentially as ‘robot teaching assistants’, which tirelessly check the work of human mathematicians, techniques from automated reasoning can actually tell us something new, via conjecture synthesis . Much as a human mathematician would discover features and behaviours of an unfamiliar mathematical creature by ‘poking at it’ (i.e. making educated guesses about how it will behave and trying to prove them), there exist automated techniques that do this at high speed. When it succeeds in a proof, the result is a freshly minted theorem that no human has ever seen or even thought to ask about.
In quantum information and computation research, symbolic methods have been widely used for human specification and reasoning about quantum states and operations. At the same time, they are essential for ensuring the scalability and efficiency of automated reasoning and verification tools for quantum algorithms and programs. However, a formal theory for symbolic specification and reasoning about quantum data and operations is still lacking, which significantly limits the practical applicability of automated verification techniques in quantum computing. In this paper, we present a general logical framework, called Symbolic Operator Logic SOL\mathbf{SOL}SOL, which enables symbolic specification and reasoning about quantum data and operations. Within this framework, a classical first-order logical language is embedded into a language of formal operators used to specify quantum data and operations, including their recursive definitions. This embedding allows reasoning about their properties modulo a chosen theory of the underlying classical data (e.g., Boolean algebra or group theory), thereby leveraging existing automated verification tools developed for classical computing. It should be emphasised that this embedding of classical first-order logic into SOL\mathbf{SOL}SOL is precisely what makes the symbolic method possible. We envision that this framework can provide a conceptual foundation for the formal verification and automated theorem proving of quantum computation and information in proof assistants such as Lean, Coq, and related systems.
In recent years, diagrammatic languages have been shown to be a powerful and expressive tool for reasoning about physical, logical, and semantic processes represented as morphisms in a monoidal category. In particular, categorical quantum mechanics, or "Quantum Picturalism", aims to turn concrete features of quantum theory into abstract structural properties, expressed in the form of diagrammatic identities. One way we search for these properties is to start with a concrete model (e.g. a set of linear maps or finite relations) and start composing generators into diagrams and looking for graphical identities. Naively, we could automate this procedure by enumerating all diagrams up to a given size and check for equalities, but this is intractable in practice because it produces far too many equations. Luckily, many of these identities are not primitive, but rather derivable from simpler ones. In 2010, Johansson, Dixon, and Bundy developed a technique called conjecture synthesis for automatically generating conjectured term equations to feed into an inductive theorem prover. In this extended abstract, we adapt this technique to diagrammatic theories, expressed as graph rewrite systems, and demonstrate its application by synthesising a graphical theory for studying entangled quantum states.
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.
Though the truths of logic and pure mathematics are objective and independent of any contingent facts or laws of nature, our knowledge of these truths depends entirely on our knowledge of the laws of physics. Recent progress in the quantum theory of computation has provided practical instances of this, and forces us to abandon the classical view that computation, and hence mathematical proof, are purely logical notions independent of that of computation as a physical process. Henceforward, a proof must be regarded not as an abstract object or process but as a physical process, a species of computation, whose scope and reliability depend on our knowledge of the physics of the computer concerned.