1

In computer science there is a concept of string complexity, called kolmogorov complexity, which basically says that the complexity of a string is the length of the smallest program that prints that string. If we take the formal proofs of mathematical theorems as strings, how do we know that they are actually optimized? That is, how do we know that (for example) a 10-page proof could not be compressed into 3 pages using perhaps another approach and producing a string of less complexity?

I believe that in any case what matters in mathematics is not so much to produce the shortest possible proof but to prove a theorem period. I was curious, however, to know if there are methods to understand if a proof can be simplified or not and how much mathematicians take it into account.

Yamar69
  • 203

1 Answers1

1

I think that the issue is that the Kolmogorov complexity is defined for a fixed predetermined programming language.

Therefore it does not make any sense to define an optimized proof. I could create a program language that outputs the four color theorem proof when you input nothing. Hence the Kolmogorov complexity is $0$ (for this specific language).

This is exagerate, but you should have a look at code-golf SE site, where you'll find plenty example of such challenge (e.g. example). The game are played up to the byte.

Thomas Lesgourgues
  • 4,685