En principio, cualquier cuestión matemática $\psi$ que no es independiente de ZFC (o de alguna teoría estándar más fuerte, como ZFC+grandes cardinales) es reducible al procedimiento computacional finito: buscar una prueba de $\psi$ o una prueba de $\neg\psi$ . Si el enunciado no es independiente, entonces encontraremos uno u otro; pero tales procedimientos de cálculo son generalmente inviables, sin que se conozca el límite de su longitud. Mientras tanto, si $\psi$ es demostrablemente independiente de ZFC, entonces podemos buscar una prueba de ello. Pero, por desgracia, si nuestros axiomas son consistentes, entonces algunos enunciados pueden ser independientes, pero no demostrables, y podemos demostrar que si nuestros axiomas son consistentes, entonces habrá tales ejemplos.
Mientras tanto, hay muchas teorías interesantes y útiles que se han demostrado decidibles, pero que tienen procedimientos de decisión inviables. Por ejemplo, cualquier cuestión de geometría cartesiana en cualquier dimensión finita es decidible en principio por medios computacionales, ya que la teoría de los campos reales cerrados es decidible lo que significa que, en principio, podemos decidir la verdad de cualquier afirmación expresable en la estructura $\langle\mathbb{R},{+},{\cdot},{\lt},0,1\rangle$ que incluye muchos enunciados interesantes, muchos de los cuales son problemas abiertos naturales del tipo que usted busca, como casi todos los famosos problemas de empaquetamiento. Desgraciadamente, los algoritmos más conocidos para este procedimiento de decisión son, como mínimo, de tiempo doblemente exponencial y, por tanto, inviables. Del mismo modo, la teoría de los grupos abelianos es decidible; Aritmética de Presburgo es decidible; el teoría del ajedrez infinito es decidible y muchas otras teorías interesantes, capaces de expresar muchos problemas naturales.
Así que parece que hay una abundancia de ejemplos del tipo que usted busca.