Corria o ano de 1611 quando o matemático alemão Johannes Kepler propôs que a melhor forma de arrumar objetos esféricos seria empilhá-los numa pirâmide, como as pirâmides de laranjas que vemos no supermercado, mas não conseguiu prová-lo matematicamente. Aliás, apesar dos esforços nenhum humano conseguiu fazê-lo com 100% de certeza. Mais de 400 anos depois foi um computador que trouxe a confirmação.

Existe um número quase infinito de formas para empilhar esferas, embora resultem da variação de alguns milhares de temas principais. Ainda assim, qual seria a forma mais eficiente? Johannes Kepler apostou na pirâmide, mas não conseguiu prová-lo matematicamente, por isso Thomas Hale, matemático na Universidade de Pittsburgh, na Pensilvânia (Estados Unidos), decidiu encetar esta jornada épica: criou um programa de computador que lhe permitiu testar cada uma das hipóteses entre as milhares possíveis. Em 1998 estava em condições de dizer que Johannes Kepler estava correto.

Porém, o relatório matemático de 300 páginas não granjeou mais do que uma certeza de 99% pelos 12 cientistas que o avaliaram. Thomas Hale não ficou satisfeito com esta resposta e em 2003 deu início ao projeto Flyspeck cujo objetivo era realizar uma verificação formal dos resultados que tinha obtido sem precisar de recorrer a humanos, pelo menos fora da sua equipa. Usou os programas Isabelle e HOL Light, criados para ajudarem a confirmar teoremas matemáticos e realizar cálculos lógicos e aperfeiçoados para não cometerem erros. No dia 10 de agosto a equipa do projeto Flyspeck anunciou que os cálculos de Thomas Hale estavam corretos, logo ,que Johannes Kepler tinha razão.

“Com esta tecnologia os júris matemáticos são colocados fora do processo de verificação”, diz Thomas Hale. “A sua opinião sobre se a prova está correta deixa de ter importância.” Alan Bundy, investigador na Universidade de Edimburgo,apesar de não ter estado envolvido neste projeto, também defende o uso de programas de computador para se validarem as provas matemáticas. “Ver tudo nos seus detalhes mais profundos está além das nossas capacidades, como humanos não conseguimos absorver tanto.”