Finalmente publicada solução definitiva e verificada de um problema matemático de mais de 300 anos!

Qual é o método mais eficiente de agrupar esferas no espaço de forma a ter uma densidade máxima, ou seja, ocupar o menor espaço possível?

Sim, intuitivamente, é fácil responder essa pergunta. Na verdade, quase todo supermercado utiliza essa resposta para organizar laranjas, por exemplo: empilha-se as mesmas na organização piramidal mostrada na imagem acima. Porém, provar isso matematicamente é um gigantesco desafio, sendo que a solução do problema só foi comprovada definitivamente somente este ano, através de uma prova formal publicada semana passada no Fórum dos Matemáticos, Pi, da Universidade de Cambridge (1).

Por mais de 300 anos esse problema matemático de geometria discreta (provar a melhor forma de comprimir bolas no espaço) ficou insolúvel e conhecido como A Conjectura de Kepler. Foi somente em 1998 que os matemáticos Thomas Hales e Samuel Ferguson anunciaram uma prova matemática solucionando o problema. Só que os cálculos utilizados eram tão complexos e grandes (espalhados por 100 páginas de trabalho) que matemáticos ficaram anos verificando a prova, parte por parte, mas acabaram desistindo de analisar tudo e decidiram que a prova provavelmente estava certa, já que nenhum erro tinha sido encontrado. Então, em 2005, Hales publicou oficialmente a solução (2).

Porém, ficou aquele desconforto de não se saber, 100%, se a complexa solução matemática encontrada para a Conjectura de Kepler estava realmente correta. Então Hales, e colaboradores, resolveram utilizar técnicas computacionais de "verificação formal" para destrinchar todos os cálculos matemáticos da prova final e garantir a inexistência de erros. Para impedir erros computacionais, também foi desenvolvido mecanismos de segurança para os cálculos de lógica formal estrita efetuados pelos computadores.

O projeto de verificação computacional levou bastante tempo para ser concluído e só foi completado há alguns anos, com sucesso. Através da maior e mais complexa prova de um teorema matemático verificado por computadores, a Conjectura de Kepler ganhou sua solução matemática inquestionável (1). Além de finalmente resolver de uma vez por todas um problema de séculos, a técnica computacional otimizada de verificação formal poderá ser uma grande ferramenta de ajuda para todos os matemático no mundo, facilitando bastante a segurança na resolução de cálculos.

(1) Publicação da prova formal: https://doi.org/10.1017/fmp.2017.1

(2) Solução publicada em 2005: http://annals.math.princeton.edu/wp-content/uploads/annals-v162-n3-p01.pdf

Referência adicional: http://blog.journals.cambridge.org/2017/06/12/proving-the-kepler-conjecture/