TOPICS 
The Kreisel conjecture is a conjecture in proof theory that postulates that, if 
is a formula in the language of arithmetic for which there exists a nonnegative integer 
such that, for every nonnegative integer 
, Peano arithmetic proves 
in at most 
steps, then Peano arithmetic proves its universal closure, 
.
A special case of the conjecture was proven true by M. Baaz in 1988 (Baaz and Pudlák 1993).
Portions of this entry contributed by Lorenzo Sauras-Altuzarra
." In Arithmetic, Proof Theory, and Computational Complexity, Papers from the Conference Held in Prague, July 2-5, 1991 (Ed. P. Clote and J. Krajiček). New York: Oxford University Press, pp. 30-60, 1993.Dawson, J. "The Gödel Incompleteness Theorem from a Length of Proof Perspective." Amer. Math. Monthly 86, 740-747, 1979.Kreisel, G. "On the Interpretation of Nonfinitistic Proofs, II." J. Sym. Logic 17, 43-58, 1952.Santos, P. G. and Kahle, R. "Variants of Kreisel's Conjecture on a New Notion of Provability." Bull. Sym. Logic 24, 337-350, 2021.Sauras-Altuzarra, Lorenzo and Weisstein, Eric W. "Kreisel Conjecture." From MathWorld--A Wolfram Resource. https://mathworld.wolfram.com/KreiselConjecture.html