Parece que George Gonthier y sus colaboradores han terminado de formalizar el Teorema de la orden impar .
En su trabajo anterior sobre el Teorema de los cuatro colores, Gonthier inventó un montón de nuevos algoritmos (en su mayoría variantes de BDD y algoritmos de gráficos) que eran especialmente susceptibles de verificación formal. Como ha dicho que continúa utilizando este estilo de verificación de reflexión a pequeña escala en el trabajo sobre la teoría de grupos finitos, me pregunto qué nuevos trucos algorítmicos se desarrollaron durante este desarrollo.
lo.logic
proof-assistants
Neel Krishnaswami
fuente
fuente
Respuestas:
(Convertir un comentario en una respuesta y ampliarlo)
De hablar con alguien que trabajó en esto: no. Inventó todo tipo de refinamientos inteligentes para muchas pruebas, y reestructuró muchos desarrollos teóricos, los cuales son extremadamente valiosos, pero los algoritmos involucrados no son interesantes; de hecho, muchos de ellos son una fuerza bruta tonta, todo lo contrario de interesante.
Básicamente, lo que se buscaba era una línea directa a la prueba de Feit Thompson, sin preocuparse por el 'contenido computacional' en el camino (e incluso sin preocuparse demasiado por la reutilización de algunos de los módulos). Esto ya era extremadamente ambicioso dados los plazos. Afortunadamente, varias de las personas involucradas en el proyecto han refactorizado muchas partes de las pruebas para ser
fuente