1611-ben Johannes Kepler kitalált egy megoldást arra a fontos problémára, hogy milyen alakzatba is érdemes pakolni a gömb formájú dolgokat, például a narancsot (bár Kepler korában talán inkább az ágyúgolyó lett volna a legjobb példa). A tudós azt mondta, hogy a piramisforma (bár matematikában a gúla a pontos megnevezés) a legjobb módszer, de az igazát nem tudta bizonyítani. Most, 403 évvel később egy számítógépes szimuláció eredménye alapján igaza volt.

Valójában a tételt már 1998-ban bizonyította egy Thomas Hales nevű figura a Pittsburgh-i Egyetemről, de ott is volt egy kis baj: Hales 300 oldalas bizonyítását 12 opponens nézte át, és négy év vizsgálódás után is csak 99 százalékos bizonysággal merték azt mondani, hogy a tudós nem tévedett. Hales valószínűleg kicsit bepöccent, mert 2003-ban elkezdett fejleszteni egy Flyspeck nevű programot, egy olyan szimulációt, ami végre minden kétséget kizáróan igazolja, hogy neki és Keplernek van igaza.

A projekt két olyan, egyszerű szoftveren alapszik, amik alapszintű logikai állítások alapján dolgozva mindenféle egyéb logikai állítás valóságtartalmát meg tudják állapítani, ha hagyják őket egy kicsit gondolkozni.

Múlt vasárnap Hales és munkatársai bejelentették, hogy végeztek a 300 oldalas bizonyítás betáplálásával, és a programok nem dobtak hibát, tehát az állítás igaz: ha kerek dolgokat akarunk tárulni, pakoljuk azokat piramis formájú halomba. „Mintha tíz évet fiatalodtam volna” – kommentálta Hales a végeredményt a New Scientistnek adott interjújában. A kutató egyébként a bizonyítást jelentős részben egy magyar matematikus, Fejes-Tóth László tanulmányaira építve végezte el.