Aquí está una larga cita del artículo vinculado en la pregunta:
Para la mayor parte de su historia, matemáticas fue esencialmente computacional: geometría tratados con construcciones de objetos geométricos, álgebra se ocupa de la algorítmica de soluciones de sistemas de ecuaciones, y el análisis de medios para calcular el comportamiento futuro de los sistemas que evolucionan a lo largo del tiempo. A partir de la prueba de un teorema en el sentido de que "para todo x existe un y tal que ...", que en general fue sencillo para extraer un algoritmo para calcular dicho y dado de x.
En el siglo xix, sin embargo, el aumento en la complejidad de los argumentos matemáticos empujado matemáticos para desarrollar nuevos estilos de razonamiento que suprimir algorítmica de la información y la invocación de las descripciones de los objetos matemáticos que abstraen los detalles de cómo los objetos están representados. El objetivo fue obtener un poderoso "conceptual" de la comprensión, sin estancarse en computacional detalles, pero esto tenía el efecto de la admisión de teoremas matemáticos que son simplemente falsas en un directo computacional de la lectura.
Con esto, vemos que los autores están hablando acerca de los teoremas de la forma "para cada $x$ no es un porcentaje ( $y$ ... ". Hay muchos de esos teoremas que son verdadero clásico, y donde los objetos del tipo de $x$ $y$ podría estar representada por un equipo, pero donde no hay un programa para producir $y$$x$. Esta área de estudio se superpone constructivo de las matemáticas y la teoría de la computabilidad. En la teoría de la computabilidad, en lugar de sólo demuestra que en particular los teoremas no son computably cierto, que en lugar de tratar de clasificar cómo uncomputable los teoremas son. También hay un campo de investigación de la prueba de minería de datos que es capaz de extraer de los algoritmos a partir de una serie de clásicas pruebas (por supuesto, no todos). Este programa ha llevado a nuevos límites de hormigón de teoremas en el análisis, entre otras cosas.
El fenómeno de la uncomputability en los clásicos teoremas matemáticos, es muy generalizado. Voy a dar sólo algunos ejemplos, tratando de incluir varias áreas de las matemáticas.
Hilbert 10 del Problema Un ejemplo viene de Hilbert del 10 de problema. Dado un multivariable polinomio con coeficientes enteros, no es un número natural $n$, de modo que $n = 1$ si el polinomio tiene una raíz entera, y $n = 0$ lo contrario. Este es un trivial clásico teorema, pero el MDRP teorema muestra exactamente que no hay ningún programa que puede producir $n$ desde el polinomio en cada caso.
Es decir, dada una multivariable polinomio con coeficientes enteros, donde podemos sustituir enteros para las variables, no hay una forma efectiva para decidir si $0$ está en el rango. La prueba de los usos clásicos de la teoría de la computabilidad, y muestra que esta decisión el problema es equivalente a detener problema, un ejemplo de prueba de referencia de un uncomputable decisión del problema.
Jordan formas de la Antera ejemplo viene cuando trabajamos con precisión infinita de números reales, de manera que un número real es representado como una secuencia de Cauchy racionales que converge a una tasa fija. Estas secuencias pueden ser manipulados por los programas, y esto es una parte estándar de la computables análisis.
Sabemos de álgebra lineal que cada cuadrado de la matriz sobre los reales tiene una forma canónica de Jordan. Sin embargo, no hay un programa que, dada una matriz cuadrada de precisión infinita de reales, produce la forma canónica de Jordan de la matriz.
La razón fundamental de esto es la continuidad: la fijación de una dimensión $N$, el mapa que lleva un $N \times N$ matriz a su Jordan en la forma no es continua. Sin embargo, si esta función se computable, entonces sería continuo, dando una contradicción.
Contables de la teoría de grafos es fácil representar una contables gráfico para un equipo: nos vamos a los números naturales representan los nodos, y nos proporciona una función que indica si hay una arista entre cualesquiera dos nodos. Es un clásico teorema de que "para cada contables gráfico no es un conjunto de nodos para que el conjunto tiene exactamente un nodo de cada componente conectado". Esto es falso de cómputo: no son contables gráficos para que el borde de la relación es computable, pero no es computable conjunto que se selecciona un nodo de cada componente conectado.
König del Lexema Cada infinita, finitely ramificación de los árboles tiene un camino infinito. Sin embargo, incluso si el árbol en sí es computable, no hay necesidad de ser un infinito computable camino.
Teorema del valor intermedio de Regresar a análisis, también podemos representar funciones continuas de los reales a los reales en una forma que, dado un infinito número de real de precisión, un programa puede calcular el valor de la función en ese número, la producción de otro precisión infinita número real. La representación es el llamado código de la función.
El teorema del valor intermedio es interesante porque es computably cierto en un sentido débil, pero no en un sentido más fuerte.
Es cierto que, para cualquier computable función continua $[0,1] \to \mathbb{R}$$f(0)\cdot f(1) < 0$, hay una computable real $\xi \in [0,1]$$f(\xi) = 0$. Así, si vivimos en un mundo donde todo era computable, el teorema del valor intermedio sería cierto.
Al mismo tiempo, no hay una computable funcional $G$ que toma como entrada el código de una función continua $f$ la satisfacción de las hipótesis anteriores, y se produce una $\xi = G(f)$$f(\xi) = 0$. Así, aunque el teorema del valor intermedio puede ser cierto, no hay manera de encontrar o construir la raíz acaba de dar un código para la función continua.
