Um bug do verificador de provas já invalidou uma prova principal?

29

A maioria dos assistentes de prova (todos?) Tem bugs corrigidos na ocasião. No entanto, daqueles que eu vi esses bugs geralmente são difíceis de encontrar sem querer, e os resultados provados antes que o bug seja corrigido geralmente se mantêm após a correção.

Três perguntas, em ordem de força:

  1. Uma correção desse tipo de correção causou falha em uma prova importante, sem modificá-la?
  2. Se (1) for verdadeira, foram necessárias grandes modificações para corrigir a prova?
  3. Se (2) for verdadeiro, alguém provou um teorema importante errado devido a um erro de solidez?

Vou deixar a definição de "major" para os outros.

proof-assistants soundness Geoffrey Irving
fonte
11
Provavelmente isso mostra minha ignorância, mas um teorema importante já foi estabelecido pela primeira vez com um assistente de prova? É claro que conheço o teorema das quatro cores e a conjectura de Kepler, mas não acho que as primeiras provas tenham usado assistentes. Estou curioso.
Sasho Nikolov
11
Acredito que nenhum ser humano provou ser um compilador correto, e estava correto quanto a isso, até o CompCert. Mas você está certo que isso tornaria (3) uma questão menos interessante.
Geoffrey Irving
4
@ShohoNikolov: isso não é realmente relevante, pois a maioria das provas feitas na prática por assistentes de prova não é sobre matemática. Eles geralmente são sobre sistemas de software, ou sobre propriedades de sistemas formais etc. (É apenas uma questão de tempo quando a grande maioria das provas feitas neste planeta não é sobre matemática pura. Os robôs estão chegando.) Seria bastante irritante. se, por exemplo, alguém provou, usando um assistente de prova, que algum sistema crítico é seguro, e depois descobriu-se que eles usaram acidentalmente uma inconsistência.
Andrej Bauer 13/01
11
Obrigado @AndrejBauer. Então "prova principal" e "teorema importante" aqui significam não ser importante para matemáticos de pesquisa, mas provas de correção de sistemas críticos importantes?
Sasho Nikolov
11
Eu acho que qualquer prova que seja considerada importante por muitas pessoas (matemáticos, especialistas em segurança, engenheiros de software) contaria. Tenho medo que não vamos descobrir porque se alguém fez tropeçar a este problema, as chances são eles calmamente fixa-lo.
Andrej Bauer 13/01

Respostas:

11

Que eu saiba, nenhuma máquina verificada prova de um desenvolvimento matemático complexo já foi retirada.

Como aponta Andrej fora, porém, às vezes acontece que os erros de quebra de solidez que surgem nestes sistemas (embora geralmente não silenciosamente , como Andrej sugere), e a correção para esse bug envolve algumas mudanças para as provas existentes, ou, mais provavelmente, de a biblioteca padrão do sistema de prova envolvido.

Alguns exemplos dessas provas de quebra de biblioteca na Coq:

https://coq.inria.fr/bugs/show_bug.cgi?id=4294

https://sympa.inria.fr/sympa/arc/coq-club/2013-12/msg00119.html

É difícil dizer se as provas estabelecidas dependiam da inconsistência, pois, após a correção, elas exigiram pequenos ajustes para serem aceitos pelo verificador de provas. Mas isso acontece a cada atualização não trivial!

Minha opinião pessoal é que é improvável que tais erros ocorram, pois a prova em papel precisa ser bem polida antes que a formalização da máquina possa ser tentada.

Inconsistências em estruturas de prova geralmente exigem o uso pesado de combinações estranhas de recursos esotéricos e, muito raramente, surgem "por acidente".

cody
fonte
3
Eu estava me referindo às pessoas que corrigiam problemas em seus scripts de prova silenciosamente , ou mesmo sem o saber, como Geoffrey apontou, como uma reação aos erros dos assistentes de prova. Obviamente, as inconsistências nos assistentes de prova são sempre recebidas com um incrível nível de entusiasmo. Os matemáticos devem ter uma inconsistência em matemática, o que levaria alguns meses interessantes.
Andrej Bauer
2
O que há com as pessoas que jogam links da Wikipedia para mim? @ RickyDemer, por favor, explique seu ponto de vista. Já ouvi falar do paradoxo de Russell, você sabe. Isso foi há mais de 100 anos e levou a algumas excelentes matemáticas. Estou propondo que estamos maduros para outro.
Andrej Bauer
Por enquanto, aceito esta resposta, mas é claro que não a aceitarei se alguém responder na outra direção! (Divulgação completa: Esta foi a resposta que eu estava esperando.)
Geoffrey Irving
11
@GeoffreyIrving A resposta é um tanto insatisfatória, já que é difícil para mim provar a falta de retratação! A resposta é, portanto, um tanto necessariamente baseada na minha falta de conhecimento, embora tenha havido tão poucas formalizações de máquinas em grande escala que estou pelo menos um pouco confiante em minha resposta. Também ouvi dizer que algumas formalizações importantes no método B demonstraram ter suposições inconsistentes (você precisa adicionar muitos axiomas para declarações não triviais, e as coleções de axiomas tomadas em conjunto foram posteriormente mostradas como sendo ...
cody
11
... inconsistente). Infelizmente, não consigo encontrar uma referência para isso, então não a incluí na minha resposta. Também a formalização era sobre um programa grande, e não sobre matemática pura.
Cody