Samozrejme, počítač nám i v tom pomáha. Nepriamo, ako každému, pri vyhľadávaní potrebných informácií, alebo keď treba preskúmať veľa prípadov či situácií. No základným postupom matematického poznávania je exaktné overenie – tvrdenia treba dokázať a nielen štatisticky podporiť.
Veď čo z toho, ak ani ten najvýkonnejší počítač nenašiel ani počas rokov výpočtov protipríklad pre nejaké tvrdenie – stále to ešte nie je dôkaz, že tvrdenie platí. Iná je situácia, ak by sme vedeli dokázať, že stačí preskúmať obmedzenú množinu kandidátov. Takáto situácia nastala v roku 1976, keď Kenneth Appel a Wolfgang Haken vyriešili Teorému štyroch farieb (zjednodušená formulácia: vystačíme so štyrmi farbami na vytlačenie ľubovoľnej politickej mapy).
Vo svojom dôkaze ukázali, že stačí preskúmať množinu 1¤936 máp – a to už zverili počítaču. Matematikom sa ich dôkaz nie celkom pozdával, keďže bol založený na viere, že algoritmus, jeho implementácia (program) a počítač, na ktorom sa vykonal, boli bezchybné. Niekto si môže povedať, že čo sú to za pochybnosti v čase, keď počítače riadia celý svet – metro pod zemou, vlaky a elektrárne na zemi a lietadlá nad hlavou. Veríme im a tu zrazu pochybnosti pri neporovnateľne jednoduchšej (a pre kartografiu bezvýznamnej) úlohe. No ale matematika je už taká.
Hádam väčšinu pochybovačov presvedčili v septembri 2004 Georges Gonthier a Benjamin Werner, ktorí teorému dokázali – síce opäť pomocou počítača, no tentoraz ho použili inak. Využili špeciálny softvér pomáhajúci pri dokazovaní – napr. overuje a zjednodušuje jednotlivé kroky (koho to zaujíma, volá sa Coq a je vyvíjaný na viacerých francúzskych akademických pracoviskách).
Nedávno, 20. septembra, Georges Gonthier oznámil ďalšiu významnú aplikáciu systému Coq. Po šiestich rokoch práce sa podarilo formálne dokázať Feit-Thompsonovu teorému (každá konečná grupa nepárneho rádu je riešiteľná). Pôvodný, 50 rokov starý dôkaz mal niekoľko sto strán. Počítačový „dôkaz“ má síce tiež úctyhodných 170-tisíc riadkov, použilo sa v ňom 15-tisíc pomocných definícii a 4 300 teorém, no je overený systémom Coq.
Na jednej strane by sa mohlo namietať, že vlastne žiadne nové poznanie táto práca nepriniesla. Lenže ono to zas nie je vôbec málo. Koľko dôkazov je takto precízne preverených? Zvlášť keď sú dlhé a neriešia nejaký vychytený problém či nevedú k veľmi nečakanému záveru? Vtedy záleží len na pár (omylných) recenzentoch, akú námahu budú anonymne a bezplatne venovať ich overovaniu. Pochybnosti sú na mieste. Teraz sa otvárajú nové možnosti. No, ale aby som tomu zas na záver predsa len trochu ubral z optimizmu – formálnu správnosť Coq systému (softvér plus hardvér) ešte nikto nedokázal. Ostatne, rovnako ako neomylnosť recenzentov.
