Matemático resolve o problema depois de 400 anos
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]
7 comentários
Mais eficiente em qual sentido? Menor espaço? Mais resistente? Mais fácil de montar?
Tem uma página no Wolfram sobre a Conjectura de Kepler:
http://mathworld.wolfram.com/KeplerConjecture.html
Pelo que eu entendi, trata-se de eficiência no uso do espaço, ou seja, como empilhar de forma a maximizar o número de objetos esféricos em um determinado volume.
Também fiquei curioso. Se for empilhar ao “ar livre”, de fato parece ser lógico em pirâmide, senão fica tudo espalhado pelo chão.
Menor espaço sem estragar a fruta.
E quantos revisores revisaram o software?
Acho que esta informação você encontra na página do FlySpeck:
https://code.google.com/p/flyspeck/
O trabalho inverso será possível também? Criar provas matemáticas para conjecturas automaticamente?