On short and long mathematical proofs

Susanna Figueiredo de Rezende will receive her doctoral degree in computer science from KTH Royal Institute of Technologyin 2019. Thanks to a grant from the Knut and Alice Wallenberg Foundation, she will hold a postdoctoral position with Professor Pavel Pudlák at the Institute of Mathematics of the Czech Academy of Sciences, Prague, Czech Republic.

Short proofs are adequate for some mathematical theorems, while others require longer and more complicated ones. Mathematicians prefer short and elegant proofs of beautiful theorems. There is also a practical aspect – a short proof that is easy to verify may be necessary, for example because it demonstrates that the control system in a nuclear power plant can never cause a meltdown.

De Rezende's research is about understanding why some mathematical theorems permit short proofs, while others seem to require proofs that are so long that even a computer cannot verify them. One example for which there does not seem to be a short proof is managing a list of 100 people, each of whom also has a list of friends. The question is whether it is possible to divide the people into twenty groups so that no one is in a group with one of their friends. If the answer is positive, a solution consisting of such a partition would be a short proof of the fact that it is possible. But if the answer is negative, it is not clear how to provide a proof of this fact.

One obvious way of solving the task is to write down all possible combinations for dividing the people into twenty groups, and show that none of them gives a valid solution.

However, there are 461925547044215873829002327767063134987973369022
4737295400769553540316688341714252515748587739178140524570560271 different ways to do this. Even a computer that checks a billion solutions per second would have to perform calculations for 10⁹⁰years – for much longer than the age of the entire universe.

So, is it possible to find a short and elegant proof that this task is impossible? Most researchers do not believe so, but no one knows for sure. This problem is one of the famous six millennium problems in mathematics, each of which has a 1 million dollar prize awaiting the solution.