¿Puedes predecir la cantidad de pasos necesarios para resolver un enunciado matemático?

¿Puedes predecir la cantidad de pasos necesarios para resolver un enunciado matemático?

Voy a interpretar esto como: dada una declaración matemática T, ¿podemos predecir la longitud de la prueba de T (si hay una), o la prueba de ~ T (si hay una)?

Podemos dar un límite superior en la longitud de la prueba. Sea TP una máquina de Turing que genera los teoremas de ZFC uno por uno. (TP significa “Bomba de teorema”). Entonces, la prueba más corta de T, si hay una, tiene una longitud inferior a

BB (longitud (T) + longitud (TP))

Aquí BB es la función Busy Beaver: Busy beaver – Wikipedia

Prueba: https://arxiv.org/pdf/1406.1808.pdf

BB es una función indiscutible. No podemos dar un límite superior computable en la longitud de una prueba. Si pudiéramos, sería decidible si T es un teorema o no (calcule el límite superior, luego verifique todas las pruebas hasta ese límite superior). Y luego podríamos resolver el problema de detención.