No início do século 17, a Inglaterra estava desbancando portugueses, espanhóis, franceses e holandeses para tornar-se o império global. Logo a marinha britânica dominaria os sete mares, claro, com a ajuda de seus canhões. E, dado que o espaço a bordo é escasso, como armazenar as balas de canhão de modo a poder levar o maior número possível 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 movem-se em órbitas elípticas; o Sol ocupa um dos focos da elipse; 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, por exemplo, 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 realizado 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 4 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.