15/08/2014 – Atualizado em 15/08/2014
Por: jornal ciencia
A prova de um problema de 400 anos de idade, agora verificada com a ajuda de um computador, pode abrir o caminho para uma nova era da matemática, onde as máquinas fazem o trabalho pesado e deixam os seres humanos livres para estimularem outras linhas de pensamento.
O problema é um quebra-cabeça bem familiar para os donos de quitandas de todos os lugares: qual é a melhor maneira de dispor uma porção de objetos esféricos, como uma pilha de laranjas, para exposição? Em 1611, Johannes Kepler sugeriu que a forma piramidal seria a mais eficiente, mas nunca conseguiu provar.
Agora, um matemático anunciou a conclusão de uma jornada épica para comprovar formalmente a chamada conjectura Kepler. “Um enorme peso foi tirado dos meus ombros”, diz Thomas Hales, da Universidade de Pittsburgh, Pensilvânia, nos EUA, que liderou o trabalho.
Hales, em 1998, apresentou pela primeira vez uma prova de que a intuição de Kepler poderia estar correta. Apesar de existirem infinitas maneiras de empilhar muitas esferas, Hales quebrou o problema em milhares de arranjos possíveis que, matematicamente, representam as possibilidades. Tudo isso foi possível utilizando um software.
Mas a prova final rendeu um relatório de 300 páginas, que teve 12 revisores trabalhando por quatro anos para verificar se haviam erros. Mesmo quando foi publicado na revista Annals of Mathematics, em 2005, os revisores diziam que apenas tinham “99 por cento de certeza” sobre o estudo.
Em 2003, Hales começou o projeto Flyspeck, um esforço para reivindicar a sua prova através da verificação formal. Sua equipe utilizou dois softwares, chamados de Isabelle e HOL Light, ambos construídos com base na apuração lógica isenta de erros, fornecendo uma base para o computador verificar qualquer série de instruções lógicas para confirmar se são verdadeiras.
No último domingo, a equipe Flyspeck anunciou que finalmente havia conseguido traduzir a matemática densa do trabalho de Hale, através da plataforma computadorizada, verificando que suas teorias estão corretas. “Essa tecnologia exclui os árbitros matemáticos do processo de verificação”, disse Hales.
“Tem sido um grande esforço”, diz Alan Bundy, da Universidade de Edimburgo, no Reino Unido, que não estava envolvido no trabalho. Ele espera que o sucesso da Flyspeck inspire outros matemáticos a começarem a usar os assistentes digitais de prova. “Um matemático mundialmente famoso abraçou a demonstração automática de teoremas, esse tipo de fato sociológico é muito importante”, diz ele.
Idealmente, os assistentes de prova funcionariam como matemáticos suplentes tentando descobrir novas ideias. Softwares já podem provar alguns conceitos básicos, por si só, mas poderiam ser mais fáceis de usar. “Nós precisamos, de alguma forma, explorar provas, obtendo um grande quadro de resultados”, diz Bundy. “Ajudaria a perceber todos os detalhes. Nós, como seres humanos, não podemos absorver tanta coisa ao mesmo tempo”, disse.
Quanto a Hales, ele está pronto para seguir em frente. “Eu tive muitas ideias enquanto trabalhava nesta questão. Vamos esperar que o próximo projeto não demore 20 anos”, brincou o pesquisador.
