1611-ben Johannes Kepler azt állította, hogy a gömb alakú dolgokat, mint amilyen a narancs vagy a sárgadinnye, gúla vagy piramis alakba érdemes rendezni, ám a német matematikus elméletét nem tudta bizonyítani.

A probléma Thomas Hales-t, a Pittsburghi Egyetem professzorát sem hagyta nyugodni. A szakember 1998-ban 300 oldalas bizonyítást  írt, melyet 12 opponens nézett át, és négy évnyi elemzés és alapos vizsgálat után is csak 99 százalékos bizonysággal merték kijelenteni, hogy a matematikus elmélete helyes.

Most, Kepler felvetése után 403 évvel egy számítógépes program segítségével kiderült, hogy a tudós nem tévedett - írja a New Scientist.

Hales ugyanis nem adta fel, és 2003-ban elkezdett fejleszteni egy számítógépes programot, mellyel alá tudja támasztani igazát. A Flyspeck névre keresztelt program két egyszerű szoftverrel működik, melyek bizonyos idő alatt képesek bonyolult matematikai elméletek logikai állításait ellenőrizni.

Hales professzor és csapata vasárnap bejelentette, hogy '98-as elméletét megvizsgálta a program, és nem talált benne hibát. A tétel tehát helyes. "Hirtelen 10 évet fiatalodtam" - nyilatkozta a New Scientistnek.

A szakma is üdvözölte a Flyspecket. "Hatalmas munka volt" - nyilatkozta Alan Bundy, az Edinburghi Egyetem munkatása, aki nem vett részt a program fejlesztésében. Mint mondta, bízik benne, hogy Hales sikere más matematikusokat is arra fog ösztönözni, hogy hasonló segístéggel éljenek.

A szakember a portálnak elmondta, hogy ideális esetben a helyességbizonyító eszközök a háttérben dolgoznak, míg a matematikusok új ötleteket próbálnak ki. A szoftverek már néhány alapvető tételt önmagukban is tudnak bizonyítani, de lehetnének könnyebben használhatóak. "Valamilyen megoldásra van szükségünk, hogy felfedezzük a bizonyítást, úgy, hogy közben átfogó képet kapjunk", mondja Bundy. "Hogy mindent a legapróbb részletig átlássunk, az egyszerűen túl van a képességeinken, az emberek képtelenek ennyi információt befogadni."