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 ${\mathsf{NP}}$.

## Euler’s Example

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 ${n}$th power cannot be written as the sum of fewer than ${n}$ nontrivial powers for ${n \ge 3}$.

Leon Lander and Thomas Parkin used a computer to solve the problem for ${n=5}$ and found a counterexample. Here is their whole paper:

Note, if they had just sent the answer it would have been: $\displaystyle 27^5 + 84^5 +110^5 + 133^5 = 144^5.$

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 ${n=4}$ case. He showed that $\displaystyle (85v^{2}+484v-313)^{4} + (68v^{2}+586v+10)^{4} + (2u)^{4} = (357v^{2}-204v+363),$

where $\displaystyle u^{2} = 22030+28849v + 56158v^{2} + 36941v^{3} + 31790v^{4}.$

In 1988, Roger Frye found the smallest counterexample based on Elkies’ ideas: $\displaystyle 95800^{4} + 217519^{4} + 414560^{4} = 422481^{4}.$

## Gems

Note that ${x^2 - P^2 = (x+P)(x-P)}$ always has the integer roots ${\pm P}$, which are distinct when ${P \neq 0}$. And $\displaystyle (x^2 - P)^2 - Q^2 = (x^2 - a^2)(x^2 - b^2)$

is solvable in integers by ${P = 5}$, ${Q = 4}$, ${a = 1}$, ${b = 3}$ among many other possibilities.

That is, $\displaystyle (x^2 - 5)^2 - 4^2 = x^4 - 10x^2 + 9 = (x^2 - 1)(x^2 - 9)$

has four distinct integer roots in pairs ${\pm 1}$ and ${\pm 3}$.

Going from degree ${d = 4}$ to ${d = 8}$, we can solve $\displaystyle ((x^2 - P)^2 - Q)^2 - R^2 = (x^2 - a^2)(x^2 - b^2)(x^2 - c^2)(x^2 - d^2)$

with ${P = 85}$, ${Q= 4,176}$, and ${R = 2,880}$. These induce ${a = 1}$, ${b=7}$, ${c=11}$, and ${d=13}$, again giving ${d}$-many distinct integer roots.

Can we do this with ${d=16}$ for $\displaystyle (((x^2 - P)^2 - Q)^2 - R)^2 - S^2 = (x^2 - a^2)(x^2 - b^2)(x^2 - c^2)\cdots(x^2 - h^2)?$

There had been a conjecture—indeed, a claimed proof—of “no,” but Dominic Symes found an example—or counterexample: $\displaystyle \begin{array}{rcl} P &=& 67,405 \\ Q &=& 3,525,798,096 \\ R &=& 533,470,702,551,552,000 \\ S &=& 469,208,209,191,321,600. \end{array}$

This gives distinct roots ${\pm 11,\pm 77,\pm 101,\pm 131,\pm 343,\pm 353,\pm 359,\pm 367}$, as you can verify. Andrew Bremner found two infinite families of solutions.

Can we take it a step further to degree ${d = 32}$ with ${P,Q,R,S,T}$ and ${a,\dots,p}$? Nobody knows. This is related to Stephen Smale’s Fourth Problem which we just blogged about.

Namely, the left-hand sides ${f}$ are straight-line programs of length ${\tau(f) = 2\log_2 d}$. If there are ${Z(f) = d}$ distinct integer zeroes, this violates the conjecture ${\tau(f) \geq Z(f)^{\Omega(1)}}$.

A degree- ${d}$ polynomial ${f(x)}$ with ${d}$ distinct integer roots and a short straight-line program is called a gem by Bernd Borchert, Pierre McKenzie, and Klaus Reinhardt.

They give ${d}$-gems for ${d}$ up to ${55}$, but skipping ${d=32}$. 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 ${\mathsf{NP}}$. 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 ${N}$ can fit into 140 characters. Then I tweet back ${p,q}$ and you verify ${N = pq}$.

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.

## Open Problems

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 Note

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

[21519–>217,519]

1. October 26, 2012 5:21 pm

• October 26, 2012 9:56 pm

Thanks!

2. October 26, 2012 6:01 pm

I sympathize with much of what you write. However, I do not believe that every “interesting” theorem in CS or mathematics is amenable to a short and elegant proof. For instance, proofs of correctness for non-trivial programs or (cryptographic) protocols might need long proofs and perhaps we should accept this fact. What is boring/tedious is in the eye of the beholder and the import of the correctness proof for a cryptographic protocols might just be that the protocol works.

Aschbacher’s “Highly complex proofs and implications of such proofs” offers an interesting discussion of very long and complicated proofs in mathematics. Here are two excerpts:

“Conventional wisdom says the ideal mathematical proof should be short, simple
and elegant. However, there are now examples of very long, complicated proofs,
and as mathematics continues to mature, more examples are likely to appear.”

“My guess is that we will begin to encounter many more such problems,
theorems, and proofs in the near future. As a result we will need to re-examine
what constitutes a proof, and what constitutes a good proof. Elegance and
simplicity should remain important criteria in judging mathematics, but the
applicability and consequences of a result are also important, and sometimes
these criteria conflict. I believe that some fundamental theorems do not admit
simple elegant treatments, and the proofs of such theorems may of necessity be
long and complicated. Our standards of rigor and beauty must be sufficiently
broad and realistic to allow us to accept and appreciate such results and their
proofs. As mathematicians we will inevitably use such theorems when it is
necessary in the practice our trade; our philosophy and aesthetics should reflect
this reality.”

3. October 26, 2012 6:07 pm

Proof that n^{1/n} -> 1 as n -> oo:

By Bernoulii’s inequality, (1+n^{-1/2})^n >= 1+n^{1/2} > n^{1/2}.

Raising to the 2/n power,
n^{1/n} < (1+n^{-1/2})^2 = 1 + 2n^{-1/2}+n^{-1} < 1 + 3 n^{-1/2}.

q e d

4. October 27, 2012 5:13 am

In the view of theorems as a shortcut statements in the different proves, long proves are actually good, when used many times, similar to subroutines in programming. They loose aesthetics, but should be practical.

5. October 29, 2012 11:51 am

Two appreciations of tweet-length proofs from Michael Spivak’s well-regarded Calculus on Manifolds: (1965)

(page ix): “There are good reasons why theorems should all be easy and the definitions hard … Definitions serve a twofold purpose: they are rigorous replacements for vague notions, and machinery for elegant proofs.”

(page 103): “Stokes’ Theorem shares three important attributes with many fully evolved major theorems: (1) It is trivial. (2) It is trivial because the terms appearing in it have been properly defined. (3) It has significant consequences.”

Spivak’s remarks find an apt counterpoint in Saunders Mac Lane’s survey article Hamiltonian mechanics and geometry (1970):

“Often a book on physics will contrast a mathematical presentation of an idea (using coordinates) with a physical presentation (not using coordinates); in such cases the contrast is really between two mathematical presentations, one with coordinates and one coordinate-free.”

Theorems having “trivial” proofs that are founded upon multiple levels of carefully crafted abstraction are emerging (it seems to me) as a hallmark of a 21st century STEM enterprise in which mathematical naturality is appreciated as dual to experimental physicality.

• October 29, 2012 3:28 pm

But then John, one needs exponentially many definitions if P!=NP ;), still unreadable.

• October 29, 2012 4:44 pm

mkatkov says  “But then John, one needs exponentially many  definitions  oracles if P!=NP” 😉

To some folks (including me) oracles seem intrinsically more mysterious than definitions! 🙂

6. October 30, 2012 1:20 pm

Is a counterexample really the same as a proof? Or in other words: I guess I’m more impressed by a short proof of a “for all” statement than I am of a “there exists” statement.

• 