On dirait que George Gonthier et ses collaborateurs ont fini de formaliser le théorème des ordres impairs .
Dans ses travaux antérieurs sur le théorème des quatre couleurs, Gonthier a inventé un tas de nouveaux algorithmes (principalement des variantes de BDD et d'algorithmes graphiques) qui se prêtaient particulièrement à une vérification formelle. Puisqu'il a dit qu'il continuait à utiliser ce style de vérification à réflexion à petite échelle dans les travaux sur la théorie des groupes finis, je me demande quelles nouvelles astuces algorithmiques ont été développées au cours de ce développement?
lo.logic
proof-assistants
Neel Krishnaswami
la source
la source
Réponses:
(Transformer un commentaire en réponse et le développer)
De parler à quelqu'un qui y a travaillé: non. Il a inventé toutes sortes de raffinements intelligents pour de nombreuses preuves et restructuré de nombreux développements théoriques, tous deux extrêmement précieux, mais les algorithmes impliqués ne sont pas intéressants - en fait, beaucoup d'entre eux sont une force brute stupide, tout le contraire d'intéressant.
Fondamentalement, ce qui était recherché était une ligne directe vers la preuve de Feit Thompson, sans se soucier du `` contenu informatique '' en cours de route (et même sans trop se soucier de la réutilisabilité de certains modules). C'était déjà extrêmement ambitieux compte tenu des délais. Heureusement, plusieurs des personnes impliquées dans le projet ont continué à remanier de nombreuses parties des épreuves à
la source