The Shortest and Longest Proofs in Math

---

Learn for Math · Blog

The shortest proofs
and the longest.

This week I posted two Shorts that sit at opposite ends of mathematics. One is about a paper that is two words long. The other is about a proof so large that nobody could ever read it. Below I go through both, with a few small demos you can play with.

8 min readNumber theoryComputer proofs#learn4math

scroll down

Short 1

The shortest math paper ever is 2 words

1. In 1769 Euler guessed that a sum of $n$-th powers needs at least $n$ terms to make another $n$-th power.
2. In 1966 a computer search found just four fifth powers that add up to a fifth power.
3. You can check the last digit of that equation in your head.
4. In 2005 Conway and Soifer published a paper whose whole abstract is “$n^2+2$ can.”
5. Nobody knows yet whether $n^2+1$ is enough in general.

1769

Euler's sum of powers conjecture

Two cubes never add up to a cube. Euler thought the pattern goes further: to write an $n$-th power as a sum of $n$-th powers, you need at least $n$ of them.

$$a_1^{\,n} + a_2^{\,n} + \cdots + a_k^{\,n} = b^{\,n} \;\;\Longrightarrow\;\; k \ge n$$

$n = 3$

This case holds

The equation $a^3+b^3=c^3$ has no solution in positive whole numbers. Euler gave a proof of this case.

$n = 5$

Five terms needed?

Euler's guess says you need at least five fifth powers. For almost 200 years nobody could prove it or find a counterexample.

1966 · Lander and Parkin

Four fifth powers. Not five.

Leon Lander and Thomas Parkin ran a search on a CDC 6600, one of the fastest computers of the time, and found the equation below. Their paper is only a few lines long. One counterexample is enough to show a conjecture is false, so nothing more was needed.

$$27^5 + 84^5 + 110^5 + 133^5 = 144^5$$

Check it yourself

A quick mental check

The last-digit trick

For any whole number $n$, the number $n^5$ ends in the same digit as $n$. The reason is $n^5 \equiv n \pmod{10}$, which follows from Fermat's little theorem applied mod $2$ and mod $5$.

7

4

0

3

$7+4+0+3 = 14$ ends in $4$, and so does $144$.

Try your own number

This test can only catch a wrong equation. If an equation passes, that alone does not prove it is right.

2005 · Conway and Soifer

A paper with a two-word abstract

COVERING A TRIANGLE WITH TRIANGLES

$n^2+2$ can.

A triangle with side $n$ can be covered exactly by $n^2$ triangles of side $1$. Make the big triangle slightly larger, with side $n+\varepsilon$, and $n^2$ small triangles are no longer enough. So how many do you need?

Conway and Soifer showed that $n^2+2$ always works. Whether $n^2+1$ works is still open in general. Baek and Lee have since settled some special cases.

2 words, 200 TB

Now the other end: proofs that no person can read.

Short 2

This math proof is 200 terabytes long

1. 1976: a computer helped prove that four colours are enough for any map.
2. 1998: a computer helped prove that the pyramid stack is the densest way to pack oranges (the Kepler conjecture).
3. 2016: a colouring puzzle on whole numbers was shown to fail exactly at $7825$, with a proof of about 200 TB.
4. The problems: nobody can check these by hand, hardware can have bugs, and the proof doesn't explain why.
5. One fix is a proof assistant, where software checks every step.

1976 · Appel and Haken

Can you colour this map with 3 colours?

Tap a region to change its colour. Regions that share a border need different colours. The middle region touches all five outer ones, and the five outer regions form a ring of odd length, so they already need three colours between them.

Tap any region to start.

The Four Colour Theorem says four colours are always enough. Appel and Haken reduced the problem to about 1,900 configurations and checked them using more than 1,000 hours of computer time.

2016 · Heule, Kullmann and Marek

The Boolean Pythagorean triples problem

Colour every whole number red or blue so that no triple with $a^2+b^2=c^2$ is all one colour. You can do this for the numbers $1$ to $7824$. For $1$ to $7825$ it can't be done, and the computer proof of that is about 200 TB.

Try it with $1$ to $20$

Tap a number to switch between blank, red and blue.

Scale

How big are these proofs?

Two-word paperConway and Soifer, 2005

12 B

Pythagorean triplesHeule, Kullmann and Marek, 2016

200 TB

Schur number 5Heule, 2017

2 PB

00.5 PB1 PB1.5 PB2 PB

$10\times$the Schur proof compared with the triples proof

$\approx 10^{13}\times$the triples proof compared with the 12-byte paper, which is why that bar is only a thin mark

2,000+ yearsto read 200 TB at one 3 KB page per second, with no breaks

The bars use a linear scale. Here $1\,\text{TB} = 10^{12}$ bytes and $1\,\text{PB} = 10^{15}$ bytes.

The weak points

Three problems with computer proofs

1

No person can check it all

The referees who reviewed Hales's proof of the Kepler conjecture said they were 99% sure it was correct. In mathematics that is usually not enough.

2

Hardware can make mistakes

In 1994 Thomas Nicely noticed that the Pentium chip gave wrong answers for some divisions. He found it while computing Brun's constant.

$4195835 \div 3145727$

Correct

Faulty Pentium1.333739068902…

3

It shows that, not why

Checking a huge number of cases tells you a statement is true. It usually doesn't tell you the reason.

The fix

Letting software check the proof

Proof assistants such as Coq, Isabelle, HOL Light and Lean check every logical step against a small set of basic rules. Very large SAT proofs are checked by separate, much simpler programs.

1976 The Four Colour Theorem is proved with a computer.

1998 Hales announces a computer proof of the Kepler conjecture.

2005 Gonthier and Werner check the Four Colour Theorem in Coq.

2014 The Flyspeck project finishes a formal proof of Kepler, published in 2017.

2016–17 The triples problem and Schur number 5 are solved, each with a certificate that independent checkers can verify.

Further reading

References

1. L. J. Lander, T. R. Parkin, Counterexample to Euler's conjecture on sums of like powers, Bull. AMS 72 (1966), 1079.
2. J. H. Conway, A. Soifer, Covering a triangle with triangles, Amer. Math. Monthly 112 (2005), 78.
3. J. Baek, S. Lee, arXiv:2306.09533 (2023); Amer. Math. Monthly 132 (2025).
4. K. Appel, W. Haken, Every planar map is four colorable, Illinois J. Math. (1977).
5. G. Gonthier, Formal proof: the four-color theorem, Notices AMS 55 (2008).
6. T. Hales, A proof of the Kepler conjecture, Annals of Math. (2005); T. Hales et al., Forum of Math. Pi (2017).
7. M. Heule, O. Kullmann, V. Marek, Solving and verifying the Boolean Pythagorean triples problem via cube-and-conquer, SAT 2016.
8. M. Heule, Schur number five, AAAI 2018.
9. T. Nicely, Enumeration to $10^{14}$ of the twin primes and Brun's constant, Virginia J. Sci. (1995).

Learn for Math · If you enjoyed this, watch both Shorts and follow the channel. #learn4math