Source: Royal Society Publishing, Jan 2019

In 2000, Rüdiger Thiele [1] found in a notebook of David Hilbert, kept in Hilbert’s *Nachlass* at the University of Göttingen, a small note concerning a 24th problem. As Hilbert wrote, he had considered including this problem in his famous problem list for the International Congress of Mathematicians in Paris in 1900.

An English translation was given by Thiele as follows:

The 24th problem in my Paris lecture was to be: Criteria of simplicity, or proof of the greatest simplicity of certain proofs. Develop a theory of the method of proof in mathematics in general. Under a given set of conditions there can be but one simplest proof. Quite generally, if there are two proofs for a theorem, you must keep going until you have derived each from the other, or until it becomes quite evident what variant conditions (and aids) have been used in the two proofs. Given two routes, it is not right to take either of these two or to look for a third; it is necessary to investigate the area lying between the two routes. Attempts at judging the simplicity of a proof are in my examination of syzygies and syzygies between syzygies. The use or the knowledge of a syzygy simplifies in an essential way a proof that a certain identity is true. Because any process of addition [is] an application of the commutative law of addition etc. [and because] this always corresponds to geometric theorems or logical conclusions, one can count these [processes], and, for instance, in proving certain theorems of elementary geometry (the Pythagoras theorem, [theorems] on remarkable points of triangles), one can very well decide which of the proofs is the simplest.

#### (a) What is a proof?

Even the notion of mathematical proof is still a controversial issue (see §3a(i)). Its traditional understanding is, on the one hand, challenged by recent developments of computer-assisted proofs, notably in the context of ‘big proofs’, see, e.g. the collection of papers in [14] or [15].

Besides formal proofs, one should not neglect alternative concepts like ‘Proofs without Words’ and visual representations in general (see §3a(iii))

#### (c) A theory of the method of proof

Hilbert and his school developed in the 1920s proof theory as a new discipline in the emerging field of mathematical logic. This proof theory was conceived, first of all, to serve *Hilbert’s Programme*, the attempt to provide finitist consistency proofs of formalized mathematical theories. It succeeded, at least, in the aim of transforming mathematical proofs themselves into mathematical objects which can be studied by mathematical tools.

it is rather questionable whether length, relative to the specific proof system under consideration, would even be a good measure for simplicity. For the very example of *Pythagoras’ theorem*, mentioned by Hilbert, Loomis collected more than 350 different proofs [32], and it is more than doubtful that one would like to pick the shortest of all these proofs as the simplest.

Thiele [1, §9] draws our attention to the relation of simplicity to complexity. In the specific area of computational complexity, we are confronted with questions related to Hilbert’s 24th problem, for instance, by asking for a notion of the simplest algorithm.

Alan Cain, in Visual thinking and simplicity of proof [48], draws the attention to ‘how spatial thinking interacts with simplicity in [informal] proof’ by analysing some concrete examples of spatial proofs in mathematics in comparsion with non-spatial ones. It is argued that diagrams and spatial thinking can contribute to simplicity in a number of ways.

Michael Kinyon, in Proof simplification and automated theorem proving [52], gives a detailed analysis of a proof in algebra which can be simplified by an automated theorem prover using *length of proof* as one particular measure.