Računalno potpomognuti matematički dokazi nisu novost. Na primjer, računala su korištena za potvrdu takozvanog 'teorema četiri boje'. U kratkom izdanju, 'Računalni dokaz' Američko matematičko društvo (AMS) izvješćuje da je objavilo posebno izdanje jednog od svojih časopisa posvećeno računalno potpomognutom dokazi. 'Četiri članka Obavijesti istražuju trenutno stanje umjetnosti formalnog dokaza i pružaju praktične smjernice za korištenje računalnih pomoćnika za dokaz.' I kao što je rekao jedan od uključenih istraživača, 'takva zbirka dokaza bila bi slična slijedu matematičkog genoma.' Ali čitajte više...
Računalno potpomognuti matematički dokazi nisu novost. Na primjer, računala su korištena za potvrdu takozvanog 'teorema četiri boje'. U kratkom priopćenju 'Dokaz kompjuterski,' Američko matematičko društvo (AMS) izvještava da je objavilo posebno izdanje jednog od svojih časopisa posvećeno računalno potpomognutim dokazima. 'Četiri Obavijesti članci istražuju trenutno stanje umjetnosti formalnog dokaza i pružaju praktične smjernice za korištenje računalnih pomoćnika za dokaz.' I kao rekao je jedan od uključenih istraživača, 'takva zbirka dokaza bila bi slična sekvenciranju matematičkog genoma.' Ali čitajte više...
Pogledajmo prvo kako su se matematički teoremi dokazivali u prošlosti. "Kada matematičari dokazuju teoreme na tradicionalan način, oni iznose argument u narativnom obliku. Pretpostavljaju prethodne rezultate, prešućuju detalje za koje misle da će ih drugi stručnjaci razumjeti, koriste prečace kako bi prezentaciju učinili manje zamornom, pozivaju se na intuiciju itd. Ispravnost argumenata utvrđuje se pomnim ispitivanjem drugih matematičara, u neformalnim raspravama, na predavanjima ili u časopisima. Otrežnjujuće je shvatiti da je način kojim se verificiraju matematički rezultati u biti društveni proces i stoga je pogrešiv."
Zbog toga se sada koristi koncept 'formalnog dokaza'. "Kako bi zaobišli te probleme, informatičari i matematičari počeli su razvijati područje formalnog dokazivanja. Formalni dokaz je onaj u kojem je svaki logički zaključak provjeren sve do temeljnih aksioma matematike. Matematičari obično ne pišu formalne dokaze jer su takvi dokazi toliko dugi i glomazni da bi bilo nemoguće da ih provjere ljudski matematičari. Ali sada se mogu dobiti 'pomoćnici za računalni dokaz' da obave provjeru. Posljednjih godina računalni pomoćnici za dokaze postali su dovoljno moćni za rukovanje teškim dokazima."
Ovdje je poveznica na ovo posebno izdanje časopisa Obavijesti Američkog matematičkog društva (prosinac 2008., svezak 55, broj 11).
Prvi članak je Formalni dokaz, autor Thomas Hales Sveučilišta u Pittsburghu (PDF format, 12 str., 512 KB). Evo prvog paragrafa. „Svakodnevno se suočavamo s greškama računala. Oni se ruše, vise, podliježu virusima, pokreću softver s greškama i skrivaju špijunski softver. Naši tabloidi izvještavaju o bizarnim računalnim greškama: pokrovitelju knjižnice koji je kažnjen s 40 trilijuna američkih dolara zbog zakašnjele knjige, jer se kao visina kazne skenira barkod; ili zubara u San Diegu kojemu je na kućni prag isporučeno više od 16 000 poreznih obrazaca kada je 'apartman' u svojoj adresi skratio kao 'su'." Hales dodaje da "u prosjeku, programer uvodi 1,5 grešaka po retku tijekom tipkanja." Kao što sam napisao -- prilično dobro -- softver za superračunala dugi niz godina, mislim da je Halesova tvrdnja malo pretjerano.
Drugi članak je iz Georges Gonthier, od Microsoft Research, u Cambridgeu, Engleska, i zove se Formalni dokaz -- Teorem četiri boje (PDF format, 12 stranica, 2,58 MB). Uz ovaj vrlo tehnički dokument, ovdje su tri poveznice na članke o Wikipediji matematički dokazi, dokazi uz pomoć računala i teorem o četiri boje.
Treći članak je napisao John Harrison, koji radi za Intel Corporation. Ovdje je poveznica na Formalni dokaz -- teorija i praksa (PDF format, 12 stranica, 151 KB).
Evo prvog paragrafa. "Formalni dokaz je dokaz napisan preciznim umjetnim jezikom koji dopušta samo fiksni repertoar stiliziranih koraka. Ovaj formalni jezik obično je dizajniran tako da postoji čisto mehanički proces kojim se može provjeriti ispravnost dokaza u jeziku. U današnje vrijeme postoje brojni računalni programi poznati kao pomoćnici za dokaz koji mogu provjeriti ili čak djelomično konstruirati formalne dokaze napisane na njihovom preferiranom jeziku za dokaz. Oni se mogu smatrati praktičnim, računalnom realizacijom tradicionalnih sustava formalne simboličke logike i teorije skupova predloženih kao temelj za matematiku."
Četvrti članak ovog specijala Obavijesti pitanje se zove Formalni dokaz -- početak, autor Freek Wiedijk sa Sveučilišta Radboud, Nijmegen, Nizozemska (PDF format, 7 stranica, 153 KB).
Ako ste matematičar ili informatičar, ova četiri članka morate pročitati.
Izvori: priopćenje za javnost Američkog matematičkog društva, 6. studenog 2008.; i razne web stranice
Povezane priče pronaći ćete slijedeći donje veze.
-
Računala
-
Obrazovanje
-
Matematika
-
Znanost
-
Softver