Short and Tweet
Proofs that are about the length of a tweet.
Jack Dorsey is the creator of Twitter. We thank him for the creation of of tweets, which are of course messages of up to 140 characters in length.
Today Ken and I wish to talk about very short proofs—proofs that could almost fit into a single tweet.
It’s a fun topic, but also touches on a serious one: what is a proof really supposed to do?
These proofs must be hard to find but quick to verify, which is the essential idea of .
Let’s look at problems whose solutions fit into a single tweet, or almost.
Trying to generalize Fermat’s Last Theorem, the great Leonhard Euler conjectured that an th power cannot be written as the sum of fewer than nontrivial powers for .
Leon Lander and Thomas Parkin used a computer to solve the problem for and found a counterexample. Here is their whole paper:
Note, if they had just sent the answer it would have been:
Writing this as a LaTeX formula would have easily fit into a single Tweet—too bad they did their work 46 years ago.
Two decades later, Noam Elkies found a method to construct an infinite series of counterexamples for the case. He showed that
In 1988, Roger Frye found the smallest counterexample based on Elkies’ ideas:
Note that always has the integer roots , which are distinct when . And
is solvable in integers by , , , among many other possibilities.
has four distinct integer roots in pairs and .
Going from degree to , we can solve
with , , and . These induce , , , and , again giving -many distinct integer roots.
Can we do this with for
There had been a conjecture—indeed, a claimed proof—of “no,” but Dominic Symes found an example—or counterexample:
This gives distinct roots , as you can verify. Andrew Bremner found two infinite families of solutions.
Can we take it a step further to degree with and ? Nobody knows. This is related to Stephen Smale’s Fourth Problem which we just blogged about.
Namely, the left-hand sides are straight-line programs of length . If there are distinct integer zeroes, this violates the conjecture .
A degree- polynomial with distinct integer roots and a short straight-line program is called a gem by Bernd Borchert, Pierre McKenzie, and Klaus Reinhardt.
They give -gems for up to , but skipping . See Borchert’s project page for more, including relevance to factoring.
Short Proofs and Interaction
Ken and I believe this issue of very short proofs highlights the real reason we prove theorems in mathematics.
A proof is not just a thing that we write out and then feel happy with the knowledge that something is proved. No. A proof must be something that can be understood by others.
To be understood it must be checkable. The above are extreme examples—you can just do the arithmetic. The existence of the proof is what was hard.
In some areas of computer science proofs are viewed in a different way. One area where I hear statements like “the proof is long and boring” is cryptographic protocols.
That some proofs of protocols are tedious is exactly what I do not like about them. I do not trust a long and boring proof, exactly because it is unlikely to be checked by others.
Of course protocols themselves are often proofs, of knowledge or identity or privilege or authority. The individual steps required of the user can be short.
The idea of interaction takes proofs beyond . The interaction can be short, or have short rounds. Still, the proof that it is a proof can be long.
Even for problems like factoring, interaction can shorten the proof that one has a proof. Suppose I have a long proof of an efficient algorithm. What can I do?
I can say, “Tweet me a number.” Using ASCII for base 128, a 1,024-bit RSA modulus can fit into 140 characters. Then I tweet back and you verify .
With interaction you can’t accuse me of pre-computing results or exploiting holes like Arjen Lenstra’s project. This is a short proof of my proof.
Most protocols cannot self-prove this way because you have to prove security against possible attacks. But there as in math, it’s good to ask how far short proofs can go.
Could there be a very short proof of your favorite open problem? Can we make more proofs like tweets?
Is a post easier to read with Tweet-length paragraphs, sometimes with equations in-between, each giving one idea? Or our usual longer ones?
End NoteWe add our congratulations to Leonid Levin, himself known for very short papers, on his 2012 Knuth Prize. Ken heard his lecture at FOCS this past Monday—here is a nice post by Thomas Vidick on it.