Computador enfim confirma resposta para um problema matemático de 400 anos atrás

Jamie Condliffe - New Scientist - GIZMODO BRASIL - 12/08/2014 - São Paulo, SP

Em 1611, Johannes Kepler sugeriu que a forma mais eficiente para empilhar esferas – como organizar laranjas para venda – seria em formato de pirâmide. Assim, possível inserir o máximo de esferas (ou frutas) em determinado volume.

Infelizmente, ele não conseguiu provar isto, mas agora um computador conseguiu verificar que a conjectura é mesmo verdade, acabando com séculos de debate.

Na verdade, Thomas Hales, da Universidade de Pittsburgh (EUA), desenvolveu uma prova para este problema em 1998. Mas ela tem trezentas páginas! 12 revisores levaram quatro anos para verificar se havia erros e, mesmo assim, eles deram apenas 99% de certeza de que a prova estava correta.

Então, em 2003, Hales começou a criar o projeto Flyspeck, uma ferramenta computacional para verificar sua prova. Ele usa dois programas, chamados Isabelle e HOL Light, que começam com algumas declarações lógicas facilmente verificáveis. Com isto, os programas podem verificar qualquer série de outras declarações lógicas, como uma prova matemática, se tiverem tempo suficiente.

Neste domingo, Hales e sua equipe anunciaram que as 300 páginas de prova foram analisadas pelos dois programas e, para seu alívio, está tudo correto. Em outras palavras, o computador verificou com êxito que a ideia apresentada por Kepler há mais de 400 anos está correta. “De repente eu me sinto dez anos mais jovem”, diz Hales � New Scientist.

Mas esta não é apenas uma boa notícia para Hales: seu trabalho demonstra que provas matemáticas – mesmo que absurdamente complexas – podem ser checadas por computadores, em vez de seres humanos. E centenas de provas como essas são produzidas a cada ano! É um alívio para os matemáticos.