<p>The mathematician Andrew Granville recently published a
&quot;philosophical&quot; article, <a href="https://mxphi.com/wp-content/uploads/2023/07/Granville.pdf" rel="nofollow noreferrer">Accepted proofs: Objective truth, or culturally robust?</a>.</p>
<p>At the end, he mentions in passing a suggestion by Carlos Simpson that a
quantum computer might be able to prove theorems whose proofs are too long
to be checkable by a classical computer.  My first reaction was that this
was not possible, but as I thought about it more, I realized that I
couldn't rigorously rule it out.  Maybe I'm missing something?</p>
<p>One idea might be something like this.  Let's say that there's a proof of
the Riemann Hypothesis (in ZFC, say), but the shortest one is many orders
of magnitude larger than we can store on our computers.  Nevertheless, our computational power somehow allows us to write down a circuit <span class="math-container">$C$</span> which &quot;encodes&quot; the proof, in
the sense that the things <span class="math-container">$C$</span> accepts are precisely the Boolean clauses of a
Boolean instance which is satisfiable if and only if the desired proof of
the Riemann Hypothesis exists.</p>
<p>Now, the problem of testing whether the Boolean instance encoded by <span class="math-container">$C$</span> is satisfiable is
in <span class="math-container">$\mathsf{NEXP}$</span>.  So my main question is, has the possibility that <span class="math-container">$\mathsf{BQP} = \mathsf{NEXP}$</span> been rigorously ruled out?</p>
<p>If not, then it seems that in principle, we could have a situation in which a quantum computer reassures us that a proof of the Riemann Hypothesis exists, but the proof is too long for us to inspect directly.</p>
<hr>
<p><b>EDIT:</b> My main question has been answered in the comments, but let me be more explicit about my secondary question. Does my proposal for a succinct circuit <span class="math-container">$C$</span> actually work? Suppose we're looking for proofs of the Riemann Hypothesis of length <span class="math-container">$L$</span>. Given <span class="math-container">$L$</span> explicitly, we can easily verify, in time polynomial in <span class="math-container">$L$</span>, that <span class="math-container">$L$</span> is a valid proof. Moreover, we can write down a 3SAT instance, of size polynomial in <span class="math-container">$L$</span>, that is satisfiable if and only if <span class="math-container">$L$</span> is a valid proof.  But can this 3SAT instance be &quot;compressed&quot; into a circuit <span class="math-container">$C$</span> of size polylogarithmic in <span class="math-container">$L$</span>, in the sense that <span class="math-container">$C$</span> accepts a clause if and only if it belongs to the SAT instance?  It seems to me that there is enough &quot;regularity&quot; to the SAT instance that this should be possible, but I'm a little worried that I'm missing something.</p>

CC BY-SA 4.0
2023-09-22T21:19:36.973Z
'has the possibility that BQP=NEXP
 been rigorously ruled out' answer for that. Yes.. BQP\neq NEXP not known
Turbo
CC BY-SA 4.0
2023-09-23T01:31:03.213Z
Not even BPP = NEXP has been ruled out!
Ryan Williams
CC BY-SA 4.0
2023-09-27T01:00:14.543Z
You might also want to have a look at "implicit proofs" paper by Jan Krajicek: https://www.karlin.mff.cuni.cz/~krajicek/implicit.pdf
Kaveh
CC BY-SA 4.0
2023-09-27T01:07:32.210Z
ps: you can think of it this way: a circuit + a proof that the circuit generates a valid proof. In your quantum case, if you have a proof that the quantum algorithm actually does what it is claimed to do, you may be able to consider those together as a valid proof in a proof system.
Kaveh
<quantum-computing><proof-theory>
Could a quantum computer prove theorems with infeasibly long proofs?
Timothy Chow
# Could a quantum computer prove theorems with infeasibly long proofs?

(Asked by: username_0 on 2023-09-22)

The mathematician Andrew Granville recently published a
"philosophical" article, [Accepted proofs: Objective truth, or culturally robust?](https://mxphi.com/wp-content/uploads/2023/07/Granville.pdf).

At the end, he mentions in passing a suggestion by Carlos Simpson that a
quantum computer might be able to prove theorems whose proofs are too long
to be checkable by a classical computer. My first reaction was that this
was not possible, but as I thought about it more, I realized that I
couldn't rigorously rule it out. Maybe I'm missing something?

One idea might be something like this. Let's say that there's a proof of
the Riemann Hypothesis (in ZFC, say), but the shortest one is many orders
of magnitude larger than we can store on our computers. Nevertheless, our computational power somehow allows us to write down a circuit $C$ which "encodes" the proof, in
the sense that the things $C$ accepts are precisely the Boolean clauses of a
Boolean instance which is satisfiable if and only if the desired proof of
the Riemann Hypothesis exists.

Now, the problem of testing whether the Boolean instance encoded by $C$ is satisfiable is
in $\mathsf{NEXP}$. So my main question is, has the possibility that $\mathsf{BQP} = \mathsf{NEXP}$ been rigorously ruled out?

If not, then it seems that in principle, we could have a situation in which a quantum computer reassures us that a proof of the Riemann Hypothesis exists, but the proof is too long for us to inspect directly.

---

**EDIT:** My main question has been answered in the comments, but let me be more explicit about my secondary question. Does my proposal for a succinct circuit $C$ actually work? Suppose we're looking for proofs of the Riemann Hypothesis of length $L$. Given $L$ explicitly, we can easily verify, in time polynomial in $L$, that $L$ is a valid proof. Moreover, we can write down a 3SAT instance, of size polynomial in $L$, that is satisfiable if and only if $L$ is a valid proof. But can this 3SAT instance be "compressed" into a circuit $C$ of size polylogarithmic in $L$, in the sense that $C$ accepts a clause if and only if it belongs to the SAT instance? It seems to me that there is enough "regularity" to the SAT instance that this should be possible, but I'm a little worried that I'm missing something.

**Tags:** quantum-computing, proof-theory
> **Comments:**
> **username_1**: 'has the possibility that BQP=NEXP  been rigorously ruled out' answer for that. Yes.. BQP\neq NEXP not known  
> **username_2**: Not even BPP = NEXP has been ruled out!  
> **username_3**: You might also want to have a look at "implicit proofs" paper by Jan Krajicek: https://www.karlin.mff.cuni.cz/~krajicek/implicit.pdf  
> **username_3**: ps: you can think of it this way: a circuit + a proof that the circuit generates a valid proof. In your quantum case, if you have a proof that the quantum algorithm actually does what it is claimed to do, you may be able to consider those together as a valid proof in a proof system.  

---

## 0 answers

