Em 1611, Johannes Kepler sugeriu que a forma mais eficiente de empilhar objetos esféricos, como laranjas, era em uma formação de pirâmide.
Infelizmente, ele não conseguiu provar o que ficou chamado de conjectura de Kepler.
Agora, um computador finalmente mostrou que a ideia do astrônomo e matemático é verdadeira.
Na verdade, foi Thomas Hales, da Universidade de Pittsburgh (EUA), quem desenvolveu uma prova para o problema muitos anos atrás, em 1998.
Apesar de existirem infinitas maneiras de empilhar infinitamente muitas esferas, a maioria são variações de apenas alguns milhares de possibilidades. Sendo assim, Hales quebrou o problema em milhares de arranjos possíveis que matematicamente representam infinitas possibilidades, e utilizou um software para resolver todos.
No entanto, o trabalho final ficou com 300 páginas, e foram necessários 12 revisores e quatro anos para verificar se havia algum erro em todo o documento. Mesmo assim, quando o estudo foi publicado na revista Annals of Mathematics em 2005, os cientistas estavam apenas 99% seguros de que o resultado estava correto.
Então, em 2003, Hales começou a criar o projeto “Flyspeck”, uma ferramenta computacional capaz de verificar sua prova. O programa usa duas peças de verificação formal que contam com apenas uma pequena série facilmente validada de demonstrações lógicas.
Usando o projeto, qualquer pesquisador pode verificar qualquer série de outras declarações lógicas, como uma prova de matemática, se tiver tempo suficiente.
Recentemente, Hales e sua equipe anunciaram que as 300 páginas de seu trabalho foram analisadas pelo par de programas e, para seu alívio, está tudo correto.
Em outras palavras, o computador verificou com êxito que a ideia apresentada por Kepler mais de 400 anos atrás é precisa. “De repente, me sinto dez anos mais jovem”, disse Hales.
Essa não é apenas uma boa notícia para Hales. Centenas de provas matemáticas ridiculamente densas são criadas a cada ano, e saber que elas podem ser verificadas por computadores, em vez de seres humanos, significa que os matemáticos podem se concentrar em pensar criativamente sobre seus problemas e deixar que as máquinas façam o trabalho pesado de verificação.
Alan Bundy, da Universidade de Edimburgo, no Reino Unido, que não esteve envolvido no trabalho, espera que o sucesso de Flyspeck inspire outros matemáticos a começar a usar os computadores como assistentes de prova. “Este é um estudo de caso que poderia começar a se tornar a norma”, disse. [Gizmodo, NewScientist]