Prova assistida por computador - Computer-assisted proof

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

A maioria das provas auxiliadas por computador até agora foram implementações de grandes provas por exaustão de um teorema matemático . A ideia é usar um programa de computador para realizar cálculos longos e fornecer uma prova de que o resultado desses cálculos implica o teorema dado. Em 1976, o teorema das quatro cores foi o primeiro teorema principal a ser verificado usando um programa de computador .

Também foram feitas tentativas na área de pesquisa de inteligência artificial para criar novas provas menores e explícitas de teoremas matemáticos de baixo para cima usando técnicas de raciocínio de máquina , como a pesquisa heurística . Esses provadores automatizados de teoremas provaram uma série de novos resultados e encontraram novas provas para teoremas conhecidos. Além disso, os assistentes de prova interativa permitem que os matemáticos desenvolvam provas legíveis por humanos que, não obstante, são formalmente verificadas quanto à exatidão. Uma vez que essas provas são geralmente pesquisáveis ​​por humanos (embora com dificuldade, como acontece com a prova da conjectura de Robbins ), elas não compartilham as implicações controversas das provas por exaustão auxiliadas por computador.

Métodos

Um método para usar computadores em provas matemáticas é por meio dos chamados números validados ou numéricos rigorosos. Isso significa computar numericamente, mas com rigor matemático. Um usa aritmética de valor definido e princípio de inclusão a fim de garantir que a saída de valor definido de um programa numérico inclua a solução do problema matemático original. Isso é feito controlando, encerrando e propagando erros de arredondamento e truncamento usando, por exemplo , aritmética de intervalo . Mais precisamente, reduz-se o cálculo a uma sequência de operações elementares, digamos . Em um computador, o resultado de cada operação elementar é arredondado pela precisão do computador. No entanto, pode-se construir um intervalo fornecido pelos limites superior e inferior no resultado de uma operação elementar. Em seguida, procede-se substituindo números por intervalos e realizando operações elementares entre tais intervalos de números representáveis.

Objeções filosóficas

Artigo principal: prova não pesquisável

Provas assistidas por computador são o assunto de alguma controvérsia no mundo matemático, com Thomas Tymoczko sendo o primeiro a articular objeções. Aqueles que aderem aos argumentos de Tymoczko acreditam que longas provas auxiliadas por computador não são, em certo sentido, provas matemáticas "reais" porque envolvem tantos passos lógicos que não são verificáveis ​​na prática por seres humanos, e que os matemáticos estão efetivamente sendo solicitados a substituir a dedução lógica de axiomas assumidos pela confiança em um processo computacional empírico, que é potencialmente afetado por erros no programa de computador, bem como por defeitos no ambiente de execução e no hardware.

Outros matemáticos acreditam que longas provas assistidas por computador devem ser consideradas como cálculos , ao invés de provas : o algoritmo de prova em si deve ser provado válido, de modo que seu uso possa então ser considerado uma mera "verificação". Os argumentos de que as provas assistidas por computador estão sujeitas a erros em seus programas de origem, compiladores e hardware podem ser resolvidos fornecendo uma prova formal de correção para o programa de computador (uma abordagem que foi aplicada com sucesso ao teorema das quatro cores em 2005) como bem como replicar o resultado usando diferentes linguagens de programação, diferentes compiladores e diferentes hardwares de computador.

Outra maneira possível de verificar as provas auxiliadas por computador é gerar suas etapas de raciocínio em uma forma legível por máquina e, em seguida, usar um programa verificador de provas para demonstrar sua correção. Visto que validar uma determinada prova é muito mais fácil do que encontrar uma prova, o programa verificador é mais simples do que o programa assistente original e é correspondentemente mais fácil ganhar confiança em sua correção. No entanto, esta abordagem de usar um programa de computador para provar que a saída de outro programa está correta não atrai os céticos à prova de computador, que a veem como uma adição de outra camada de complexidade sem abordar a necessidade percebida de compreensão humana.

Outro argumento contra as provas auxiliadas por computador é que elas carecem de elegância matemática - que não fornecem insights ou conceitos novos e úteis. Na verdade, este é um argumento que poderia ser avançado contra qualquer prova longa por exaustão.

Uma questão filosófica adicional levantada por provas auxiliadas por computador é se elas transformam a matemática em uma ciência quase empírica , onde o método científico se torna mais importante do que a aplicação da razão pura na área de conceitos matemáticos abstratos. Isso se relaciona diretamente com o argumento dentro da matemática sobre se a matemática é baseada em idéias ou "meramente" um exercício de manipulação formal de símbolos. Também levanta a questão de saber se, se de acordo com a visão platônica , todos os objetos matemáticos possíveis em algum sentido "já existem", se a matemática auxiliada por computador é uma ciência observacional como a astronomia, ao invés de uma experimental como a física ou a química. Essa controvérsia dentro da matemática está ocorrendo ao mesmo tempo em que questões estão sendo feitas na comunidade da física sobre se a física teórica do século XXI está se tornando matemática demais e deixando para trás suas raízes experimentais.

O campo emergente da matemática experimental está enfrentando esse debate de frente, concentrando-se nos experimentos numéricos como sua principal ferramenta para a exploração matemática.

Formulários

Teoremas comprovados com a ajuda de programas de computador

A inclusão nesta lista não significa que exista uma prova formal verificada por computador, mas sim que um programa de computador foi envolvido de alguma forma. Veja os principais artigos para detalhes.

Teoremas para venda

Em 2010, acadêmicos da Universidade de Edimburgo ofereceram às pessoas a chance de "comprar seu próprio teorema" criado por meio de uma prova assistida por computador. Este novo teorema receberá o nome do comprador.

Veja também

Referências

Leitura adicional

links externos