Navegar

7 de agosto de 2018, 17:49h

‘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.