“Conjectura de Kepler”: problema é finalmente solucionado após 400 anos

Em 1611, o físico, matemático e astrônomo alemão Johannes Kepler propôs que a melhor maneira de se empilhar objetos esféricos — como frutas, por exemplo — seria organizá-los na forma de pirâmide. No entanto, ele não conseguiu provar que estava certo, e esse problema enigmático acabou ficando conhecido como a “Conjectura de Kepler”.

Pois, de acordo com o New Scientist, em 1998, o matemático norte-americano Thomas Hales anunciou que havia conseguido comprovar que a proposta de Kepler estava correta. Na época, Hales se apoiou em um método matemático que consiste em calcular todas as possibilidades possíveis de um teorema para se chegar à solução.

Contas e mais contas

Com base nesse método, Hales considerou que, embora existam infinitas formas de se empilhar objetos esféricos infinitamente, a maioria delas é, na verdade, apenas variações de alguns milhares de possibilidades. Assim, o matemático dividiu o problema em milhares de formas de se organizar objetos esféricos que matematicamente representavam as infinitas possibilidades de arranjos, e jogou todas essas informações em um software para fazer os cálculos.

O resultado foi uma pequena pilha de 300 páginas que levou quatro anos para ser completamente checada por 12 revisores! E mesmo depois de tanto trabalho, os matemáticos não estavam completamente seguros de que os cálculos estavam corretos, alegando que tinham apenas 99% de certeza de que a solução de Hales realmente comprovava a proposta de Kepler.

Finalmente, 100% de certeza

Bem, você sabe que “99% de certeza” não são suficientes para a matemática, não é mesmo? Pois em 2003, Hales deu início a um projeto para conseguir comprovar seus cálculos, empregando dois softwares de verificação formal — chamados Isabelle e HOL Light — para escrutinizar seu trabalho.

E não é que finalmente eles chegaram a uma conclusão! No último domingo, dia 10 de agosto, a equipe de Hales anunciou que, depois de traduzir a densa matemática presente nas 300 páginas dos cálculos de 1998 para uma linguagem computadorizada, eles conseguiram estabelecer que os cálculos estão corretos. Em outras palavras, depois de tantos séculos — e anos de esforços por parte de Hales e seu time —, a proposta de Kepler foi comprovada.

E o fato de o espírito de Kepler finalmente poder descansar em paz — e de Hales poder voltar sua atenção para outro problema complicado — não é a única boa notícia nessa história toda. Essa tecnologia pode ser utilizada na verificação da grande quantidade de trabalhos que surgem todos os anos, livrando os matemáticos dessa tarefa ingrata e permitindo que eles usem esse tempo para se concentrar em outras questões e soltar a criatividade para explorar o universo dos números.