Shtetl-Optimized

There’s a trivial question about particle accelerators that bugged me for a while. Today I finally figured out the answer, and I’m so excited by my doofus “discovery” that I want to tell the world.

In Ye Olde Times, accelerators used to smash particles against a fixed target. But today’s accelerators smash one particle moving at almost the speed of light against another particle moving at almost the speed of light — that’s why they’re called particle colliders (duhhh). Now, you’d think this trick would increase the collision energy by a constant factor, but according to the physicists, it does asymptotically better than that: it squares the energy!

My question was, how could that be? Even if both particles are moving, we can clearly imagine that one of them is stationary, since the particles’ motion with respect to the Earth is irrelevant. So then what’s the physical difference between a particle hitting a fixed target and two moving particles hitting each other, that could possibly produce a quadratic improvement in energy?

[Warning: Spoiler Ahead]

The answer pops out if we consider the rule for adding velocities in special relativity. If in our reference frame, particle 1 is headed left at a v fraction of the speed of light, while particle 2 is headed right at a w fraction of the speed of light, then in particle 1’s reference frame, particle 2 is headed right at a (v+w)/(1+vw) fraction of the speed of light. Here 1+vw is the relativistic correction, “the thing you put in to keep the fraction less than 1.” If v and w are both close to 0, then of course we get v+w, the Newtonian answer.

Now set v=w=1-ε. Then (v+w)/(1+vw) = 1 – ε²/(2-2ε+ε²), which scales like 1-ε². Aha!

To finish the argument, remember that relativistic energy increases with speed like 1/sqrt(1-v²). If we plug in v=1-ε, then we get 1/sqrt(2ε-ε²), while if we plug in v=1-ε², then we get 1/sqrt(2ε²-ε⁴). So in the case of a fixed target the energy scales like 1/sqrt(ε), while in the case of two colliding particles it scales like 1/ε.

In summary, nothing’s going on here except relativistic addition of velocities. As with Grover’s algorithm, as with the quantum Zeno effect, it’s our intuition about linear versus quadratic that once again leads us astray.

Follow

The most important research question in astronomy, to judge from the news websites, is neither the nature of dark matter and energy, nor the origin of the Pioneer anomaly or gamma-ray bursts beyond the GZK cutoff, nor the possible existence of Earth-like extrasolar planets. No, the big question is whether Pluto is “really” a planet, and if so, whether Charon and Ceres are “really” planets, and whether something has to be round to be a planet, and if so, how round.

I was going to propose we bring in Wittgenstein to settle this. But I guess the astronomers have already “ruled.”

Richard Dawkins often rails against what he calls the “tyranny of the discontinuous mind.” As far as I know, he’s not complaining about those of us who like our Hilbert spaces finite-dimensional and our quantum gravity theories discrete. Rather, he’s complaining about those who insist on knowing, for every humanoid fossil, whether it’s “really” human or “really” an ape. Ironically, it’s often the same people who then complain about the “embarrassing lack of transitional forms”!

Can anyone suggest a word for a person obsessed with drawing firm but arbitrary lines through a real-valued parameter space? (“Lawyer” is already taken.) I’ve already figured out the word for a debate about such lines, like the one we saw in Prague: chasmgasm.

Follow

In a comment on my last post, Bram Cohen writes:

This whole business of ‘formality’ and ‘review’ is really kind of dumb. A mathematical theorem is only really proven when a computer can verify the proof. Until then, it’s just hand-waving which has some degree of utility when generating a real proof.

Were it standard to present proofs in computer-checkable form, there would be no review process at all. In fact it would be possible to send a proof to a theorem server which would automatically accept any proof which checked out. Had Perelman submitted to one of those, we wouldn’t have had any review process at all, and had complete confidence from day 1, and there wouldn’t be any of this stupid game of who really proved it by making the arguments sufficiently ‘formal’ or ‘detailed’.

I view the switch to doing mathematics in the style just described as inevitable…

Like Bram, I also hope and expect that mathematicians will eventually switch to machine-readable proofs supplemented by human-readable explanations. That would certainly beat the current standard, proofs that are readable by neither machines nor humans.

So then why hasn’t it happened already? Probably the best way to answer this question is to show you the proof, in a state-of-the-art formal verification system called HOL Light, that the square root of 2 is irrational.

let rational = new_definition
`rational(r) = ?p q. ~(q = 0) / abs(r) = &p / &q`;;

let NSQRT_2 = prove
(`!p q. p * p = 2 * q * q ==> q = 0`,
MATCH_MP_TAC num_WF THEN REWRITE_TAC[RIGHT_IMP_FORALL_THM] THEN
REPEAT STRIP_TAC THEN FIRST_ASSUM(MP_TAC o AP_TERM `EVEN`) THEN
REWRITE_TAC[EVEN_MULT; ARITH] THEN REWRITE_TAC[EVEN_EXISTS] THEN
DISCH_THEN(X_CHOOSE_THEN `m:num` SUBST_ALL_TAC) THEN
FIRST_X_ASSUM(MP_TAC o SPECL [`q:num`; `m:num`]) THEN
POP_ASSUM MP_TAC THEN CONV_TAC SOS_RULE);;

let SQRT_2_IRRATIONAL = prove
(`~rational(sqrt(&2))`,
SIMP_TAC[rational; real_abs; SQRT_POS_LE; REAL_POS; NOT_EXISTS_THM] THEN
REPEAT GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
DISCH_THEN(MP_TAC o AP_TERM `x. x pow 2`) THEN
ASM_SIMP_TAC[SQRT_POW_2; REAL_POS; REAL_POW_DIV; REAL_POW_2; REAL_LT_SQUARE;
REAL_OF_NUM_EQ; REAL_EQ_RDIV_EQ] THEN
ASM_MESON_TAC[NSQRT_2; REAL_OF_NUM_EQ; REAL_OF_NUM_MUL]);;

Cool — now let’s do Fermat and Poincaré! Any volunteers?

Seriously, the biggest accomplishments to date have included formal proofs of the Jordan Curve Theorem (75,000 lines) and the Prime Number Theorem (30,000 lines). If you want to know which other famous theorems have been formalized, check out this excellent page. Or look at these notes by Harvey Friedman, which cut through the crap and tell us exactly where things stand.

A huge part of the problem in this field seems to be that there’s neither a standard proof format nor a standard proof repository — no TeX or HTML, no arXiv or Wikipedia. Besides HOL Light, there’s also ProofPower, Isabelle, Coq, Mizar, and several other competitors. I’d probably go with Mizar, simply because the proofs in it look the most to me like actual math.

Friedman gives machine-readable proofs fifty years to catch on among “real” mathematicians. That seems about right — though the time could be reduced if the Don Knuth, Tim Berners-Lee, Paul Ginsparg, or Jimmy Wales of proof-checking were to appear between now and then. As usual, it mostly comes down to humans.

Update: Freek Wiedijk put together a fantastic online book, which shows the proofs that the square root of 2 is irrational in 17 different formal systems. The “QED Manifesto” is also worth a look. This manifesto makes it clear that there are people in the formal verification world with a broad enough vision — if you like, the Ted Nelsons of proof-checking. Nelson is the guy who dreamed in 1960 of creating a global hypertext network. In his case, it took 35 years for the dream to turn into software and protocols that people actually wanted to use (not that Nelson himself is at all happy with the result). How long will it take in the case of proof-checking?

Follow

So, this year’s Fields Medals go to Terence Tao and Grisha Perelman (duhhhh), as well as to Andrei Okounkov and Wendelin Werner. The Nevanlinna Prize goes to an already-prize-bedecked Jon Kleinberg, my professor at Cornell way back in ’97. Congratulations to all!

Meanwhile, there’s a long article in yesterday’s New Yorker about Perelman and the Poincaré conjecture, by Sylvia Nasar (the media’s go-to person for reclusive mathematical geniuses) and David Gruber. Unfortunately the article’s not on the web, but fearless detective that I am, I was able to track it down in a so-called “bookstore.”

Nasar and Gruber find Perelman in a St. Petersburg apartment, where he lives with his mom, doesn’t check his mail, and just generally makes Andrew Wiles look like a hard-partying, elliptic-curve-modularizing regular dude. Perelman is nevertheless happy to grant Nasar and Gruber an interview, to confirm that he intends to be the first person in history to turn down the Fields, and to complain about his fellow mathematicians’ lax ethical standards.

What exactly is he talking about? It wasn’t clear to me, but Nasar and Gruber devote much of their article to an indictment of 1982 Fields Medalist Shing-Tung Yau, who they portray as trying to usurp credit from Perelman for the benefit of his students Xi-Ping Zhu and Huai-Dong Cao. (Zhu and Cao wrote a 328-page exposition of Perelman’s ideas, complementing other expositions by Bruce Kleiner and John Lott and by John Morgan and Gang Tian.) I have no idea to what extent, if any, the criticism of Yau is justified. But to my mind, failing to write up your result properly, and then getting upset when those who do write it up properly try to share credit, is a bit like leaving your wallet on the sidewalk and then shaking your head at human depravity when someone tries to steal it.

Nasar and Gruber also don’t comment on the obvious irony of Perelman’s “unworldliness”: that, by being such a fruitcake, he’s guaranteeing he’ll draw vastly more attention to himself than he would by just accepting the goddamned medal. (Feynman, though not exactly publicity-shy, employed similar reasoning to conclude that turning down the Nobel Prize would be a bad idea.) Indeed, supposing Perelman did aspire to celebrity status, my public-relations advice to him would be to do exactly what he’s doing right now.

Update: The New Yorker article is now online.

Follow

Alright, I can give an oracle relative to which BQP is not in SZK, thereby knocking off one of the Ten Most Annoying Questions in Quantum Computing.

It’s a forehead-slapper. Just take the problem from the paper Exponential algorithmic speedup by quantum walk by Andrew Childs et al. Here the oracle encodes an exponentially large graph, consisting of two binary trees conjoined at the leaves by a random cycle:

(I hope Childs et al. will forgive me for swiping their graphic.)

Each vertex is labeled by a random string, and given the label of a vertex, the oracle tells us the labels of its neighbors. Then, given the label of the Entrance vertex, the problem is to decide (let’s say) whether the label of the Exit vertex starts with a 1 or a 0.

Childs et al. proved that this oracle problem is in BQP but not in BPP. Intuitively, any classical random walk on the graph will get stuck for an exponentially long time in the enormous middle region, but because of interference effects, a quantum walk will tunnel right through to the Exit vertex with 1/polynomial probability.

Now, it’s easy to generalize their proof that the problem is not in BPP, to show that it’s not in SZK. One way to see this is that, for a prover to convince a verifier of the solution, the prover will (basically) have to reveal where the Exit vertex is, thereby violating the zero-knowledge property. Another way to see it is that, if we consider the Sahai-Vadhan characterization of SZK in terms of the Statistical Difference problem, then neither of the two distributions we’re comparing will depend non-negligibly on the Exit vertex.

Disappointingly, this solution is way too trivial to publish, and almost too trivial even to blog. On the other hand, so far I’ve been unable to extend the solution to get an oracle relative to which BQP is not in AM. Every variant of the problem I’ve come up with is in AM intersect coAM, sometimes for non-obvious reasons. Anyone want to help me?

Follow

I’ve decided to “launch” my latest paper on the blogosphere even before posting it to quant-ph — so that you, my loyal readers, can be the very first to lay eyes on it. (True fact: as I was writing, I didn’t look once at the screen.) Comments more than welcome.

The Learnability of Quantum States [PS] [PDF]
Scott Aaronson

Abstract: Let me warn you up-front, this is one big-ass mother of a paper. It’s got learning. It’s got quantum. It’s got philosophy. It’s got weird complexity classes (naturally). It’s even got experimental physics applications (don’t worry, I showered afterward). And dude. When I say “experimental,” I’m not talking wormholes or anthropic postselection. I’m talking stuff that you, the quantum state tomographer, can try in your lab today. And no, this is not the real abstract.

Update (8/20): I’ve posted a slightly revised version, mostly in response to the comments I received here.

Follow

1. Given an n-qubit pure state, is there always a way to apply Hadamard gates to some subset of the qubits, so as to make all 2ⁿ computational basis states have nonzero amplitudes?
2. Can we get any upper bound on QMIP (quantum multi-prover interactive proofs with unlimited prior entanglement)? It would suffice to show (for example) that the provers never need more than Ackermann(n) ebits of entanglement.
3. Can any QMA(2) (QMA with two unentangled yes-provers) protocol be amplified to exponentially small error probability? If you think the answer is trivially yes, think about it some more!
4. If a unitary operation U can be applied in polynomial time, then can some square root of U also be applied in polynomial time?
5. Suppose Alice and Bob are playing n parallel CHSH games, with no communication or entanglement. Is the probability that they’ll win all n games at most pⁿ, for some p bounded below 0.853?
6. Forget about an oracle relative to which BQP is not in PH. Forget about an oracle relative to which BQP is not in AM. Is there an oracle relative to which BQP is not in SZK?
7. Given any n-qubit unitary operation U, does there exist an oracle relative to which U can be (approximately) applied in polynomial time?
8. How many mutually unbiased bases are there in non-prime-power dimensions? (Alright, I don’t care about this one, but so many people do that I figured I’d put it in.)
9. Is there an n-qubit pure state that can be prepared by a circuit of size n³, and that can’t be distinguished from the maximally mixed state by any circuit of size n²?
10. Fill this space with your own annoying question! Here are the rules: the question must involve quantum. It must be annoying. It must be clearly-stated — no open-ended pontificating allowed. It can’t be an Everest of the field, like graph isomorphism or increasing the fault-tolerance threshold. Instead it should be a dinky little molehill, that’s nevertheless caused all would-be climbers to fall flat on their asses.

Follow

Yes.

Follow

If you hadn’t been reading the comments on my last post, you might not know that my old chum Mahmoud Ahmadinejad had launched his own blog on Sunday. Along with a rambling autobiography, this exciting new blog (which I’ve added to my linklog on the right) also includes a poll:

Do you think that the US and Israeli intention and goal by attacking Lebanon is pulling the trigger for another word [sic] war?

When I first visited, only 5% had voted “yes”, though it’s now up to 50%.

But wait, it gets better: if Mahmoud’s site identifies your IP address as coming from Israel, then it tries to install a virus on your computer by exploiting an Internet Explorer vulnerability. (Thanks to an anonymous commenter for bringing this to my attention.)

I suppose we should grateful that, at least for now, defending oneself against the modern-day Hitler is as simple as installing Firefox.

Follow

Sorry for the long delay! I had to be in Washington D.C. this week, for reasons I’m not at liberty to disclose. (Yes, I’m serious, and no, it’s not as interesting as it sounds.) Oh: on my way back to Canada, for some strange reason they confiscated my Blistex. I guess airport security guards get chapped lips a lot.

As our world descends even further into war, terror, and Armageddon, I have an exciting complexity-theoretic announcement. Building on the Complexity Zoo, Greg Kuperberg has created a “Robozoologist”: an expert system for reasoning about complexity classes. What’s more, Greg is releasing some spinoffs of his project to the masses, including a JavaScript-powered inclusion graph, and an automatically-generated RoboZoo. I can still remember them frontier days of 2002, when I had to herd the BP operators with my two bare hands…

Follow