Publicado artigo que prova a conjectura de Kepler, problema matemático não resolvido por 400 anos
Tradução e adaptação do EurekAlert!
(Imagem: o professor Hales demonstrando a solução para a conjectura. Crédito: Bob Kalmbach / Universidade de Michigan.)
Uma equipe liderada pelo matemático Thomas Hales entregou uma prova formal da Conjectura de Kepler, a qual é a resolução definitiva de um problema que tinha ficado sem resolver por mais de 300 anos. O artigo está agora disponível online no Forum of Mathematics, Pi, um periódico de acesso aberto publicado pela Cambridge University Press, a editora da Universidade de Cambridge. O artigo não apenas soluciona um problema matemático secular, mas é também um grande avanço na verificação de provas matemáticas complexas por meio de computadores.
A Conjectura de Kepler era um problema famoso da geometria discreta, que demandava pela maneira mais eficiente de empilhar esferas em um dado espaço. A resposta, apesar de não ser difícil de se supor (é exatamente como as laranjas são empilhadas no supermercado) tinha sido notavelmente difícil de provar. Hales e Fergunson anunciaram originalmente a prova em 1998, mas a solução era tão longa e complicada que um time de uma dúzia de revisores passou anos trabalhando e checando o artigo antes de desistir.
Segundo Henry Cohn, editor do Forum of Mathematics, Pi: “o veredito dos revisores era de que a prova parecia funcionar, mas que eles simplesmente não tinham o tempo e a energia para verificar tudo de forma detalhada. A prova foi publicada em 2005, e nenhum erro irreparável tinha sido identificado, mas era uma situação insatisfatória que a prova estivesse aparentemente além da habilidade da comunidade matemática de checá-la por completo. Para resolver essa situação e estabelecer uma certeza, Hales apelou para os computadores, usando técnicas de verificação formal. Ele e seu time de colaboradores escreveram a prova inteira em extraordinário detalhe usando uma lógica formal estrita, que foi checada por um programa de computador com perfeito rigor. Este artigo é o resultado do seu trabalho finalizado”
O artigo, de acesso livre, pode ser visto e baixado em:
A FORMAL PROOF OF THE KEPLER CONJECTURE ( Forum of Mathematics, Pi)
Para entender melhor a Conjectura de Kepler:
A dúvida do canhoneiro, Carmen Kawano – Revista Galileu
Referência