Parece que George Gonthier e seus colaboradores terminaram de formalizar o Teorema da Ordem Estranha .
Em seu trabalho anterior sobre o Teorema das Quatro Cores, Gonthier inventou vários novos algoritmos (principalmente variantes de BDDs e algoritmos gráficos) que eram especialmente passíveis de verificação formal. Como ele disse que continuava a usar esse estilo de verificação de reflexão em pequena escala no trabalho sobre teoria de grupos finitos, pergunto-me que novos truques algorítmicos foram desenvolvidos durante esse desenvolvimento?
lo.logic
proof-assistants
Neel Krishnaswami
fonte
fonte
Respostas:
(Transformando um comentário em resposta e expandindo-o)
De falar com alguém que trabalhou nisso: não. Ele inventou todo tipo de refinamentos inteligentes para muitas provas e reestruturou muitos desenvolvimentos da teoria, ambos extremamente valiosos, mas os algoritmos envolvidos não são interessantes - na verdade, muitos deles são força bruta muda, o oposto de interessante.
Basicamente, o que se buscava era uma linha direta para a prova de Feit Thompson, sem se preocupar com o 'conteúdo computacional' ao longo do caminho (e mesmo sem se preocupar demais com a reutilização de alguns dos módulos). Isso já era extremamente ambicioso, considerando os prazos. Felizmente, várias pessoas envolvidas no projeto refatoraram muitas partes das provas a serem
fonte