Hilbert's twenty-fourth problem
Hilbert's twenty-fourth problem is a mathematical problem that was not published as part of the list of 23 problems known as Hilbert's problems but was included in David Hilbert's original notes. The problem asks for a criterion of simplicity in mathematical proofs and the development of a proof theory with the power to prove that a given proof is the simplest possible.
The 24th problem was rediscovered by German historian in 2000, noting that Hilbert did not include the 24th problem in the lecture presenting Hilbert's problems or any published texts. Hilbert's friends and fellow mathematicians Adolf Hurwitz and Hermann Minkowski were closely involved in the project but did not have any knowledge of this problem.
This is the full text from Hilbert's notes given in Rüdiger Thiele's paper. The section was translated by Rüdiger Thiele.
In 2002, Thiele and Larry Wos published an article on Hilbert's twenty-four problem with a discussion about its relation to various issues in automated reasoning, logic, and mathematics.