Por que é tão difícil para um computador provar alguma coisa?

18

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"?

Max Muller
fonte
7
Duas dificuldades principais. Incompletude (veja os Teoremas 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.
Dave Clarke
@ Dave Clarke: ok, na verdade, você diz que um computador é capaz de provar teoremas (novos), mas a grande quantidade de pesquisas possíveis dificulta a escrita de um teorema que tenha algum valor ou seja interessante, Estou certo? Você poderia explicar por que os Teoremas de Gödel e a "Incompletude" são relevantes aqui? Além disso, você tem uma referência a um artigo de pesquisa ou pesquisa em que é demonstrado que um computador realmente prova um teorema? Por fim, há muita pesquisa em andamento para tentar fazer com que os computadores provem teoremas? Qual é o nome dessa área de pesquisa (continuação ...) #
Max Muller
e você conhece um bom material introdutório? Quais são os pré-requisitos da matemática, mas especialmente da Ciência da Computação, para realmente entender esse material?
Max Muller
7
Você pode se interessar por parte do trabalho de Dorian Zeilberger, como " Ensinar o computador a descobrir (!) E depois provar (!!) (por si só (!!!)) Análogos da notória conjectura 3x + 1 de Collatz " ( math.rutgers.edu/~zeilberg/mamarim/mamarimhtml/collatz.html ). O co-autor frequente de Zeilberger, Shalosh B. Ekhad, é um computador.
Rob Simmons
4
A questão seguinte também dá vários exemplos agradáveis de computadores que ajudam a provar teoremas: cstheory.stackexchange.com/questions/82/...
Mugizi Rwebangira

Respostas:

22

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.

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.

UMAUMA

UMABUMA

Neel Krishnaswami
fonte
18

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.

PQPQ

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.

Dave Clarke
fonte
Não pude escolher entre essas duas respostas, porque ambas são ótimas. Joguei uma moeda para decidir qual escolher. Me desculpe, eu não escolhi o seu! Muito obrigado mesmo assim.
Muller Max
Você ganha um pouco, perde um pouco.
7268 Dave Clarke
Um relato menos técnico e mais matemático da prova de quatro cores e seu significado foi publicado em uma edição recente de avisos da AMS (a edição inteira pode ser uma leitura aconselhável para as pessoas interessadas na pergunta do OP).
Francois G