Recuerdo haber leído en alguna parte que se tarda aproximadamente una semana en convertir una página de matemáticas en algo que acepte un asistente de pruebas como Isabelle o HOL Light.
¿Es este tipo de conversión algo que requiere mucha búsqueda y creatividad, o es casi mecánico?
El tiempo de formalización por página dista mucho de ser constante. Depende del material. A veces se avanza a toda velocidad y otras no.
Entre los obstáculos a la formalización figuran
A veces, el autor simplemente se rinde. El excelente texto de Kunen Teoría de conjuntos contiene una buena exposición del desarrollo de los conjuntos construibles y del axioma V=L, pero su prueba de que GCH se deduce de V=L es el esbozo más breve, de apenas 10 líneas. Esto para una prueba que le llevó a Gödel dos años y que podría decirse que le provocó un colapso mental. En otros casos, la parte más difícil de la demostración se ha dejado como ejercicio.
Debe estudiar detenidamente su material para ver si puede formalizarse con un esfuerzo razonable.
No soy un experto (he jugado un par de veces con HOL, pero nunca he formalizado completamente un teorema interesante), pero mi experiencia fue que es similar a escribir una demostración técnica después de haber trabajado en tu cabeza cómo hacerlo: la mayor parte del proceso es bastante dirigido y sólo estás completando detalles, pero a menudo tienes que hacer una pausa al principio de un paso para pensar en el mejor enfoque (que requiere una pequeña cantidad de creatividad), y de vez en cuando te encuentras con una dificultad grave que requiere pensamiento real y creatividad para superarla (en la escala de Parcheando un pequeño agujero en la demostración que conoces en su mayoría, no en la escala de llegar a una nueva demostración en primer lugar).
Estoy de acuerdo contigo, pero cabe mencionar que a veces hay formas (creativas) de sortear estas dificultades. La formalización del teorema de los cuatro colores evitó el teorema de la curva de Jordan replanteándolo como un problema de teoría de grafos. Además, hace unos años alguien habría dicho de la teoría de la homotopía lo mismo que tú dices de la topología geométrica. Pero ahora se sabe que la teoría de la homotopía está en cierto sentido "incorporada" a la teoría constructiva de tipo Martin-Löf, lo que la hace muy susceptible de ser probada por asistentes. Pero, por supuesto, se requiere una enorme dosis de creatividad para reformular un problema como éste.
Probablemente uno de los problemas es que tales demostradores tienden a estar optimizados para la lógica intuicionista (excepto Mizar, por lo que yo sé), y en mi experiencia, las matemáticas continuas hacen muchas más pruebas por contradicción. Mientras que es trivial usarlos para las matemáticas clásicas, perderás mucho del contenido computacional de las pruebas, y esto es algo que impulsa su desarrollo.
@Christoph-SimonSenjak, tanto Isabelle como HOL Light utilizan la lógica clásica (con teoría de tipos de orden superior). La prueba por contradicción no presenta ningún problema. Estoy de acuerdo en que en algunos asistentes de prueba como Coq, hay un deseo de extraer contenido computacional. Sin embargo, esa no es la única motivación. HOL Light tiene una extensa biblioteca matemática, se utiliza para certificar la aritmética de punto flotante IEEE en los chips de Intel, así como para verificar la prueba de Hale de la conjetura de Kepler. Del mismo modo, Isabelle se ha utilizado para una serie de proyectos de verificación tanto industriales como académicos.
Al igual que Henry, no soy un experto, aunque he jugado con asistentes de pruebas formales.
En primer lugar, hay que tener en cuenta si el material de base ya está formalizado. Esto puede suponer una gran diferencia. Si no está formalizado, puede que tengas que seleccionar una prueba diferente que sea más computacional y evite trucos que se aventuren en otro territorio. (Si la prueba que está formalizando es bastante nueva, puede que tenga que hacer ese trabajo usted mismo, lo que obviamente requiere tiempo y creatividad). Alternativamente, uno necesita formalizar este material de base (lo que puede ser satisfactorio, pero también lleva tiempo).
En segundo lugar, importa si lo que se pretende es construir una hermosa biblioteca matemática o si sólo se trata de reunir algunas pruebas hasta que el ordenador diga "demostrado". En el primer caso, puedes pasarte varias semanas pensando cómo quieres montar toda la estructura. (Por ejemplo, ¿define un anillo como un grupo abeliano con multiplicación o lo define desde cero? Si lo defines como un grupo abeliano, entonces también podrías utilizar todos los teoremas que demostraste para los grupos abelianos también para los anillos).
Por último, lleva algún tiempo acostumbrarse a utilizar un asistente de pruebas, pero después es bastante mecánico. No obstante, habrá veces en las que pensarás "esto es obvio, pero supongo que el ordenador no lo sabe". Entonces tendrás que averiguar cómo convencer al ordenador de que es cierto, normalmente descomponiendo la prueba en alguna lógica trivial. Sin embargo, como ocurre con todas las cosas, con la experiencia esto ocurre cada vez menos.
Siento no poder darte una tarifa del tipo "un día por página", más que nada por mi falta de experiencia.
I-Ciencias es una comunidad de estudiantes y amantes de la ciencia en la que puedes resolver tus problemas y dudas.
Puedes consultar las preguntas de otros usuarios, hacer tus propias preguntas o resolver las de los demás.
5 votos
No estoy seguro de que esta pregunta tenga una respuesta bien definida. Sin embargo, en mi opinión, a menudo hace falta creatividad para formular enunciados matemáticos con el grado de claridad necesario en diferentes contextos.
18 votos
En su artículo sobre la formalización del teorema de los números primos, Avigad informó de que, una vez que se puso al día, tardó aproximadamente un día en formalizar una página de matemáticas en Isabelle. Recomiendo este artículo por su análisis del proceso de formalización. repository.cmu.edu/filosofia/31
0 votos
@Carl Mummert: gracias por esa referencia, la desconocía y es sumamente útil.
0 votos
Hago esta CW porque parece un poco "de debate".