400 anos em busca da melhor maneira de empacotar laranjas
Resolução do problema, verificável por computador, foi publicada em 2017
No início do século 17, a Inglaterra estava desbancando portugueses, espanhóis, franceses e holandeses para se tornar império global.
Logo a marinha britânica dominaria os sete mares com a ajuda de seus canhões. E, dado que o espaço a bordo é escasso, como armazenar as balas de canhão para poder levar o maior número possível delas no navio?
O problema chegou até o matemático e astrônomo alemão Johannes Kepler (1571 – 1630), que o divulgou em trabalho publicado em 1611: se alguém pretende colocar bolas pequenas idênticas em um recipiente grande (por exemplo, laranjas em um caixa), como posicionálas de modo que caiba o maior número possível de bolas?
Kepler é conhecido sobretudo por seu trabalho em mecânica celeste. A partir das observações realizadas pelo dinamarquês Tycho Brahe (1546 – 1601), seu mentor e astrônomo oficial do Império Romano-Germânico, Kepler formulou as três leis que levam seu nome: planetas se movem em órbitas elípticas; o Sol ocupa um dos focos da elipse e a reta que liga o planeta ao Sol percorre áreas iguais em tempos iguais. Esse trabalho influenciou Isaac Newton na formulação da lei da gravitação universal.
Se as bolas forem colocadas aleatoriamente, a densidade do empacotamento (percentagem do volume de caixa ocupado pelas bolas) será cerca de 65%. É possível fazer melhor, colocando as bolas em uma disposição hexagonal, como feirantes exibem frutas em suas barracas. Nesse caso, a densidade é cerca de 74%.
Kepler conjecturou que isso é o melhor possível, mas não sabia provar. Apesar de a questão ter sido incluída (em 18º) na famosa lista de 23 problemas apresentada por David Hilbert no Congresso Internacional de Matemáticos de 1900, praticamente não houve progresso até meados do século 20.
Em 1953, o húngaro László Fejes Tóth (1915 – 2005) mostrou que o problema pode ser reduzido a um número finito (mas enorme) de cálculos, ao alcance de um computador suficientemente poderoso. Em 1998, o americano Thomas Hales anunciou ter feito tais cálculos. Mas seu trabalho era demasiado longo (250 páginas mais 3 gigabytes de código de computador): os 12 consultores encarregados de verificá-lo desistiram após quatro anos de trabalho.
Então Hales juntou uma equipe para produzir uma prova formal da conjectura, que pudesse ser verificada automaticamente por computador. O resultado dessa colaboração foi aceito para publicação em 2017, encerrando finalmente mais de quatro séculos de esforços.