Na ciência da computação (ou na matemática assistida por computador), um assistente de prova é um software que permite a escrita e verificação de provas matemáticas, seja em teoremas no sentido usual da matemática, seja em afirmações relacionadas à execução de programas .
Muitos projetos foram lançados para formalizar a matemática, em 1966 Nicolaas de Bruijn lançou o projeto Automath , seguido de outros projetos. Os projetos mais avançados são o projeto Mizar na Polónia , o projeto HOL (en) - Isabelle na Grã-Bretanha e Estados Unidos e o projeto Coq na França .
O objetivo desses projetos é fornecer ao matemático ferramentas de computador para ajudá-lo a desenvolver uma versão formal do resultado no qual está interessado. O software também armazena os resultados demonstrados anteriormente.
Escrever evidências totalmente formais é uma atividade extremamente tediosa; muitos passos que seriam pulados, porque considerados óbvios para o leitor familiarizado com a matemática, devem ser dissecados nos maiores detalhes. No entanto, o assistente de prova pode fornecer mais ou menos automação para limitar o trabalho do usuário humano.
Alguns assistentes de prova, como PVS , têm procedimentos de decisão em áreas frequentemente usadas e decidíveis (como aritmética Presburger ); frequentemente, eles são adicionados a procedimentos de semidecisão (que não necessariamente terminam com sucesso).
Segundo estudo de Freek Wiedijk citado em 2011 na revista Pour la Science, mas atualizado desde então, na lista dos “100 teoremas matemáticos mais importantes” - lista atribuída a Paul e Jack Abad - 91 dos 100 teoremas foram formalizados.
Com os assistentes de prova atuais, o trabalho de formalização torna-se tedioso por uma linguagem complexa.
Assistentes de prova são úteis para demonstrar problemas muito complexos e ajudam a produzir uma demonstração formal. O famoso problema das quatro cores é um dos problemas resolvidos com esta ferramenta.
Uma objeção ao uso de auxiliares de prova é que, em qualquer caso, a segurança das provas obtidas depende do bom funcionamento do auxiliar. Na verdade, os assistentes de prova são softwares grandes e complexos, que se pode suspeitar que eles próprios estejam bugados. Um assistente de prova de erros pode demonstrar o absurdo. Alguns assistentes de prova, como Coq, produzem um termo de prova cuja verificação pode ser delegada a um software muito mais simples do que um assistente completo; assim, Coq produz termos do cálculo de construções (agora indutivos), um cálculo lambda de ordem superior tipado , que pode-se verificar com relativa facilidade se eles foram digitados corretamente. Além disso, o Coq foi comprovado no Coq por seu verificador de demonstração, o que torna a confiança que se pode ter neste software um pouco mais legítima.
Nota sobre a terminologia: o uso de prova em vez de prova é, estritamente falando, anglicismo, como uma tradução direta da palavra prova , mas o uso da palavra "prova" agora faz parte da linguagem de especialistas e este artigo está de acordo com este usar. A dificuldade é ainda maior porque a palavra "demonstração" tem um uso comum diferente em inglês.