The shortest known unsolved proposition

It was about 150 years ago that formal logic fused into mathematics. The language univerally used today is that of predicate logic in a form similar to the one introduced by Gottlob Frege. It can savely be said that without his monumental work, die Begriffsschrift, we wouldn't have computers already. This is because Alan Turings work on computation is an answer to David Hilberts Entscheidungsproblem, which relies on Freges logic. But this is the topic of an entirely different post.

Today we have a whole array of proper formalizations of concepts that have been worked with for hundrets of years. A major such theory is Peano Arithmetic, named after Giuseppe Peano and based on the Peano axioms.

The base of the language forms a symbol usually denoted by "0" and another one denoted by "S". The intended interpretation is that 0 denotes a natural number and Sn the "successor" of n, whenever n is a natural number. So for example, this implies that S0 is a number, and so is SS0. You may think of all those expressions as the number that's given by the amount of S's in it. Thus SSSSS0 represents the number 5. Later we introduce a binary operation "+" recursively. Then Sn may be written in a more elaborate way, as n+1. The same spiel goes for multiplication. One of the rules is then, for example

a + Sa = S(a+b)

This enables us to formalize and then prove, for example

3+4 = (3+3)+1

(image source)

The computer scientist Bauer had a program running in recent year, which studied short expressions in that language, and many others. The shortest one that's not solved for being true or false is the following.

∀a. ∃b. ∀x. ∀y. (a+b)·(a+b) != SS((SSx)·(SSy))

Here a,b,x and y denote any number and ∀ and ∃ should be read "for all" and "there exists".

Thus, roughly,

there are infinite numbers b, so that b squared minus 2 isn't for the form x·y

In other words, there are infinite primes p of the form p=b^2-2.

This makes the above claim the shortest unresolved problem.