Algoritmos interessantes na formalização do teorema de Feit-Thompson?

26

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?

Neel Krishnaswami
fonte
para referência en.wikipedia.org/wiki/Feit%E2%80%93Thompson_theorem (cada grupo finito de ordem ímpar é solúvel)
Radu GRIGORE
4
Deveria ser possível que Gonthier respondesse a essas perguntas. Alguém que está perto de seu escritório, por favor, aponte-o aqui. Diga a ele que somos grandes fãs dele.
Andrej Bauer
4
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, mas os algoritmos envolvidos não são interessantes - na verdade, muitos deles são força bruta muda, exatamente o oposto de interessante.
Jacques Carette
@JacquesCarette: Eu acho que deve ser uma resposta, vendo como nada mudou sobre ele em poucos anos ...
Joshua Grochow

Respostas:

10

(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

  • mais reutilizável para um conjunto mais amplo de aplicativos
  • mais computacionalmente significativo
Jacques Carette
fonte