Matemático resolve o problema depois de 400 anos

Por , em 12.08.2014

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]

1 Star2 Stars3 Stars4 Stars5 Stars (4 votos, média: 4,25 de 5)

7 comentários

  • Fernando Sakugava:

    Mais eficiente em qual sentido? Menor espaço? Mais resistente? Mais fácil de montar?

    • Cesar Grossmann:

      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.

    • Eric M. Souza:

      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.

    • Marcell Chaveiro Silva:

      Menor espaço sem estragar a fruta.

  • Eneida Melo:

    E quantos revisores revisaram o software?

  • Cesar Grossmann:

    O trabalho inverso será possível também? Criar provas matemáticas para conjecturas automaticamente?

Deixe seu comentário!