Matemático Resolve o problema de Kepler 400 anos depois......
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.
Os problemas de matemática que valem 1 milhão de dólares
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.
4 problemas infinitos
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.
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]
http://hypescience.com/matematico-resolve-o-problema-da-conjectura-de-kepler-depois-de-400-anos/?utm_source=feedburner&utm_medium=email&utm_campaign=Feed%3A+feedburner%2Fxgpv+%28HypeScience%29
Nenhum comentário:
Postar um comentário