1. Hilbert's note on his 24th problem
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 [2–4].
(a) The textThe short paragraph reads in German as follows: Als 24stes Problem in meinem Pariser Vortrag wollte ich die Frage stellen: Kriterien für die Einfachheit bez. Beweis der grössten Einfachheit von gewissen Beweisen führen. Ueberhaupt eine Theorie der Beweismethoden in der Mathematik entwickeln. Es kann doch bei gegebenen Voraussetzungen nur einen einfachsten Beweis geben. Ueberhaupt, wenn man für einen Satz 2 Beweise hat, so muss man nicht eher ruhen, als bis man sie beide aufeinander zurückgeführt hat oder genau erkannt hat, welche verschiedenen Voraussetzungen (und Hilfsmittel) bei den Beweisen benutzt werden: Wenn man 2 Wege hat, so muss man nicht bloss diese Wege gehen oder neue suchen, sondern dann das ganze zwischen den beiden Wegen liegende Gebiet erforschen. Ansätze, die Einfachheit der Beweise zu beurteilen, bieten meine Untersuchungen über Syzygien und Syzygien zwischen Syzygien. Die Benutzung oder Kenntnisse einer Syzygie vereinfacht den Beweis, dass eine gewisse Identität richtig ist, erheblich. Da jeder Process des Addierens Anwendung des commutativen Gesetzes der Addition ist—dies immer geometrischen Sätzen oder logischen Schlüssen entspricht, so kann man diese zählen und z. B. beim Beweis bestimmter Sätze in der Elementargeometrie (Pythagoras oder über merkwürdige Punkte im Dreieck) sehr wohl entscheiden, welches der einfachste Beweis ist. (figure 1).
Figure 1.Copy from Hilbert's notebook [5, Heft 3, p. 25f]. We are grateful to the Niedersächsische Staats- und Universitätbibliothek Göttingen for permission to reproduce it here. (Online version in colour.)
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.
(b) Historical tracesHilbert did not include this problem in the list of the now famous 23 problems from the International Congress of Mathematicians in Paris in 1900. We have no indications for his motives, and it would be pure speculation to discuss such possible motives.
There are two (very thin) threads of the 24th problem in Hilbert's work.1 The published version2 of his contribution to the International Congress of Mathematician contains some general considerations which address simplicity in relation to rigour [4]:3
Besides, it is an error to believe that rigor in the proof is the enemy of simplicity. On the contrary, we find it confirmed by numerous examples that the rigorous method is at the same time the simpler and the more easily comprehended. The very effort for rigor forces us to find out simpler methods of proof.
This claim is illustrated by referring to three examples concerning the theory of algebraic curves, power series and the calculus of variations. In these examples, he is far from any form of criteria for simplicity, but it is worth noting that they are all taken from core mathematics.
There is only one other instance where we found simplicity mentioned in David Hilbert's work, albeit at a very prominent place. In September 1917, Hilbert gave a talk at the Swiss Mathematical Society with the title Axiomatisches Denken (Axiomatic Thinking) [8,9]:
By closer inspection, we realize soon that the question of consistency for the whole numbers and sets is not an isolated one, but it belongs to a wide range of most difficult epistemological questions of specific mathematical colouring: I mention, to characterize briefly this area of questions, the problem of the principle solvability of any mathematical question, the problem of a posteriori controllability of the result of a mathematical investigation, further the question of a criterion for the simplicity of mathematical proofs, the question of the relation between contentness and formalismin mathematics and logic, and finally the problem of the decidablity of a mathematical question by a finite number of operations.
A ‘criterion for the simplicity of mathematical proofs’ is mentioned here only alongside several other questions. But one may note the slight change from the plural ‘criteria’ in his note of 1900 to the singular ‘criterion’ in 1917. In any case, the question of simplicity was never taken up by the Hilbert school.4
As possible exception, one could think of Saunders MacLane's PhD dissertation [11,12] written in Göttingen in 1934. Its title ‘Abgekürzte Beweise im Logikkalkul’ (Abbreviated Proofs in Logic Calculus) sounds like an echo of Hilbert's 24th problem. The content, however, does not address simplicity directly, but just brevity of (encoding of) proofs. Officially, MacLane was supervised by Hermann Weyl (Hilbert's successor in Göttingen), but one can safely assume that the de-facto supervisor was Paul Bernays,5 who could still have had reminiscences of the 24th problem in mind. But there is no written evidence to support such a link.
2. The challengesLooking today at Hilbert's 24th problem, which asks for a theory of the method of proof to give criteria of simplicity, one has to admit that we are still not yet there. The problem represents several challenges for philosophers of mathematics, logicians, and mathematicians which are under discussion, but without general solution.
(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]. On the other hand, reflections on mathematical practice [16] have expanded the discussion, even opening it up to empirical studies (see §3a(ii)). Any analysis of the simplicity of proof has, of course, first to specify its understanding of the notion of proof. Besides formal proofs, one should not neglect alternative concepts like ‘Proofs without Words’ and visual representations in general (see §3a(iii)). Also, proofs as given in school mathematics deserve a special attention (see §3a(iv)). In addition, any analysis of the simplicity of proof is subject to philosophical assumptions. And one may note that the question of simplicity of proof loses its significance when a theorem receives its sense only via its proof (and therefore, receives different senses by different proofs). This may apply to Wittgenstein, but also to proof-theoretic semantics [17,18].
(b) Mathematical proofIn 1900, Hilbert had clearly ordinary mathematical proofs in mind, rather than formal derivations in logical calculi. Thus, an appreciation of Hilbert's 24th problem requires to look at mathematical examples (see §3c(ii)). One should also take Hilbert's own suggestion into account and look to his ‘examination of syzygies and syzygies between syzygies’ (see §3c(ii)). Thiele identified a passage in Hilbert's unpublished lecture notes to which he could have referred [19, lectures XXXII–XXXIX]; see also [1, §11]. Today, we have a rather long list of well-studied examples of theorems with different proofs at hand; while in many instances, it is easy to judge whether one proof is simpler than another (or on which different conditions they depend), for now, it does not look like that these examples would give rise to general criteria. A standard reference for such examples are the Proofs from THE BOOK collected by Aigner & Ziegler [20]. This book does not aim for simplicity in the proofs but rather for elegance. And one may agree with Inglis and Aberdein that ‘Beauty Is Not Simplicity’ [21]. But the collection of Aigner and Ziegler should still be the first benchmark for any theory of simplicity of mathematical proof.
(c) A theory of the method of proofHilbert 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.6 When mathematical proofs are represented by formal proofs, we may get a faithful translation. But neither does this imply that mathematical proofs ought to be formal proofs—see [24]—nor could we even expect that such a translation tells us something about the method of proof.
Avigad [25] observed that the standard models of formal deductions are not well-equipped to deal with methods of proofs. He suggests to take into account approaches from computer-assisted theorem proving—like tactics of the proof system Isabelle—to capture the concept of method. This gives a promising link to computer-assisted theorem proving, but one is still far from a theory which would allow to study simplicity in terms of method.7
(d) Proof structureDespite the mathematical character of Hilbert's 24th problem, it is also studied in terms of the logical structure of proofs, see, for instance, Hughes [27,28], Straßburger [29,30] (see also §3b(ii)) and Negri and von Plato [31] (see also §3b(i)), among others. They link the problem mainly with structural properties of formal calculi as studied in Gentzen-style proof theory.
These studies concentrate on aspects of simplicity within the logical representation of proofs. When Hilbert referred to the counting of proof processes, such a counting can, indeed, be best performed in logical calculi. But, 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.
Still, in very specific areas, as for instance semigroup theory, counting might be a reasonable measure (see §3b(iii)).
(e) Axiom systemsThe simplified claim ‘there can be but one simplest proof’ will surely be rejected by a majority of scholars but Hilbert was careful enough to qualify it by adding ‘under a given set of conditions’. It might still be doubtful whether ‘under a given set of conditions’, indeed, ‘there can be but one simplest proof’. But Hilbert at least made clear, that we have to identify this ‘given set of conditions’ for different proofs (of the same theorem). At least, the identification of different conditions can be seen as the result of an investigation of ‘the area lying between the two routes.’ And in modern terms, such conditions may correspond simply to different axiomatizations (non-logical axioms) of a certain field of mathematics.
In this direction Hilbert's 24th problem was studied by considering variations of (non-logical) axiom systems (e.g. for geometry, for algebra, etc.) which were compared with respect to simplicity of proofs. Here we may refer to the discussion of Pambuccian [33,34] and Alama [35] which gives progressively improved axiomatizations for (hyperbolic) Geometry which allows one to identify various criteria of simplicity for the chosen axioms. The emphasis is, thus, on mathematical content (semantically, in the form of axioms), with little concern for formal calculi and notions defined therein (e.g. proof length). Thus, it focuses more on the axiom systems rather than the proofs themselves (see §3c(i)).
(f) Computer-assisted proof systemsAfter the publication of Hilbert's 24th problem by Rüdiger Thiele [1], various scholars took up the challenge of simplicity in one or the other form. This starts with Thiele himself who published a joint paper with Wos in relation to automated reasoning [36]. Wos & Pieper took the study of the problem in the context of automated reasoning further, linking it with elegance [37]. We already mentioned Avigad [25] who approaches the question of the method by concepts from interactive theorem proving. Such concepts were, of course, already under consideration before Hilbert's 24th problem was rediscovered, for example, proof plans as discussed in [38].
(g) Related questionsPurity of method was already addressed by Hilbert—most notably at the end of his famous book Grundlagen der Geometrie [39, p. 131]—as a particular objective of proof. Quite similiar to simplicity, we still do not have a satisfactory theory of purity at hand. But there are several studies concerning this notion, e.g. [40–43]. In [44], Arana addressed the question of how simplicity might be related to purity. It might not come as a surprise that there seems to be, in general, a trade-off between simplicity and purity of mathematical proofs.
Another question is whether simplicity can play a role in clarifying the notion of explanation in mathematics (see, for instance, [16,45], and §3a(ii)), even if such a clarification was—to our knowledge—not envisaged by Hilbert himself.
Finally, 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.
3. The contributions to this special issueIn the following, we review briefly the contributions to this special issue. It is the aim of this special issue to give a broad view of ongoing discussions concerning Hilbert's 24th problem and of questions related to it.
(a) ProofBefore analysing simplicity of proof, one has to have a clear specification of what a proof is and what purpose(s) it serves. Today we have a clear definition at hand of the notion of formal proof , not least through the work of the Hilbert school. Its adequacy for the informal notion of proof as used in mathematics, however, is far from being uncontroversial. Thus, the first group of papers in this special issues addresses more general questions concerning the notion of mathematical proof.
(i) Metaphor of proofNikolai Vavilov questions, indeed, the adequacy of formal proof to represent mathematical proof in his contribution Reshaping the metaphor of proof [46]. He goes even a step further and puts up to discussion the thesis that ‘a mathematical proof considered as a text proves nothing except the fact of existence of proofs.’
(ii) ExplanationAlison Pease, Andrew Aberdein & Ursula Martin, in their paper Explanation in mathematical conversations: an empirical investigation [47], confront simplicity with the objectives of a ‘good proof’. With empirical data, they discuss six conjectures about mathematical explanation. As a result, their empirical methodology is suggested as a new and fruitful tool to investigate informal notions such as the simplicity of proof.
(iii) Spatial thinkingAlan 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.
(iv) School mathematicsHelena Rocha characterizes, in Mathematical proof: from mathematics to school mathematics [49], ‘the understanding of mathematical proof in school, its function and the meaning and relevance attributed to the notion of simple proof’. It is observed that, in school mathematics, the understanding of proof differs from the understanding in the mathematical research community and, therefore, also the notion of simplicity of proof may be treated differently in school.
(b) Proof structureIt appears that proof theory, as conceived by the Hilbert school in the 1920s is not the ‘theory of the method of proof’ which Hilbert had envisaged in his 24th problem. It plays, however, an important role in the clarification of the notions around any concept of proof. In particular, it gives us a handle on the formal structure of proof.
(i) Proof theorySara Negri & Jan von Plato used prominently the expression Hilbert's last problem in the subtitle for their book on Proof analysis [31]. In their contribution From mathematical axioms to mathematical rules of proof: recent developments in proof analysis [50] they discuss examples of Gentzen-style proof theory which address the general part of Hilbert's 24th problem concerning a theory of proof methods in mathematics.
(ii) Proof identityLutz Straßburger focuses on the particular problem of proof identity which clearly relates to simplicity. In his paper, The problem of proof identity, and why computer scientists should care about Hilbert's 24th problem [51], ‘4 objectives that a satisfactory notion of proof identity should obey’ are formulated, and the problem is discussed in the context of Hughes's notion of combinatorial proofs [27].
(iii) Proof simplificationMichael 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.
(c) Mathematical proofsWhen stating his 24th problem, Hilbert had clearly informal proofs of mathematical theorems in mind, rather than proofs of, let us say, logical tautologies. Therefore, it is particularly interesting to look to examples of Mathematics, including Geometry, Set Theory, and—as Hilbert himself mentioned it—the theory of Syzygies.
(i) Use of axiomsVictor Pambuccian, in his contribution Prolegomena to any theory of proof simplicity [53], draws the attention to the choice of axioms which are used to prove a particular theorem. Using examples from Geometry, he discusses how the number of uses of an axiom may serve as a measurement for simplicity; but, of course, only after a fixed set of axioms is already chosen.
(ii) Variations of proofsWilfried Sieg analyses in The Cantor–Bernstein Theorem: how many proofs? [54] seemingly different proofs of the Cantor–Bernstein Theorem and formalizes their core in Zermelo–Fraenkel set theory with the conclusion that ‘there is essentially one proof that comes in two variants due to Dedekind and Zermelo, respectively.’
(iii) SyzygiesAntónio Malheiro and José Francisco Reis, in Identification of proofs via Syzygies [55], follow the suggestion of Hilbert and look to the question of simplicity of proofs in the context of syzygies. The modern theory of Gröbner Bases helps, indeed, to investigate examples of simplifications of polynomials which Hilbert might have had in mind as models for simplifications of proofs.
Data accessibilityThis article has no additional data.
Competing interestsWe declare we have no competing interests.
FundingThis work is partially supported by University Postgraduate Award and the International Postgraduate Tuition Award by the University of Wollongong (Australia) and by the Portuguese Science Foundation, FCT, through the projects UID/MAT/00297/2019 (Centro de Matemática e Aplicações) and PTDC/MHC-FIL/2583/2014 (Hilbert's 24th Problem).
Footnotes1 We follow here the presentation of [6] where one can find a more detailed discussion of these threads.
2 It his talk, Hilbert didn't read the full paper and presented only 10 of the 23 problems explicitly, see [7, p. 68].
3 See also the discussion in [1, § 5]. It is worth noting that this relation was included by Charlotte Angas Scott in her report of Hilbert's oral presentation in Paris: ‘in seeking this rigor we may find simplicity.’ [7, p. 68].
4 Thiele, however, observed that Hilbert included the problem of simplicity in an index for his notebooks [5, Heft 3, inserted page] prepared at the end of his life [1, p. 7]. And, when Bernays wrote in 1967 an encyclopaedia entry for ‘David Hilbert’ [10, p. 500], he clearly copied from the above mentioned passage, mentioning also the question ‘of finding a standard of simplicity for mathematical proofs’.
5 See MacLane's recollections in [13].
6 See Gentzen ([22, p. 237], English translation of [23]): ‘A foremost characteristic of Hilbert's point of view seems to me to be the endeavour to withdraw the problem of the foundations of mathematics from philosophy and to tackle it as far as in any way possible with methods proper to mathematics.’
7 In [26, §6.1], the modularity of method is addressed as one task.
One contribution of 11 to a theme issue ‘The notion of ‘simple proof’ - Hilbert's 24th problem’.
Full issue here.
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 [2–4].
(a) The textThe short paragraph reads in German as follows: Als 24stes Problem in meinem Pariser Vortrag wollte ich die Frage stellen: Kriterien für die Einfachheit bez. Beweis der grössten Einfachheit von gewissen Beweisen führen. Ueberhaupt eine Theorie der Beweismethoden in der Mathematik entwickeln. Es kann doch bei gegebenen Voraussetzungen nur einen einfachsten Beweis geben. Ueberhaupt, wenn man für einen Satz 2 Beweise hat, so muss man nicht eher ruhen, als bis man sie beide aufeinander zurückgeführt hat oder genau erkannt hat, welche verschiedenen Voraussetzungen (und Hilfsmittel) bei den Beweisen benutzt werden: Wenn man 2 Wege hat, so muss man nicht bloss diese Wege gehen oder neue suchen, sondern dann das ganze zwischen den beiden Wegen liegende Gebiet erforschen. Ansätze, die Einfachheit der Beweise zu beurteilen, bieten meine Untersuchungen über Syzygien und Syzygien zwischen Syzygien. Die Benutzung oder Kenntnisse einer Syzygie vereinfacht den Beweis, dass eine gewisse Identität richtig ist, erheblich. Da jeder Process des Addierens Anwendung des commutativen Gesetzes der Addition ist—dies immer geometrischen Sätzen oder logischen Schlüssen entspricht, so kann man diese zählen und z. B. beim Beweis bestimmter Sätze in der Elementargeometrie (Pythagoras oder über merkwürdige Punkte im Dreieck) sehr wohl entscheiden, welches der einfachste Beweis ist. (figure 1).
Figure 1.Copy from Hilbert's notebook [5, Heft 3, p. 25f]. We are grateful to the Niedersächsische Staats- und Universitätbibliothek Göttingen for permission to reproduce it here. (Online version in colour.)
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.
(b) Historical tracesHilbert did not include this problem in the list of the now famous 23 problems from the International Congress of Mathematicians in Paris in 1900. We have no indications for his motives, and it would be pure speculation to discuss such possible motives.
There are two (very thin) threads of the 24th problem in Hilbert's work.1 The published version2 of his contribution to the International Congress of Mathematician contains some general considerations which address simplicity in relation to rigour [4]:3
Besides, it is an error to believe that rigor in the proof is the enemy of simplicity. On the contrary, we find it confirmed by numerous examples that the rigorous method is at the same time the simpler and the more easily comprehended. The very effort for rigor forces us to find out simpler methods of proof.
This claim is illustrated by referring to three examples concerning the theory of algebraic curves, power series and the calculus of variations. In these examples, he is far from any form of criteria for simplicity, but it is worth noting that they are all taken from core mathematics.
There is only one other instance where we found simplicity mentioned in David Hilbert's work, albeit at a very prominent place. In September 1917, Hilbert gave a talk at the Swiss Mathematical Society with the title Axiomatisches Denken (Axiomatic Thinking) [8,9]:
By closer inspection, we realize soon that the question of consistency for the whole numbers and sets is not an isolated one, but it belongs to a wide range of most difficult epistemological questions of specific mathematical colouring: I mention, to characterize briefly this area of questions, the problem of the principle solvability of any mathematical question, the problem of a posteriori controllability of the result of a mathematical investigation, further the question of a criterion for the simplicity of mathematical proofs, the question of the relation between contentness and formalismin mathematics and logic, and finally the problem of the decidablity of a mathematical question by a finite number of operations.
A ‘criterion for the simplicity of mathematical proofs’ is mentioned here only alongside several other questions. But one may note the slight change from the plural ‘criteria’ in his note of 1900 to the singular ‘criterion’ in 1917. In any case, the question of simplicity was never taken up by the Hilbert school.4
As possible exception, one could think of Saunders MacLane's PhD dissertation [11,12] written in Göttingen in 1934. Its title ‘Abgekürzte Beweise im Logikkalkul’ (Abbreviated Proofs in Logic Calculus) sounds like an echo of Hilbert's 24th problem. The content, however, does not address simplicity directly, but just brevity of (encoding of) proofs. Officially, MacLane was supervised by Hermann Weyl (Hilbert's successor in Göttingen), but one can safely assume that the de-facto supervisor was Paul Bernays,5 who could still have had reminiscences of the 24th problem in mind. But there is no written evidence to support such a link.
2. The challengesLooking today at Hilbert's 24th problem, which asks for a theory of the method of proof to give criteria of simplicity, one has to admit that we are still not yet there. The problem represents several challenges for philosophers of mathematics, logicians, and mathematicians which are under discussion, but without general solution.
(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]. On the other hand, reflections on mathematical practice [16] have expanded the discussion, even opening it up to empirical studies (see §3a(ii)). Any analysis of the simplicity of proof has, of course, first to specify its understanding of the notion of proof. Besides formal proofs, one should not neglect alternative concepts like ‘Proofs without Words’ and visual representations in general (see §3a(iii)). Also, proofs as given in school mathematics deserve a special attention (see §3a(iv)). In addition, any analysis of the simplicity of proof is subject to philosophical assumptions. And one may note that the question of simplicity of proof loses its significance when a theorem receives its sense only via its proof (and therefore, receives different senses by different proofs). This may apply to Wittgenstein, but also to proof-theoretic semantics [17,18].
(b) Mathematical proofIn 1900, Hilbert had clearly ordinary mathematical proofs in mind, rather than formal derivations in logical calculi. Thus, an appreciation of Hilbert's 24th problem requires to look at mathematical examples (see §3c(ii)). One should also take Hilbert's own suggestion into account and look to his ‘examination of syzygies and syzygies between syzygies’ (see §3c(ii)). Thiele identified a passage in Hilbert's unpublished lecture notes to which he could have referred [19, lectures XXXII–XXXIX]; see also [1, §11]. Today, we have a rather long list of well-studied examples of theorems with different proofs at hand; while in many instances, it is easy to judge whether one proof is simpler than another (or on which different conditions they depend), for now, it does not look like that these examples would give rise to general criteria. A standard reference for such examples are the Proofs from THE BOOK collected by Aigner & Ziegler [20]. This book does not aim for simplicity in the proofs but rather for elegance. And one may agree with Inglis and Aberdein that ‘Beauty Is Not Simplicity’ [21]. But the collection of Aigner and Ziegler should still be the first benchmark for any theory of simplicity of mathematical proof.
(c) A theory of the method of proofHilbert 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.6 When mathematical proofs are represented by formal proofs, we may get a faithful translation. But neither does this imply that mathematical proofs ought to be formal proofs—see [24]—nor could we even expect that such a translation tells us something about the method of proof.
Avigad [25] observed that the standard models of formal deductions are not well-equipped to deal with methods of proofs. He suggests to take into account approaches from computer-assisted theorem proving—like tactics of the proof system Isabelle—to capture the concept of method. This gives a promising link to computer-assisted theorem proving, but one is still far from a theory which would allow to study simplicity in terms of method.7
(d) Proof structureDespite the mathematical character of Hilbert's 24th problem, it is also studied in terms of the logical structure of proofs, see, for instance, Hughes [27,28], Straßburger [29,30] (see also §3b(ii)) and Negri and von Plato [31] (see also §3b(i)), among others. They link the problem mainly with structural properties of formal calculi as studied in Gentzen-style proof theory.
These studies concentrate on aspects of simplicity within the logical representation of proofs. When Hilbert referred to the counting of proof processes, such a counting can, indeed, be best performed in logical calculi. But, 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.
Still, in very specific areas, as for instance semigroup theory, counting might be a reasonable measure (see §3b(iii)).
(e) Axiom systemsThe simplified claim ‘there can be but one simplest proof’ will surely be rejected by a majority of scholars but Hilbert was careful enough to qualify it by adding ‘under a given set of conditions’. It might still be doubtful whether ‘under a given set of conditions’, indeed, ‘there can be but one simplest proof’. But Hilbert at least made clear, that we have to identify this ‘given set of conditions’ for different proofs (of the same theorem). At least, the identification of different conditions can be seen as the result of an investigation of ‘the area lying between the two routes.’ And in modern terms, such conditions may correspond simply to different axiomatizations (non-logical axioms) of a certain field of mathematics.
In this direction Hilbert's 24th problem was studied by considering variations of (non-logical) axiom systems (e.g. for geometry, for algebra, etc.) which were compared with respect to simplicity of proofs. Here we may refer to the discussion of Pambuccian [33,34] and Alama [35] which gives progressively improved axiomatizations for (hyperbolic) Geometry which allows one to identify various criteria of simplicity for the chosen axioms. The emphasis is, thus, on mathematical content (semantically, in the form of axioms), with little concern for formal calculi and notions defined therein (e.g. proof length). Thus, it focuses more on the axiom systems rather than the proofs themselves (see §3c(i)).
(f) Computer-assisted proof systemsAfter the publication of Hilbert's 24th problem by Rüdiger Thiele [1], various scholars took up the challenge of simplicity in one or the other form. This starts with Thiele himself who published a joint paper with Wos in relation to automated reasoning [36]. Wos & Pieper took the study of the problem in the context of automated reasoning further, linking it with elegance [37]. We already mentioned Avigad [25] who approaches the question of the method by concepts from interactive theorem proving. Such concepts were, of course, already under consideration before Hilbert's 24th problem was rediscovered, for example, proof plans as discussed in [38].
(g) Related questionsPurity of method was already addressed by Hilbert—most notably at the end of his famous book Grundlagen der Geometrie [39, p. 131]—as a particular objective of proof. Quite similiar to simplicity, we still do not have a satisfactory theory of purity at hand. But there are several studies concerning this notion, e.g. [40–43]. In [44], Arana addressed the question of how simplicity might be related to purity. It might not come as a surprise that there seems to be, in general, a trade-off between simplicity and purity of mathematical proofs.
Another question is whether simplicity can play a role in clarifying the notion of explanation in mathematics (see, for instance, [16,45], and §3a(ii)), even if such a clarification was—to our knowledge—not envisaged by Hilbert himself.
Finally, 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.
3. The contributions to this special issueIn the following, we review briefly the contributions to this special issue. It is the aim of this special issue to give a broad view of ongoing discussions concerning Hilbert's 24th problem and of questions related to it.
(a) ProofBefore analysing simplicity of proof, one has to have a clear specification of what a proof is and what purpose(s) it serves. Today we have a clear definition at hand of the notion of formal proof , not least through the work of the Hilbert school. Its adequacy for the informal notion of proof as used in mathematics, however, is far from being uncontroversial. Thus, the first group of papers in this special issues addresses more general questions concerning the notion of mathematical proof.
(i) Metaphor of proofNikolai Vavilov questions, indeed, the adequacy of formal proof to represent mathematical proof in his contribution Reshaping the metaphor of proof [46]. He goes even a step further and puts up to discussion the thesis that ‘a mathematical proof considered as a text proves nothing except the fact of existence of proofs.’
(ii) ExplanationAlison Pease, Andrew Aberdein & Ursula Martin, in their paper Explanation in mathematical conversations: an empirical investigation [47], confront simplicity with the objectives of a ‘good proof’. With empirical data, they discuss six conjectures about mathematical explanation. As a result, their empirical methodology is suggested as a new and fruitful tool to investigate informal notions such as the simplicity of proof.
(iii) Spatial thinkingAlan 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.
(iv) School mathematicsHelena Rocha characterizes, in Mathematical proof: from mathematics to school mathematics [49], ‘the understanding of mathematical proof in school, its function and the meaning and relevance attributed to the notion of simple proof’. It is observed that, in school mathematics, the understanding of proof differs from the understanding in the mathematical research community and, therefore, also the notion of simplicity of proof may be treated differently in school.
(b) Proof structureIt appears that proof theory, as conceived by the Hilbert school in the 1920s is not the ‘theory of the method of proof’ which Hilbert had envisaged in his 24th problem. It plays, however, an important role in the clarification of the notions around any concept of proof. In particular, it gives us a handle on the formal structure of proof.
(i) Proof theorySara Negri & Jan von Plato used prominently the expression Hilbert's last problem in the subtitle for their book on Proof analysis [31]. In their contribution From mathematical axioms to mathematical rules of proof: recent developments in proof analysis [50] they discuss examples of Gentzen-style proof theory which address the general part of Hilbert's 24th problem concerning a theory of proof methods in mathematics.
(ii) Proof identityLutz Straßburger focuses on the particular problem of proof identity which clearly relates to simplicity. In his paper, The problem of proof identity, and why computer scientists should care about Hilbert's 24th problem [51], ‘4 objectives that a satisfactory notion of proof identity should obey’ are formulated, and the problem is discussed in the context of Hughes's notion of combinatorial proofs [27].
(iii) Proof simplificationMichael 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.
(c) Mathematical proofsWhen stating his 24th problem, Hilbert had clearly informal proofs of mathematical theorems in mind, rather than proofs of, let us say, logical tautologies. Therefore, it is particularly interesting to look to examples of Mathematics, including Geometry, Set Theory, and—as Hilbert himself mentioned it—the theory of Syzygies.
(i) Use of axiomsVictor Pambuccian, in his contribution Prolegomena to any theory of proof simplicity [53], draws the attention to the choice of axioms which are used to prove a particular theorem. Using examples from Geometry, he discusses how the number of uses of an axiom may serve as a measurement for simplicity; but, of course, only after a fixed set of axioms is already chosen.
(ii) Variations of proofsWilfried Sieg analyses in The Cantor–Bernstein Theorem: how many proofs? [54] seemingly different proofs of the Cantor–Bernstein Theorem and formalizes their core in Zermelo–Fraenkel set theory with the conclusion that ‘there is essentially one proof that comes in two variants due to Dedekind and Zermelo, respectively.’
(iii) SyzygiesAntónio Malheiro and José Francisco Reis, in Identification of proofs via Syzygies [55], follow the suggestion of Hilbert and look to the question of simplicity of proofs in the context of syzygies. The modern theory of Gröbner Bases helps, indeed, to investigate examples of simplifications of polynomials which Hilbert might have had in mind as models for simplifications of proofs.
Data accessibilityThis article has no additional data.
Competing interestsWe declare we have no competing interests.
FundingThis work is partially supported by University Postgraduate Award and the International Postgraduate Tuition Award by the University of Wollongong (Australia) and by the Portuguese Science Foundation, FCT, through the projects UID/MAT/00297/2019 (Centro de Matemática e Aplicações) and PTDC/MHC-FIL/2583/2014 (Hilbert's 24th Problem).
Footnotes1 We follow here the presentation of [6] where one can find a more detailed discussion of these threads.
2 It his talk, Hilbert didn't read the full paper and presented only 10 of the 23 problems explicitly, see [7, p. 68].
3 See also the discussion in [1, § 5]. It is worth noting that this relation was included by Charlotte Angas Scott in her report of Hilbert's oral presentation in Paris: ‘in seeking this rigor we may find simplicity.’ [7, p. 68].
4 Thiele, however, observed that Hilbert included the problem of simplicity in an index for his notebooks [5, Heft 3, inserted page] prepared at the end of his life [1, p. 7]. And, when Bernays wrote in 1967 an encyclopaedia entry for ‘David Hilbert’ [10, p. 500], he clearly copied from the above mentioned passage, mentioning also the question ‘of finding a standard of simplicity for mathematical proofs’.
5 See MacLane's recollections in [13].
6 See Gentzen ([22, p. 237], English translation of [23]): ‘A foremost characteristic of Hilbert's point of view seems to me to be the endeavour to withdraw the problem of the foundations of mathematics from philosophy and to tackle it as far as in any way possible with methods proper to mathematics.’
7 In [26, §6.1], the modularity of method is addressed as one task.
One contribution of 11 to a theme issue ‘The notion of ‘simple proof’ - Hilbert's 24th problem’.
Full issue here.
RSS Feed
