‘Toda prova matemática deve ser compreensível e verificável’
Não importa se é o mapa do Brasil, com seus 26 estados (e um Distrito Federal), ou o gigante EUA, que ostenta 50 unidades federativas. Segundo os matemáticos, todo mapa, real ou imaginário, pode ser colorido com apenas quatro cores, de modo que regiões vizinhas não tenham a mesma cor.
Apesar de tradicionalmente considerado o marco do nascimento da área de machine-assisted proof, o “Teorema do mapa de quatro cores”, comprovado por Appel, Haken e Koch em 1976, não foi a primeira formulação verificada por máquina. Mais de dez anos antes, teoremas já eram provados por meio de exaustivas enumerações em computadores.
Leia também: Transferência de calor é tema da palestra de Milton Jara
Translado para o Aeroporto Internacional em 9 de Agosto
Teoria de pesquisador premiado permite avanço na medicina
No painel da União Internacional de Matemática (IMU), especialistas em machine-assisted proof se reuniram para debater quais as implicações desse tipo de prova matemática (pelo menos parcialmente gerada por computador) para autores, editoras e leitores. Mediada por James Davenport, a mesa redonda teve a participação dos matemáticos Bjorn Poonen, James Maynard, Harald Helfgott, Pham Huu Tiep e Luís Cruz-Filipe.
Até o momento, a maioria das provas auxiliadas por máquina tem sido implementações de grandes provas por exaustão de um teorema matemático. A ideia é usar um programa de computador para realizar cálculos demorados e fornecer uma prova de que o resultado dessas computações implica o teorema dado.
Mas o método é alvo de controvérsias no mundo da Matemática. A dificuldade de verificação de provas com muitas etapas lógicas e o fato de que processos computacionais podem ser afetados por erros no programa ou defeitos no tempo de execução e hardware são alguns dos argumentos levantados.
“Não importa se a prova foi feita pelo computador ou pelo homem, todas têm que ser compreensíveis e verificáveis”, frisou Poonen.
