L. Wos and R. Thiele, "Hilbert's New Problem," Preprint ANL/MCS-P959-0102, January 2002. [pdf]
Throughout the twentieth century, the worlds of logic and mathematics were well aware of Hilbert's twenty-three problems and the challenge they offered. Although not known until very recently, there existed yet one more challenge offered by Hilbert, his twenty-fourth problem. This problem focuses on finding simpler proofs, on the criteria for measuring simplicity, and on the "development of a theory of the method of proof in mathematics in general". Of the three themes of Hilbert's twenty-fourth problem, the first two are central to this article. We visit various areas of logic, showing that some of the studies of the masters are indeed strongly connected to this newly discovered problem. We also demonstrate that the use of an automated reasoning program (specifically, W. McCune's OTTER) enables one to address this challenging problem. We offer questions that remain unanswered.