Keplerjeva domneva: problem se je končno rešil po 400 letih

Leta 1611 je nemški fizik, matematik in astronom Johannes Kepler predlagal, da bi bil najboljši način za zlaganje sferičnih predmetov - na primer sadja -, da jih razporedimo v obliki piramide. Vendar ni mogel dokazati, da ima prav, in ta enigmatična težava je sčasoma postala znana kot "Keplerjeva zamisel."

Kajti po poročanju New Scientist je ameriški matematik Thomas Hales leta 1998 sporočil, da je lahko dokazal, da je Keplerjev predlog pravilen. Takrat se je Hales opiral na matematično metodo izračunavanja vseh možnih možnosti izrek, da pride do rešitve.

Računi in več računov

Na podlagi te metode je Hales menil, da obstajajo neskončni načini, kako sferične predmete neskončno zlagati, večina pa je dejansko le nekaj tisoč možnosti. Tako je matematik težavo razdelil na tisoče načinov organizacije sferičnih predmetov, ki so matematično predstavljali neskončne možnosti dogovorov, in vse te podatke vrgel v programsko opremo za izračune.

Rezultat je bil majhen nabor strani na 300 strani, ki je potreboval štiri leta, da jih je 12 pregledovalcev v celoti preverilo! A tudi po toliko dela matematiki niso bili povsem prepričani, da so izračuni pravilni, trdijo, da so le 99 odstotkov prepričani, da Halesova rešitev resnično podpira Keplerjev predlog.

Končno 100% prepričan

No, saj veste, da "99% prepričan" ni dovolj za matematiko, kajne? Leta 2003 je Hales začel s projektom dokazovanja svojih izračunov, pri čemer je uporabil dve uradni verifikacijski programski opremi - Isabelle in HOL Light - za pregled svojega dela.

In ni, da so končno prišli do zaključka! Minulo nedeljo, 10. avgusta, je Halesova ekipa sporočila, da so po prevajanju goste matematike, ki je bila prisotna na 300 straneh izračunov iz leta 1998, v računalniški jezik, lahko ugotovili, da so bili izračuni pravilni. Z drugimi besedami, po toliko stoletjih - in letih prizadevanj Halesa in njegove ekipe - je Keplerjev predlog dokazan.

A dejstvo, da lahko Keplerjev duh končno počiva v miru - in Hales lahko svojo pozornost usmeri na še en zapleten problem - ni edina dobra novica v vsej tej zgodbi. To tehnologijo je mogoče uporabiti za preverjanje ogromne količine dela, ki se pojavi vsako leto, in matematike osvoboditi te nehvaležne naloge ter jim omogočiti, da se uporabijo čas za osredotočanje na druga vprašanja in sprostijo svojo ustvarjalnost za raziskovanje vesolja števil.