Keplerjeva domneva

Keplerjeva domnéva [képlerjeva ~] je v matematiki domneva o najgostejšem pakiranju krogel v trirazsežnem evklidskem prostoru. Po njej imata kubično ploskovno centrirano in šestkotniško gosto pakiranje kot razporeditvi enako velikih krogel v prostoru največjo srednjo gostoto. Gostota takšnih razporeditev je malo več kot 74 %.

Izvor problema

Slika iz Keplerjevega dela O šestoglati snežinki

Slika iz Keplerjevega dela O šestoglati snežinki

Prikaz kubičnega (levo) in šestkotniškega gostega pakiranja (desno). V kubičnem pakiranju posamezne vrste krogel niso poravnane (ABC), v šestkotniškem pa je tretja vrsta poravnana s prvo (ABA)

Razporeditev 35-ih krogel v obliki tetraedra je zgled šestkotniškega gostega pakiranja

Domnevo je leta 1611 podal Johannes Kepler v delu O šestoglati snežinki (Strena sue de nive sexangula). Kepler je začel raziskovati razporeditve krogel med svojim dopisovanjem s Thomasom Harriotom leta 1606. Harriot je bil prijatelj Walterja Raleigha, ki je postavil problem Harriotu o najboljši razporeditvi topovskih krogel na ladijskih krovih. Harriot je objavil delo o različnih vzorcih pakiranja leta 1591 in bil eden od pionirjev teorije o atomih.

Verjetni dokaz

Thomas Callister Hales, trenutno Mellonov profesor matematike na Univerzi v Pittsburghu, je leta 1998 podal dokaz Keplerjeve domneve. Njegov dokaz z grobo silo preverja posamezne primere s pomočjo računalnika in menijo, da je njegova pravilnost 99 %.

Ozadje problema

Problem obravnava velik zaboj z enako velikimi kroglami. Gostota razporeditve krogel je delež prostornine zaboja, ki jo zavzamejo krogle. Za največje možno število krogel v zaboju je treba poiskati razporeditev z največjo možno gostoto, da bodo krogle zapakirane najbližje kot se le da.

Poskusi kažejo, da naključno nalaganje krogel da gostoto približno 65 %. Še večjo gostoto je moč doseči s skrbnim postavljanjem krogel. Najprej se naložijo krogle v šestkotno mrežo, nato se nanje naložijo krogle v najnižje točke nad prvo vrsto. Na ta način so naložene na primer tudi pomaranče v trgovinah. Ta naravna razporeditev krogel da dva podobna vzorca pakiranja, kubično in šestkotniško. Obe razporeditvi imata povprečno gostoto:

${\frac {\pi {\sqrt {2}}}{6}}\approx 0,740480\!\,.$

Keplerjeva domneva trdi, da je to največja gostota. Nobena druga razporeditev krogel nima višje povprečne gostote.

Kasnejše obravnave problema

Kepler ni imel dokaza za svojo domnevo. Gauss je leta 1831 objavil delno rešitev. Dokazal je, da je Keplerjeva domneva resnična, če se krogle razporedijo v pravilno mrežo. To je pomenilo, da mora biti vsaka razporeditev, za katero Keplerjeva domneva ne bi veljala, nepravilna. Izločevanje nepravilnih razporeditev je zelo težko, zato je dokaz Keplerjeve domneve tako trd oreh. Dejansko obstajajo nepravilne razporeditve, ki imajo v dovolj majhni prostornini celo večjo gostoto od kubičnega pakiranja, vendar je gostota na večji prostornini vedno manjša.

Hilbert je dal problem leta 1900 na svoj seznam triindvajsetih nerešenih matematičnih problemov. Keplerjeva domneva je tretji del Hilbertovega osemnajstega problema.

László Tóth je leta 1953 pokazal, da se lahko problem določanja največje gostote porazdelitev (pravilnih in nepravilnih) prevede na končno (vendar zelo veliko) število računanj. To je pomenilo, da je dokaz z grobo silo načeloma izvedljiv. Tóth je uvidel, da lahko dovolj hiter računalnik ta teoretični rezultat obrne v praktični pristop k problemu.

Medtem so poskušali poiskati zgornjo mejo za največjo gostoto poljubne razporeditve krogel. Rogers je leta 1958 podal vrednost zgornje meje približno 78 %. Tudi drugi matematiki so to vrednost še malo znižali, vendar je bila še vedno precej višja od gostote 74 % kubičnega gostega pakiranja.

Podali so tudi nekaj nepravilnih dokazov. Fuller, znani ameriški arhitekt, je leta 1975 trdil, da ima dokaz, vendar so kmalu ugotovili, da je napačen. V letu 1993 je Hsiang z Univerze Kalifornije v Berkeleyju objavil članek, v katerem je trdil, da je s pomočjo geometrijskih metod dokazal Keplerjevo domnevo. Nekateri so trdili, da so bile nekatere navedbe premalo podprte. Čeprav niso našli nič nepravilnega v Hsiangovem delu, so dosegli dogovor, da je njegov dokaz nepopoln. Eden od najbolj glasnih kritikov je bil Hales, ki je tedaj delal na svojem dokazu.

Halesov dokaz

Hales je, tedaj na Univerzi Michigana v Ann Arborju, prek Tóthovega pristopa ugotovil, da je moč največjo gostoto vseh razporeditev najti z najmanjšo mejo funkcije s 150 spremenljivkami. V letu 1992 je s pomočjo asistenta Samuela Fergusona začel raziskovalni program s sistematično obravnavo metod linearnega programiranja za ugotavljanje spodnje meje vrednosti te funkcije za vsako množico od več kot 5000 različnih možnih razporeditev krogel. Če bi se lahko našla spodnja meja (za funkcijsko vrednost) za vsako od teh razporeditev in bi bila večja od funkcijske vrednosti za kubično gosto pakiranje, bi bila Keplerjeva domneva dokazana. Iskanje spodnjih mej za vse primere je obsegalo približno 100.000 problemov linearnega programiranja.

V letu 1996 je Hales navedel, da je konec projekta na obzorju, vendar bo morda zahteval »še eno ali dve leti«. Avgusta 1998 je najavil, da je dokaz končan. V tej fazi je vseboval 250 strani opomb in 3 gigabajte računalniških programov, podatkov in razultatov.

Navkljub neobičajni naravi dokaza so se uredniki Annals of Mathematics odločili, da ga bodo objavili. Sprejel ga je odbor dvanajstih odbornikov. Leta 2003 je po štirih letih dela vodja odbora Gábor Tóth (sin Lászla Tótha) poročal, da je verjetnost pravilnosti dokaza 99 %. Odbor ni mogel potrditi pravilnost vseh računalniških izračunov. Februarja 2003 je Hales objavil 100-stranski članek v katerem je podrobno opisal neračunalniški del svojega dokaza.

Annals of Mathematics bo objavila teoretični del Halesovega dokaza. Računalniški del bo objavljen v posebni reviji Discrete and Computational Geometry.

Strogi dokaz

Hales je januarja 2003 začel s skupnih projektom za izdelavo popolnega strogega dokaza Keplerjeve domneve. Cilj projekta je točno določiti veljavnost dokaza s strogim dokazom, ki bi ga bilo mogoče preveriti s samodejnim programom za preverjanje dokazov kot je na primer HOL. Projekt se imenuje Project FlysPecK, kjer F, P in K pomenijo začetnice za Formal Proof of Kepler. Hales ocenjuje, da bo celoten strogi dokaz zahteval približno 20 let dela.