Računalnik (končno) dovolj dober za pravoveren matematični dokaz

Leta 1976 sta dva matematika, Appel in Haken, dokazala več kot sto let star problem barvanja zemljevidov (zanima nas najmanj koliko barv moramo uporabiti, da za vsako "državo" velja, da se z nobeno izmed sosed ne ujema v barvi, torej da se nikjer ne stikata dve enako obarvani). No, skoraj dokazala. Težava je bila v tem, da sta pravzaprav le omejila prostor rešitev in nato nad preostanek nagnala računalnik. Čudo tehnike je mlelo in mlelo ter na koncu izplunilo 4 (zavedam se, da do 42 manjka samo ena 2, ampak vseeno se pretvarjajmo, da je podobnost povsem naključna).

Vse lepo in prav, če se v dvatisoč in še nekaj letih matematika ne bi že malo izrodila in začela težiti k (platonski) popolnosti. Po svoje imajo puristi prav. "Zavihajmo rokave in upajmo na najboljše" pristop se vsekakor ne more meriti z eleganco nekajvrstičnih dokazov. Ako bi to novico pisal nekaj dni nazaj, bi mi preostalo le še, da zapadem v že tisočkrat prežvečene debate, češ, je indukcija sprejemljivo orodje? Smo lahko gotovi, da dani program kje ne skriva enklave ščurkov? In tako naprej, nazaj, okoli ovinka in po hribu navzgor vse do zgodnjih jutranjih ur.

Ampak vse to je preteklost! Gonthier in Werner sta dokaz, torej algoritem uporabljen za preiskovanje prostora rešitev, prenesla ("prenesla" se morda ne sliši kot kdo ve kakšen dosežek, ampak v resnici zahteva popolno abstrakcijo tako problema kot rešitve, kar ni mačji kašel) v Coq, jezik za preverjanje logičnih izjav. Pravovernejšega dokaza od povsem abstraktnega formalno-logičnega sistema si težko zaželimo. V kolikor v njunem delu ne najdejo kakšne resne napake, s tem kritikom računalnikov ne ostane več veliko streliva.

Rezultat sam ni pretirano presunljiv, Appel in Haken sta imela prav. Precej bolj presunljive so možnosti, ki jih orodja kot je Coq odpirajo. Microsoft (Gonthier je zaposlen v njihovem raziskovalnem centru na Cambridgu) tako namerava s formalizacijo programske logike zdesetkati populacijo hroščev v svojih izdelkih še preden jih prvič prevedejo.

Na novico nas je opozoril snow. Naj mu vsi hrošči v kodi poginejo!