Prova assistida por computador

Uma Prova assistida por Computador é uma prova matemática que foi pelo menos parcialmente gerada por computador.

A maioria das provas assistidas até hoje têm sido implementações de grandes provas por exaustão de um teorema matemático. A ideia é usar um programa de computador para realizar computações longas, e prover uma prova de que o resultado dessas computações implica o teorema dado. Em 1976, o teorema das Quatro Cores foi o primeiro grande teorema a ser verificado usando um programa de computador.

Tentativas também foram feitas na área de pesquisa de inteligência artificial para criar provas novas, explícitas e menores de teoremas matemáticos usando técnicas de inteligência artificial como busca heurística. Tais provadores de teoremas matemáticos provaram uma quantidade de novos resultados e acharam novas provas para teoremas conhecidos. Adicionalmente, assistentes de provas interativos permitiram que matemáticos desenvolvessem provas humanamente legíveis que são no entanto formalmente verificadas por corretude. Uma vez que essas provas são geralmente inspecionadas por humanos (embora com dificuldade, como a prova de Conjectura de Robbins), elas não compartilham as implicações controversas de provas por exaustão assistidas por computador.

Métodos

Um método para usar computadores em provas matemáticas é o tão chamados numéricos validados ou numéricos rigorosos. Isso significa que computar numericamente sendo que ainda com rigor matemático. Um uso da aritmética dos conjuntos(precisa de verificação) e principio da inclusão para garantir que a saída de um programa numérico inclua a solução do problema matemático original. Isso é feito controlando, enclausurando e propagando erros de truncamento e arredondamento usando, por exemplo, aritmética de intervalos. Mais precisamente, uma reduz para uma computação de sequencias de operações elementares(como +, - , *, /). No computador, o resultado de cada operação elementar é arredondado pela precisão computacional. Entretanto, um pode construir um intervalo fornecido pelos limites inferior e superior no resultado de uma operação elementar. Então ele avança substituindo números com intervalos e efetuando operações elementares entre tais intervalos de números representados.

Objeções Filosóficas

Provas assistidas por computador são tópicos de maior controvérsia do mundo matemático. Alguns matemáticos acreditam que provas assistidas por computador longas não são, em algum sentido, provas matemáticas reais porque envolvem tantos passos lógicos que eles não são verificáveis, por seres humanos, na pratica, e que matemáticos estão sendo pedidos para substituir dedução logica de axiomas assumidos com confiança em um processo computacional empírico, que é potencialmente afetado por erros de um programa de computador, assim como defeitos no ambiente de execução e no hardware.

Outros matemáticos acreditam que provas assistidas por computador longas devem ser consideradas como cálculos, ao invés de provas: o algoritmo de prova por si só deve ser provado valido, para que seu uso então possa ser considerado uma mera verificação. Isso é conhecido como Princípio de Poincaré na comunidade matemática, depois de uma afirmação de Henri Poincaré. Discussões de que provas assistidas por computador estão sujeitas a erros no seu programa fonte, no compilador e no hardware podem ser resolvidas ao se provir com uma prova formal de corretude do programa de computador(uma abordagem que foi aplicada com sucesso no teorema das quatro cores em 2005) assim como replicar o resultado usando diferentes linguagens de programação, diferentes compiladores e diferentes hardwares.

Outra possível maneira de se verificar provas assistidas por computador é gerar o raciocínio dos seus passos em uma forma legível por máquinas, então usar um provador de teorema matemático para demonstrar sua corretude. Essa abordagem de utilizar programas de computador para provar a corretude de outros programas ainda não convence as pessoas céticas que provas podem ser feitas dessa maneira, pessoas que veem isso como a adição de outra camada de complexidade sem abordar a notável necessidade por entendimento humano.

Outro argumento contra essas provas é que elas sempre carecem de elegância matemática - que elas não proveem novas visões ou conceitos uteis. De fato, esse é um argumento que poderia ser usado contra qualquer prova por exaustão longa.

Um problema filosófico adicional levantado por provas assistidas por computador é se elas fazem da matemática uma ciência quasi-empirica, onde o método cientifico se torna mais importante do que a aplicação de pura razão na área de conceitos matemáticos abstratos. Isso está relacionado diretamente com a discussão dentro da matemática de se a matemática baseia-se em ideias, ou se é meramente um exercício da manipulação de símbolos formais. Isso também levanta a questão de se, se acordo com a visão platonista, todos os possíveis objetos matemáticos de alguma forma já existem, se matemática assistida por computador é uma ciência observacional, assim como a astronomia, e não uma experimental como química e física. Interessantemente, essa controvérsia entre matemáticos está ocorrendo ao mesmo tempo em que perguntas estão sendo feitas na comunidade de física sobre se a física teórica do século 21 está se tornando muito matemática, e deixando para trás suas raízes experimentais.

O campo emergente da matemática experimental está confrontando esse debate de cabeça por focar em experimentos como sua principal ferramenta de exploração matemática.

Lista de Teoremas provados com Programas de Computador

Inclusão nessa lista não implica que um prova formal checada por computador existe, mas que um programa de computador esteve envolvido de alguma forma. Veja o artigo principal para detalhes.

• Teorema das quatro cores, 1976.
• Conjectura de Mitchell Feigenbaum's universalidade, 1982.
• Connect Four, 1988 – um jogo.
• Não-existencia do plano pojetivo finito de ordem 10, 1989.
• Conjectura de Robbins, 1996.
• Conjectura de Kepler, 1998.
• Atrator de Lorenz, 2002.
• 17-ponto caso do problema do Final Feliz, 2006.
• NP-difícil de triangulação de peso minimo, 2008.

Ver também

• Computação simbólica.
• Checagem de modelos.
• Checagem de provas.
• Raciocínio automatizado.
• Verificação formal.
• Estudo observacional.
• Garbage in, garbage out.
• Seventeen or Bust.