Keplers förmodan handlar om hur effektivt man kan packa sfärer i det tredimensionella rummet. Det finns två relativt uppenbara sätt att packa, en slags alternerande hexagonal konfiguration eller i en sida-mot-sida kubisk konfiguration (som när man staplar en pyramid). Dessa två är lika effektiva och fyller rummet till ca 74%. Kepler förmodade 1611 att det inte existerade mer effektiva packningsmetoder.
Detta bevisades inte förrän 1998 av Thomas Hales. Men beviset var över 300 sidor långt och inte ens när beviset efter noggrann kontroll publicerades år 2005, så kunde granskarna säga sig vara helt säkra på att det verkligen var korrekt. Hales startade då ett projekt för att formalisera beviset så att det skulle kunna verifieras av en specifik typ av programvara. Detta arbete är nu slutfört och beviset är datorverifierat.
»»» Proof confirmed of 400-year-old fruit-stacking problem [New Scientist]
»»» Keplers 400-åriga gåta löst [DN]
»»» Keplers förmodan [Wikipedia]