Cálculo matemático sobre empilhamento de frutas é finalmente resolvido após 400 anos!
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.
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.
Foto: Reprodução / WikipédiaCommons
Fonte:Jornal Ciência
Post a Comment