„Čovek ne mora da veruje u Boga da bi bio matematičar, ali bi valjalo da veruje u Božiju knjigu“, tvrdio je mađarski matematičar Pol Erdoš, misleći pri tome na hipotetičku knjigu koju je predložio kao zbirku svih najlepših matematičkih dokaza koje nije moguće predstaviti jednostavnije.
Jedan od primera dokaza koji je „prepisan“ iz ove knjige bio bi sigurno Euklidov dokaz postojanja beskonačno mnogo prostih brojeva (deljivih samo sa sobom i jedinicom). Euklid je prvo pretpostavio suprotno, da postoji konačno prostih brojeva i najveći među njima označen sa P. Zatim je zamislio broj koji bi dobio tako što bi pomnožio sve proste brojeve N=2*3*5*…*P. Ukoliko bi tom broju dodao 1 jasno je da taj broj, N+1, ne bi bio deljiv ni sa jednim prostim brojem jer bi pri deljenju dao ostatak 1. Prema tome taj broj je takođe prost, a pri tom je veći od pretpostavljenog P što nam govori da nikada ne možemo pronaći najveći prost broj, odnosno mora ih biti beskonačno mnogo.
Za razliku od ideala lepog dokaza, koga se moguće ne bi postidelo ni sveznajuće biće, priča koja je počela davne 1852. godine iznedrila je jedan neočekivano drugačiji dokaz. Fransis Gutri je te godine tokom bojenja mape Engleske primetio da mu je za bojenje svih županija dovoljno samo 4 različite boje, a da se pri tom dve isto obojene županije ne dodiruju. Pitao se da li je svaku mapu moguće obojati sa samo 4 boje. Svoje otkriće je preko brata koji je studirao matematiku podelio sa profesorom Augustusom De Morganom zatraživši od njega objašnjenje. Profesor bi vrlo jednostavno mogao pokazati da pretpostavka nije tačna ukoliko bi pronašao samo jednu mapu za koju je potrebno 5 boja, a sa druge strane čak ni milioni mapa koje se mogu obojati sa 4 boje ne bi bile dokaz pretpostavke.
Objašnjenje je izostalo u narednih skoro 150 godina i na ovom problemu su lomili koplja mnogi veliki umovi. Kada je dokaz pronađen većina matematičara ga je dočekala razočarano zbog specifičnog postupka dokazivanja koji dokazu definitivno ne dozvoljava da se nađe u Božijoj knjizi. Kenet Apel i Volfgang Haken su 1976. godine problem razložili na 1936 mogućnosti pokrivši tako sve tipove mapa koje je moguće nacrtati. Sve te tipove su zatim uneli u računar i prepustili da računar da konačnu reč, a on je potvrdivši teoremu upisao kao prvu u zbirku teorema koje je dokazao računar.
