1. 11

  2. 2

    This is mind-blowing stuff I barely understand right now. One thing jumped out at me:

    “Yet as other researchers run with the proof, the line of inquiry that prompted it is coming to a halt. For more than three decades, computer scientists have been trying to figure out just how far interactive verification will take them. They are now confronted with the answer, in the form of a long paper with a simple title and echoes of Turing.

    “There’s this long sequence of works just wondering how powerful” a verification procedure with two entangled quantum provers can be, Natarajan said. “Now we know how powerful it is. That story is at an end.””

    That sounds pretty confident. Physicists and mathematicians have been wrong about the universe so many times I’m surprised anyone will claim something is decided after a few people do some work. So, maybe it’s true. Maybe the universe will surprise us again. Who knows.

    1. 3

      RE is effectively the top of complexity theory. All classes next to or beyond it are at least as difficult as Halting, Rice’s Theorem, and all those other friendly theorems from fundamentals of computation. To show that something is equivalent to RE is to show that there is no way to compute it other than to write a program that continually enumerates and guesses and refines its estimates without bound.

      QMIP, or MIP*, is near the top of a tower of interactive proof classes in terms of proof power. We now know how powerful interactive proofs need to get before they are no longer really so interactive: Being convinced of something by multiple quantum agents who have exchanged some qubits with each other is just as powerful as being convinced of something by a pocket calculator which is allowed to run for an arbitrarily long amount of time. (Assuming that the calculator has infinite space, of course; I am being poetic.) So this gives one reason for the research program for interactive proofs to be at a natural turning point; there are no more features to add to IP which can augment its power in interesting ways. The air is thinner up where the classes are harder, and fewer folks work on them; after all, many eyes are on the prize.

      While this proof might sound like a result in physics, it is actually a result in abstract mathematics. The wrongness about the universe in this situation is limited to being wrong about the degree to which quantum logic correctly describes particle physics; however, the proof’s abstracta remain valid on their own foundations. This means that the proof will likely be forward-portable to whatever post-quantum principles physicists choose to use in the future. This pattern is so common in physics that we ought to give it a name; for example, entanglement is possible classically (using Einsteinian mechanics), linear logic (stoichiometry) described chemistry before electrons were identified and still works today in quantum electronics, and puzzles about dishonest guards in front of doors were common for centuries before interactive proof systems were developed formally.

      In the spirit of interactive proofs, I would ask: By what evidence do you doubt this proof? I’ll say that I have 5 nines of certainty in this proof’s correctness, impact, and relationship to other nearby proofs. How much doubt do you have?

    2. 2

      RE really is a very natural class. We first found it when studying Halting in discrete classical computers, but it also shows up when doing physical measurements, when manipulating real numbers, and now here, when simulating multiple quantum agents. This proof may be the end of the saga of interactive proofs, but it is not the end of the saga of Halting and RE.

      1. 1

        Here is a link to their paper “MIP*=RE”: https://arxiv.org/abs/2001.04383

        We show that the class MIP* of languages that can be decided by a classical verifier interacting with multiple all-powerful quantum provers sharing entanglement is equal to the class RE of recursively enumerable languages. Our proof builds upon the quantum low-degree test of (Natarajan and Vidick, FOCS 2018) by integrating recent developments from (Natarajan and Wright, FOCS 2019) and combining them with the recursive compression framework of (Fitzsimons et al., STOC 2019).
        An immediate byproduct of our result is that there is an efficient reduction from the Halting Problem to the problem of deciding whether a two-player nonlocal game has entangled value $1$ or at most $\frac{1}{2}$. Using a known connection, undecidability of the entangled value implies a negative answer to Tsirelson’s problem: we show, by providing an explicit example, that the closure $C_{qa}$ of the set of quantum tensor product correlations is strictly included in the set $C_{qc}$ of quantum commuting correlations. Following work of (Fritz, Rev. Math. Phys. 2012) and (Junge et al., J. Math. Phys. 2011) our results provide a refutation of Connes’ embedding conjecture from the theory of von Neumann algebras.

        It was publicized a month ago by vice but this is a much, much better explanation.