Svaku kartu na kojoj se države dodiruju moguće je obojiti s četiri boje tako da nijedne dvije susjedne ne dijele istu. Tvrdnju je 1852. postavio Francis Guthrie, a dokazana je tek 1976., i to računalom.
Sada postoji novi dokaz. Potpisuju ga Mikkel Thorup sa sveučilišta u Kopenhagenu, Carsten Thomassen s danskog Tehničkog sveučilišta, Ken-ichi Kawarabayashi s japanskog Nacionalnog instituta za informatiku, Bojan Mohar sa Simon Fraser sveučilišta te Yuta Inoue i Atsuyuki Miyashita. Rad je objavljen u ožujku, a predstavlja se u studenom na konferenciji Foundations of Computer Science.
Zašto je stari dokaz bio sporan
Kenneth Appel i Wolfgang Haken 1976. su problem sveli na 1482 slučaja i svaki provjerili računalom. Matematičari su se tada podijelili: dokaz koji nijedan čovjek ne može pročitati u cijelosti mnogima nije izgledao kao dokaz. Godine 1997. broj slučajeva spušten je na 633, ali računalo je ostalo.
Novi dokaz ima ih više, 8202, pa na prvi pogled izgleda kao korak unatrag.
Gdje je onda napredak
U brzini bojenja. Stari postupak je za graf s n čvorova trebao red veličine n na kvadrat koraka, novi n log n. Na karti s tisuću područja to je razlika između milijun i tri tisuće koraka.
To teorem prebacuje iz kategorije dokazanog u kategoriju upotrebljivog. Bojenje grafa nije samo pitanje karata: isti postupak raspoređuje frekvencije odašiljačima, smjene radnicima i registre u prevoditelju programskog jezika.
Quanta ne navodi je li dokaz formalno provjeren. Priča je počela 2015. na danskoj plaži, gdje su Kawarabayashi i Thorup počeli razgovarati o problemu.
