Computador prova teoria matemática de 400 anos

O matemático Johannes Kepler, que viveu nos séculos XVI e XVII, formulou uma teoria segundo a qual a forma mais eficiente de empilhar esferas, como as laranjas da foto, é colocá-las no formato de pirâmide. Embora tenha sido aceita em larga escala pelo comércio, a tese só foi provada no último domingo, 403 anos depois, por um computador.

O matemático responsável pelo projeto, Thomas Hayles, já havia criado uma prova matemática da teoria de Kepler em 1998, mas o resultado rendeu 300 páginas e levou quatro anos para ser revisado por 12 pessoas. Na época, apesar de todo o trabalho, o grupo disse ter 99% de certeza de que o trabalho estaria correto.

Em 2003, Hayles começou a traduzir os resultados da pesquisa para a forma computacional com o intuito de submetê-los aos softwares Isabelle e HOL Light, que teriam condições de dar respostas mais conclusivas ao problema. 

Via: New Scientist com Juru Em destaque