A partir de 2018, pruebas matemáticas siguen siendo decidido por el ser humano consenso. es decir, Dar la prueba a los pocos capaces los seres humanos y si ninguno de ellos puede encontrar cualquier error de votar que la prueba es correcta y que pueda ser publicado.
Sin duda, esto no es una manera infalible de decidir matemática verdades.
Uno podría pensar que habría, por ahora alguna manera estándar de pruebas podría ser por escrito y el equipo comprueba la exactitud.
Leí acerca de un par de ordenador comprobación de los sistemas de hace un par de años que espera hacer las cosas como comprobar Artimaña de la prueba del último teorema de Fermat o la Clasificación de los Simples Grupos de Teorema. Pero no mucho más se ha oído hablar de ellos.
Lo que ha sucedido en este empeño. Tener matemáticos perdido el interés en tener pruebas de equipo comprueba?
Solía ser que los matemáticos se esfuerzan para la formalización de todas las matemáticas. Y, sin embargo, parece que prefieren el mal formalismo actual de las matemáticas que no puede ser traducido al lenguaje de computadora, debido a que es ambigua.
Yo habría pensado que en el 2018, cada prueba sometida a una matemática diario sería básicamente por escrito en un formulario que podría ser automáticamente una prueba marcada. Y por el contrario todos los que no están fundados teorema escrito en un lenguaje que podría ser alimentado en una computadora.
Incluso un aficionado podría publicar una prueba a la revista y con la prensa de un botón, a ver si la prueba es correcta o basura.
¿Sabéis cuál es el estado actual de la que es esto?
