Amazing progress on longstanding open problems

For those who haven’t seen it:

1. Aubrey de Grey, better known to the world as a radical life extension researcher, on Sunday posted a preprint on the arXiv claiming to prove that the chromatic number of the plane is at least 5—the first significant progress on the Hadwiger-Nelson problem since 1950.  If you’re tuning in from home, the Hadwiger-Nelson problem asks: what’s the minimum number of colors that you need to color the Euclidean plane, in order to ensure that every two points at distance exactly 1 from each other are colored differently?  It’s not hard to show that at least 4 colors are necessary, or that 7 colors suffice: try convincing yourself by staring at the figure below.  Until a few days ago, nothing better was known. This is a problem that’s intrigued me ever since I learned about it at a math camp in 1996, and that I spent at least a day of my teenagerhood trying to solve. De Grey constructs an explicit graph with unit distances—originally with 1567 vertices, now with 1585 vertices after after a bug was fixed—and then verifies by computer search (which takes a few hours) that 5 colors are needed for it.  So, can we be confident that the proof will stand—i.e., that there are no further bugs?  See the comments of Gil Kalai’s post for discussion.  Briefly, though, it looks like it’s now been independently verified, using different SAT-solvers, that the chromatic number of de Grey’s corrected graph is indeed 5, including by my good friend Marijn Heule at UT Austin. If and when it’s also mechanically checked that the graph is unit distance (i.e., that it can be embedded in the plane with distances of 1), I think it will be time to declare this result correct.  Update: De Grey emailed to tell me that this part has now been independently verified as well.  I’ll link to details as soon as I have them. Question for experts: is there a general principle by which we can show that, if the chromatic number of the plane is at least 6, or is 7, then there exists a finite subgraph that witnesses it?  (This is closely related to asking, what’s the logical complexity of the Hadwiger-Nelson problem: is it Π₁?)  Update: As de Grey and a commenter pointed out to me, this is the de Bruijn-Erdös Theorem from 1951.  But the proofs inherently require the Axiom of Choice.  Still not sure about the Π₁ part.
2. Last week, Urmila Mahadev, a student (as was I, oh so many years ago) of Umesh Vazirani at Berkeley, posted a preprint on the arXiv giving a protocol for a quantum computer to prove the results of any computation it performs to a classical skeptic—assuming a relatively standard cryptographic assumption, namely the quantum hardness of the Learning With Errors (LWE) problem, and requiring only classical communication between the skeptic and the QC.  I don’t know how many readers remember, but way back in 2006, inspired by a $25,000 prize offered by Stephen Wolfram, I decided to offer a $25 prize to anyone who could solve the problem of proving the results of an arbitrary quantum computation to a classical skeptic, or who could give oracle evidence that a solution was impossible.  I had first learned this fundamental problem from Daniel Gottesman. Just a year or two later, independent work of Aharonov, Ben-Or, and Eban, and of Broadbent, Fitzsimons, and Kashefi made a major advance on the problem, by giving protocols that were information-theoretically secure.  The downside was that, in contrast to Mahadev’s new protocol, these earlier protocols required the verifier to be a little bit quantum: in particular, to exchange individual unentangled qubits with the QC.  Or, as shown by later work, the verifier could be completely classical, but only if it could send challenges to two or more quantum computers that were entangled but unable to communicate with each other.  In light of these achievements, I decided to award both groups their own checks for half the prize amount ($12.50), to be split among themselves however they chose. Neither with Broadbent et al.’s or Aharonov et al.’s earlier work, nor with Mahadev’s new work, is it immediately clear whether the protocols relativize (that is, whether they work relative to an arbitrary oracle), but it’s plausible that they don’t. Anyway, assuming that her breakthrough result stands, I look forward to awarding Urmila the full $25 prize when I see her at the Simons Institute in Berkeley this June.

Huge congratulations to Aubrey and Urmila for their achievements!