Isso pode ser considerado uma pergunta estúpida. Eu não sou formado em ciência da computação (e também não sou formado em matemática), então, desculpe-me se você acha que as seguintes perguntas apresentam algumas suposições errôneas importantes.
Embora haja planos para formalizar o Último Teorema de Fermat (veja esta apresentação ), nunca li ou ouvi dizer que um computador possa provar até um teorema "simples" como o de Pitágoras.
Por que não? Qual é (/ são) a (s) principal (s) dificuldade (s) por trás do estabelecimento de uma prova totalmente autônoma por um computador, auxiliada apenas por alguns "axiomas embutidos"?
Uma segunda pergunta que gostaria de fazer é a seguinte: Por que somos capazes de formalizar muitas provas, enquanto atualmente é impossível para um computador provar por si próprio um teorema? Por que isso é "mais difícil"?
fonte
Respostas:
Em 1949, Tarski provou que quase tudo em The Elements se encontra dentro de um fragmento decidível da lógica, quando mostrou a decidibilidade da teoria de primeira ordem dos campos fechados reais. Portanto, o teorema de Pitágoras, em particular, não é muito comentado, porque não é especialmente difícil.
fonte
Duas dificuldades principais. Incompletude (consulte os Teoremas de Incompletude de Gödel) e o vasto tamanho do espaço de pesquisa (existem muito mais teoremas desinteressantes do que interessantes). Um progresso considerável foi feito usando assistentes de prova ( Coq , Isabelle, Agda, etc.). Com eles, o matemático escreve os teoremas e lemas e o assistente de prova ajuda a encontrar provas e garante que as provas sejam logicamente válidas.
Este artigo descreve como o assistente de prova Coq é usado para provar o teorema das quatro cores. A matemática mecanizada ( visão geral ) é uma área do TCS dedicada a (semi) provar automaticamente os teoremas (e, em geral, usar computadores para ajudar matemáticos).
Uma área em que a prova automatizada de tipos de teoremas está causando impacto está na verificação e descoberta de modelos. A verificação de modelo trata de determinar se um determinado sistema satisfaz uma determinada propriedade, enquanto a localização do modelo encontra um sistema para satisfazer uma determinada coleção de propriedades. A ferramenta Alloy emprega verificação de modelo e descoberta de modelo com bom efeito, e é bastante utilizável.
fonte