Hubo una conferencia sobre el último teorema de Fermat donde vendieron una camiseta como esta: las camisetas del último teorema de Fermat. El material al que se hace referencia en la camiseta representa de alguna manera la última fase del trabajo sobre ella. Las charlas en la conferencia tuvieron como objetivo ayudar a proporcionar un trasfondo para lo que creo que se incluyó en un volumen de varios cientos de páginas. Bourbaki hizo un intento de desarrollar las matemáticas de una manera rigurosa a partir de la teoría de conjuntos, y uno necesitaría bastante de esto.
Entonces, incluso sin que ninguno de nosotros sea un verdadero experto en el material de la prueba, esto podría darnos una idea cruda de cuánto tiempo podría ser la prueba si se expresa en lenguaje humano natural . Podría estar equivocado, pero estoy pensando que mil páginas no serían suficientes a menos que trabajes duro para mantener todo conciso. Ya hay algunos requisitos previos que probablemente tomarían unos cientos de páginas cada uno. Por otro lado, me parece probable que diez mil páginas serían suficientes para hacer una especie de tratamiento actualizado tipo Bourbaki, además de libros de texto sobre los temas de fondo necesarios, y finalmente esa serie de documentos que finalmente llegaron a Fermat.
Otra forma de decirlo es que no creo que sea tanto tiempo que una persona individual no pueda leerlo en principio, no es probable que alguien quiera hacerlo. Los matemáticos como Wiles probablemente toman algunos resultados previos necesarios sobre la confianza en lugar de leerlos todos, pero si se hubiera preocupado exclusivamente por leer el trabajo anterior en lugar de desarrollar nuevos resultados, y si hubiera tenido a alguien mirando por encima del hombro, diciéndole cuál de los los papeles que estaba leyendo serían necesarios, creo que podría haberlo hecho. Parecía tener una reputación de ser razonablemente exhaustivo en su comprensión de las herramientas que necesitaba, por lo que la brecha entre las pruebas que se necesitaban y las pruebas que había estudiado podría no ser tan amplia.
Estoy de acuerdo con Daniil Kozhemyachenko cuando se trata de formalizar en ZFC. Se sabe que ZFC es horrible para la formalización real. En sí mismo no le permite definir una fórmula como la formalización de “x es un número ordinal” y, a partir de ese momento, abreviarla como ord (x) o alguna otra abreviatura. Los lógicos que escriban sobre ZFC usarán abreviaturas como esa, porque entienden que, en principio, uno podría expandirlo, y lo importante generalmente es que existe una fórmula de este tipo, no con cuánto tiempo es. No pude rastrearlo, pero he visto ejemplos absurdos del tamaño de la fórmula en el lenguaje de ZFC que se obtiene al sustituir las definiciones. Para estar dentro de un orden de magnitud requeriría saber al menos cuántas capas de expansión de definición serían necesarias. No es necesario que sea una prueba larga y sofisticada para que sea bastante inútil estimar a qué se expandiría.
- ¿Cómo se puede demostrar matemáticamente que, si n y k son enteros positivos, entonces [matemática] \ lceil {\ frac {n} {k}} \ rceil = \ lfloor {\ frac {n-1} {k}} \ rfloor +1 [/ matemáticas]?
- ¿Por qué la función de estimación primaria de ejemplo cuenta menos los compuestos?
- ¿Cómo demostró Euler la conexión entre los números primos y la función Zeta de Riemann?
- Cómo comenzar a aprender teoría de números
- ¿Cuál es el algoritmo más eficiente para encontrar el período de Pisano para un entero dado (incluso para enteros grandes)?
En un verificador de pruebas automatizado más sensato, donde (por un lado) hay fórmulas tan definidas, sería menos loco. El lenguaje está diseñado para ser lo suficientemente conciso como para leerlo. La relación entre la duración de una prueba informal y su formalización en un verificador de pruebas razonable se ha denominado el “factor de Bruijn”. El documento aquí (http://www.sciencedirect.com/sci…) tiene un ejemplo en el que el factor parece ser alrededor de 20. Haga lo que quiera.