Sunday, August 27, 2006

Bananas

In the wake of my very public relativity humiliation, I've decided to sentence myself to a one-month punishment term of only blogging about things that I actually understand. That means, unfortunately, that from now until September 27 this blog is going to be quite boring and limited in scope. It also means that Lev R.'s prizewinning question, about the survival prospects of the human race, will need to be deferred until after the punishment term.

To be clear: No string theory. No global warming. No biting vaginas. No Mahmoud. Quantum complexity classes are probably kosher.

The remainder of today's entry will be about the topic of bananas. Bananas are long, yellow fruits that grow in bunches on some sort of plant or other. They consist of two components: the peel, and the "meat." Well, there are probably other components as well, but those two are the most readily identifiable. The meat is delicious when fresh, even more so if covered with chocolate. When not fresh, on the other hand, it tends to form brown spots. The peel is not so good to eat, but is reputed to good for tripping dumb, careless, unwary people. Like me.

Saturday, August 26, 2006

Why I'm not a physicist: reason #4329

I botched the calculation. While I got the answer I wanted (a quadratic improvement in energy), and while I more-or-less correctly identified the reason for that answer (unintuitive properties of the relativistic velocity addition formula), I did the calculation in the rest frame of one of the particles instead of the zero-momentum rest frame, and thereby obtained a scaling of 1/sqrt(ε) versus 1/ε instead of 1/ε1/4 versus 1/sqrt(ε). As a result, my answer flagrantly violates conservation of energy.

Thanks to rrtucci and perseph0ne. In my defense, I did call it a doofus discovery.

Why I'm not a physicist: reason #4328

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-2ε+ε2), which scales like 1-ε2. Aha!

To finish the argument, remember that relativistic energy increases with speed like 1/sqrt(1-v2). If we plug in v=1-ε, then we get 1/sqrt(2ε-ε2), while if we plug in v=1-ε2, then we get 1/sqrt(2ε24). 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.

Friday, August 25, 2006

Chasmgasm

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.

A far-off dream: automating a problem in P

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?

Tuesday, August 22, 2006

Fruitcake fields

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.

Monday, August 21, 2006

Low-hanging fruit from two conjoined trees

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?

Thursday, August 17, 2006

Pipin'-hot learnin' theorems

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.

Tuesday, August 15, 2006

The ten most annoying questions in quantum computing

  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 2n 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 pn, 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 n3, and that can't be distinguished from the maximally mixed state by any circuit of size n2?

  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.

Is it possible to write a competent newspaper article about math?

Breaking Mahmoud news -- too hot for Slashdot

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.

Saturday, August 12, 2006

CIA, NSA, FBI, DoD, SZK, RNC, QMA, BPE

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...

Tuesday, August 01, 2006

Merneptah and Spinoza

A reader from Istanbul wrote in, asking me to comment on the war in Israel and Lebanon. In other words, he wants me to make this blog the scene of yet another intellectual bloodbath, with insult-laden rockets launched from untraceable IP addresses and complexity-theoretic civilians trapped in the crossfire. What a neat idea! Why didn't I think of it before?

Alright, let me start with some context. No, I'm not talking about the Gaza pullout, or Camp David, or the last Lebanon invasion, or the Yom Kippur War, or the Six-Day War, or the War of Independence, or the UN partition plan, or the 1939 White Paper. I'm talking about the first appearance of Israel in the extrabiblical historical record, which seems to have been around 1200 BC. Boasting in a victory stele about his recent military conquests in Canaan, the Egyptian pharaoh Merneptah included a single sentence about Israel:
Israel is laid waste; his seed is destroyed.
Sure, the pharoah was a bit premature. But give him credit for prescience if not for accuracy. Unlike (say) pyramid-building or Ra-worship, Merneptah's Jew-killing idea has remained consistently popular for 3.2 millennia.

Today, in the year 2006, as the LHC prepares to find the Higgs boson and the New Horizons probe heads to Pluto, Am Yisra'el (literally, "the people that argues with God") is once again surrounded by enemies whose stated goal is to wipe it off the face of the Earth. And, in the familiar process of fighting for its existence, that people is grievously, inexplicably, incompetently, blowing up six-year-olds and farmers while failing to make any visible progress on its military objectives.

So what is there to say about this that hasn't already been said Ackermann(50) times? Instead of cluttering the blogosphere any further, I'll simply point you to a beautiful New York Times op-ed by Rebecca Goldstein, commemorating the 350th anniversary of Spinoza's excommunication from the Jewish community of Amsterdam. Actually, I'll quote a few passages:
Spinoza’s reaction to the religious intolerance he saw around him was to try to think his way out of all sectarian thinking. He understood the powerful tendency in each of us toward developing a view of the truth that favors the circumstances into which we happened to have been born. Self-aggrandizement can be the invisible scaffolding of religion, politics or ideology.

Against this tendency we have no defense but the relentless application of reason.

Spinoza’s system is a long deductive argument for a conclusion as radical in our day as it was in his, namely that to the extent that we are rational, we each partake in exactly the same identity.

Spinoza’s dream of making us susceptible to the voice of reason might seem hopelessly quixotic at this moment, with religion-infested politics on the march. But imagine how much more impossible a dream it would have seemed on that day 350 years ago.

America the nonexistent

A commenter on a previous post writes:
A lot of great discoveries came from non-scientific losers. E=MCC. Airplanes. America. Someone discovered how to make an airplane by playing with a box. Physics is mostly theoretical. America, I guess, is the most scientific discovery. They applied the scientific method to determine its existence, but they used no control group, and no placebo. For that, America's existence is not yet proven. There seem to be other ways of establishing truth than just the scientific method. Scientists are contemporary soothsayers. They should use every means possible of proving a fact.
Despite its insightfulness and coherence, the above argument raises some immediate questions:
  1. What does it have to do with anything I said?

  2. E=MCC?

  3. What would mean to use a placebo or control group to test America's existence? Would it mean sending a ship in a different direction, and checking that it didn't also reach America? Would it mean verifying that America can't be reached from Europe by foot -- since if it could, then it wouldn't be America, but rather part of Eurasia?

  4. Has England's existence been scientifically proven? What about France's?

  5. Where do so many people get the cockamamie idea that there's such a thing as a "scientific method" -- that science is not just really, really, really careful thinking? (I blame the school system.)