Hilbert's Twenty-Fourth Problem.

For almost a century, a treasure lay hidden in a library in Germany, hidden until a remarkable discovery was made. Indeed, for most of the twentieth century, all of science thought that Hilbert had posed twenty-three problems, and no others. In the mid-1990s, however, as a result of a thorough reading of Hilbert's files, a twenty-fourth problem was found (in a notebook, in file Cod. ms. D. Hilbert 600:3), a problem that might have a profound effect on research. This newly discovered problem focuses on the finding of simpler proofs and criteria for measuring simplicity. A proof may be simpler than previously known in one or more ways that include length, size (measured in terms of the total symbol count), and term structure. A simpler proof not only is more appealing aesthetically (and has fascinated masters of logic including C. A. Meredith, A. Prior, and I. Thomas) but is relevant to practical applications such as circuit design and program synthesis. This article presents Hilbert's twenty-fourth problem, discusses its relation to certain studies in automated reasoning, and offers researchers with varying interests the challenge of addressing this newly discovered problem. In particular, we include open questions to be attacked, questions that (in different ways and with diverse proof refinements as the focus) may prove of substantial interest to mathematicians, to logicians, and (perhaps in a slightly different manner) to those researchers primarily concerned with automated reasoning. [ABSTRACT FROM AUTHOR]