The Kreisel conjecture is a conjecture in proof theory that postulates that, if ϕ(x) is a formula in the language of arithmetic for which there exists a nonnegative integer k such that, for every nonnegative integer n, Peano arithmetic proves ϕ(n) in at most k steps, then Peano arithmetic proves its universal closure, for all x ϕ(x). A special case of the conjecture was proven true by M. Baaz in 1988.