Quantum Computing Since Democritus Lecture 12: Proof
After a ten-month hiatus, the Quantum Computing Since Democritus series sheepishly returns with Lecture 12, which explores how, over the past couple of decades, theoretical computer scientists have bent, twisted, and kneaded the concept of mathematical proof into strange and barely-recognizable forms. Read about proofs that don’t impart any knowledge beyond their own validity, proofs you can check by examining a few random symbols, and (for those who already know that stuff) proofs that certain interpretations of quantum mechanics would predict you can see over the course of your life, yet can’t hold in your mind at any individual time.
I apologize if this lecture isn’t as polished as some earlier ones — but while I’m working on this, I’m now also teaching a new course at MIT, 6.080/6.089 Great Ideas in Theoretical Computer Science. Barring unforeseen delays, the lecture notes for that course should be available by 2043.
Follow
Comment #1 February 12th, 2008 at 2:42 am
Excellent! I look forward to seeing it narrated by attractive women in the form of a printer advert on Australian TV.
Comment #2 February 12th, 2008 at 3:25 am
Yay!
Hoping you someday get at least to Lecture 13 before giving up, I’m curious about that one… 🙂
By the way, one very small thing I’m not sure you noticed: On your blog front page, the Quantum Computing Since Democritus sidebar has the lectures in strict lexical order… such that “Lecture 11:” is sorted before “Lecture 1:”…
Comment #3 February 12th, 2008 at 7:27 am
A fun “confection” for the Great Ideas course is the SIAM News 22(4) Editors Name Top Ten Algorithms. I especially enjoyed the SIAM editors comment “Most algorithms take shape over time, with many contributors.” Who should know better than an editor?
Comment #4 February 12th, 2008 at 9:18 am
Coin: Unfortunately, one “feature” of the latest version of WordPress is that apparently they took away the ability to sort the links as one wishes. Does anyone know how to get that ability back?
(Update: Alright, I figured out how to edit the PHP script so that the lectures are correctly sorted. Enjoy!)
Comment #5 February 12th, 2008 at 9:28 am
Okay, so if I understand correctly, ever NP problem admits a PCP. The naive intuition is demonstrated by using the exponential encoding that you mentioned, but you claim there is always a poly-sized encoding. So given a valid proof, what is the computational complexity of finding a valid poly-sized encoding?
Comment #6 February 12th, 2008 at 9:29 am
Steve: Polynomial.
Comment #7 February 12th, 2008 at 12:28 pm
Thank you!
Comment #8 February 12th, 2008 at 1:19 pm
Here is one of my favorite quotes regarding physics, quantum computation and mathematical proofs:
“Among the many ramifications of quantum computation for apparently distant fields of study are its implications for the notion of mathematical proof. Performing any computation that provides a definite output is tantamount to proving that the observed output is one of the possible results of the given computation. Since we can describe the computer’s operations mathematically, we can always translate such a computation into the proof of some mathematical theorem. This was the case classically too, but in the absence of interference effects it is always possible to keep a record of the steps of the computation, and thereby produce (and check the correctness of) a proof that satisfies the classical definition – as “a sequence of propositions each of which is either an axiom or follows from earlier propositions in the sequence by the given rules of inference”. Now we are forced to leave that definition behind. Henceforward, a proof must be regarded as a process — the computation itself — for we must accept that in future, quantum computers will prove theorems by methods that neither a human brain nor any other arbiter will ever be able to check step-by-step, since if the
‘sequence of propositions’ corresponding to such a proof were printed out, the paper would fill the observable universe many times over.”
Machines, Logic and Quantum Physics
David Deutsch and Artur Ekert
November 19, 1999
http://xxx.lanl.gov/PS_cache/math/pdf/9911/9911150v1.pdf
Comment #9 February 12th, 2008 at 1:27 pm
…proofs that certain interpretations of quantum mechanics predict you can have seen over the course of your life but can’t hold in your mind at any individual time
This doesn’t parse. =) Can you give a translation?
Comment #10 February 12th, 2008 at 2:20 pm
Jon: Read the lecture!
Comment #11 February 12th, 2008 at 2:39 pm
I had trouble parsing that too. I had to read it three or four times to understand that “that certain interpretations…” is not what’s being proved, but an adjectival clause describing the proofs.
Since I’m currently in editing mode, let me suggest “proofs that certain interpretations of quantum mechanics would predict that you can see over the course of your life but that you can’t hold in your mind at any individual time.”
Comment #12 February 12th, 2008 at 2:48 pm
Sorry, I should have noted that the paper I reference above was co-authored as well by Rossella Lupacchini.
Comment #13 February 12th, 2008 at 3:27 pm
Michael: While that quote from Deutsch et al. is music to my ears, the one thing I’d add is that even before quantum computing became a field, computer scientists had already generalized the notion of proof in the way they describe (from a static sequence of symbols to a computational process) for completely unrelated reasons.
Comment #14 February 12th, 2008 at 8:45 pm
Michael: One criticism of Deutsch’s quote above is that it is probably not possible even in principle to know what the Hamiltonian of your actual quantum computer is over time. This seems to me to be a big issue.
“Performing any computation that provides a definite output is tantamount to proving that the observed output is one of the possible results of the given computation. Since we can describe the computer’s operations mathematically, we can always translate such a computation into the proof of some mathematical theorem.”
All the statements here are true BUT knowing exactly what “the given computation” actually was seems problematic. Another way of saying this is that which “mathematical theorem” is being proved depends on the details of your physical system, which you probably can’t know. You can write down an effective Hamiltonian which you think describes your system, and assume that this is the mathematical machinery of interest, but in actuality the true physics of the system is probably not fully described by the best effective Hamiltonian you can generate.
Imagine you set up your quantum computation to test whether or not the answer “zero” is possible. You run the computation and lo and behold you get “zero”. Is this an ironclad “proof” that zero is possible for this computation? No, because your model of the QC may not in actuality be what the QC is doing (the Hamiltonian problem above), and it may be this (potentially very small difference) that’s allowing the answer to be zero, and not some fundamental truth about nature.
Comment #15 February 12th, 2008 at 9:16 pm
Geordie: Yes, I agree that a computational proof is only as good as the assumptions about the underlying physics (even if the assumption is just that the prover can’t predict the verifier’s random coin tosses, as for PCP’s). Maybe I didn’t stress that enough in the lecture.
Comment #16 February 12th, 2008 at 11:12 pm
In the zero-knowledge proof section you have:
That person then asks: “which graph did I start with?” If the graphs are not isomorphic, then you should be able to answer this question with certainty.
Should that not be there? If so then i don’t understand that section.
Comment #17 February 12th, 2008 at 11:38 pm
I’m not sure I understand the proof sketch for 3-colorability in CZK. When you encrypt the colors, are you throwing in some additional data along with it (so, instead of hashing “red” over and over again, you’re hashing “red12349” versus “red29304” etc.?) Otherwise I don’t see how the prover isn’t just giving the verifier a 3-coloring.
Comment #18 February 12th, 2008 at 11:56 pm
Job: Yes, the “not” should be there. If two graphs are isomorphic, then obviously you can’t know which one you’re looking at a permutation of.
Comment #19 February 12th, 2008 at 11:57 pm
Harrison, i think that’s the case. And i have another question: why would the verifier become convinced if it can’t verify that the prover is properly decoding the colors? Is the verifier taking for granted that the prover is honest? Otherwise the prover can always “decode” the colors such that they’re different (the verifier doesn’t have the decoder algorithm, so he’s none the wiser).
Comment #20 February 12th, 2008 at 11:58 pm
Harrison: Yes, you throw in additional random data along with the colors. (Modern encryption schemes always throw in additional data, for exactly the reason you say.)
Comment #21 February 13th, 2008 at 12:01 am
Thanks – duh! on my original coment.
Comment #22 February 13th, 2008 at 12:03 am
Job: After the prover decrypts the colors, the verifier just checks for himself whether the decryptions are correct. (For this to work, obviously you need a cryptosystem with unique decryption, but that’s known to exist assuming one-way functions.)
I apologize for skipping these details; will fill them in when I get a chance.
Comment #23 February 13th, 2008 at 6:25 am
Just one question from someone who is not familiar with interactive protocols:
In the protocol of 3-colorability, how could the verifier know if the decryption is valid? You, the prover, are the one who encrypted the colors of the two vertices and you are the one who decrypted them, so you can decrypt them as red and blue all the time (cheating) and the verifier won’t know whether this is a valid decryption or not.
Have I missed something?
Comment #24 February 13th, 2008 at 6:31 am
Sorry, I didn’t notice that my question was already posed by someone else.
Comment #25 February 13th, 2008 at 9:37 am
Again, you encrypt in such a way that there’s only one valid way to decrypt. For example, let’s say you want to encrypt a single bit. If the bit is 0, then multiply together two huge prime numbers neither of which ends with a ‘7’. If the bit is 1, multiply together two huge prime numbers at least one of which ends with a ‘7’. Use the product as the ciphertext.
Because every number has a unique prime factorization, and because it’s possible to determine efficiently whether a number is prime, you just have to send the verifier the prime factors and then the verifier can check for himself that the decryption is correct.
Comment #26 February 13th, 2008 at 10:02 am
” . . . computer scientists had already generalized the notion of proof in the way they describe (from a static sequence of symbols to a computational process) for completely unrelated reasons.”
Scott,
Is this the same as the authors’ contention that quantum computation shows ” . . . that neither a human brain nor any other arbiter will ever be able to check step-by-step, since if the ‘sequence of propositions’ corresponding to such a proof were printed out, the paper would fill the observable universe many times over.”
My sense was that the implications of quantum computation — even if only based on our assumptions about the underlying physics (what isn’t?) — can be thought of as proving the classical intuition.
Perhaps though this isn’t the right way to look at it.
Comment #27 February 13th, 2008 at 10:10 am
Michael, if the set of all possible challenges and responses that could be exchanged in a classical interactive protocol were printed out, it would also fill the observable universe.
As for what doesn’t depend on any assumptions about physics: arguably, conventional mathematical proofs (like the proof that √2 is irrational). But I don’t want to start another flamewar about this.
Comment #28 February 13th, 2008 at 10:15 am
Thanks Scott.
Comment #29 February 13th, 2008 at 4:25 pm
See also:
http://terrytao.wordpress.com/2008/01/04/pcm-article-generalised-solutions/#comment-23080
“… The [Princeton] Companion [of Philosophy] also has a section on history of mathematics; for instance, here is Leo Corry’s PCM article “The development of the idea of proof”, covering the period from Euclid to Frege. We take for granted nowadays that we have precise, rigorous, and standard frameworks for proving things in set theory, number theory, geometry, analysis, probability, etc., but it is worth remembering that for the majority of the history of mathematics, this was not completely the case; even Euclid’s axiomatic approach to geometry contained some implicit assumptions about topology, order, and sets which were not fully formalised until the work of Hilbert in the modern era. (Even nowadays, there are still a few parts of
mathematics, such as mathematical quantum field theory, which still do not have a completely satisfactory formalisation, though hopefully the situation will improve in the future.)…”
===========
I’d previously cross-posted:
5 January, 2008 at 2:21 pm
Jonathan Vos Post
I’ve cited this thread, and excerpted the wonderful Leo Corry’s article “The development of the idea of proof”, over at January 2, 2008 Two Cultures in the Philosophy of Mathematics? Posted by David Corfield, on the n-Category Cafe.
=========
Or am I thinking of the book “The Princeton Companion to Mathematics” by Gowers, T., ?
=========
I cannot resist adding:
36 Methods of Mathematical Proof
http://www.bluemoon.net/%7Ewatson/proof.htm
Proof by obviousness
“The proof is so clear that it need not be mentioned.”
[truncated]
…
Proof by intuition
“I just have this gut feeling. . .”
[JVP: and the last is not as silly as it sounds, because the human gastrointestinal tract has approximately 10^9 neurons embedded in its layers of the 20+ feet of nonaxisymmetric concentric cylinders, histologically speaking, with is fully 1% as many neurons as in the brain in your skull, and more than are in the spinal cord. I am simulating this system in SBML (Systems Biology Markup Language) for a paper by myself and Dr. Thomas L. Vander Laan, M.D., F.A.C.S, FCCWS, to be submitted to “Nature” on what I unofficially call a General Unified Theory of the Gut, or G.U.T. of GUT, and is to be clinically tested at USC Medical School. This is, in a sense, an application of the absolutely gorgeous (and includes proofs) paper “Nonlinear Dynamics of Networks: The Groupoid Formalism” by Ian Stewart and
Martin Golubitsky, Bull. Amer. Math. Soc., July 2006, pp.305-364)]