komu bol'she very?
V smysle, kompjuteru ili cheloveku? Vot tut v 2001 godu, a na dnjax eshhe vot tut, byli interesnye besedy o "kompjuternyx" dokazatel'stvax. Sobstvenno, tam vse uzhe i skazali, vo vsex vozmozhnyx sochetanijax. No filosovstvovat' - eto ne matematikoj zanimat'sa, tut povtorjat' mozhno i nuzhno (a ne povtorit' kogo-to - prakticheski nevozmozhno:) ).


1. V smysle nadezhnosti (garantii ot oshibok) - kompjuter dast cheloveku 100 ochkov vpered.
Oshibki zheleza voobshhe mozhno ne schitat': oni sluchajny i potomu bessmyslenny. Takaja oshibka ne privodit k nevernomu otvetu - ona privodit k otsutstviju otveta. Sluchajno gde-to smenilsa bit vo vremja vypolnenija tipichnoj operacii: "vzjat' sed'moj bajt ot adresa v registre R1, pribavit' ego k registru R2, razymenovat', otschitat' 24 bajta i peredat' upravlenie po tomu adresu, chto tam napisan" - da zavisnet vse, ili eshhe kak-nibud' slomaetsa.
Oshibki cheloveka gorazdo opasnee: oni osmyslenny. Poetomu, naprimer, verojatnee, chto drugoj chelovek, chitaja, povtorit tu zhe oshibku. A esli rassuzhdajut "ot protivnogo" (kak v 99% dokazatel'stv) - vovse koshmar. Ljubaja sluchajnaja oshibka v konce koncov privedet k kakomu-to protivorechiju, i tut zhe "Ura! Contrary to (37), we have so-and-so, and this contradiction proves the theorem". Imenno tak v svoe vremja chut' ne upustili nekotorye sporadicheskie konechnye prostye gruppy.
Oshibki pri prevrashhenii algoritma, rasskazannogo v statje na estestvennom jazyke, v programmu - gde-to poseredke po stepeni opasnosti. V osnovnom eto budut obschety na 1 (tipa "repeat" vmesto "while") i nepravil'no inicializirovannye peremennye - i vse oni, skoree vsego, budut otlovleny, ibo privedut k bessmyslennomu povedeniju na testovyx zadachkax.

2. O "konceptual'nom" vozrazhenii.
Ono vovse ne rabotaet, kogda kompjuter primenjaetsa kak bol'shoj kal'kuljator: naprimer, dlja dlinnyx simvol'nyx vykladok. Nu razve chto chelovek, znaja, chto Maple vse soschitaet, polenitsa zametit', chto v formule mozhno vynesti (x-x), i poluchit pravil'nyj otvet 0, no ne pojmet, pochemu. Togda sam on i postradaet: esli b zametil, to i text vyshel by elegantnee, a to i smog by uvidet' i dokazat' chto-nibud' novoe.
Xuzhe, kogda komputer nuzhen dlja bol'shogo perebora. No tut uzhe nichego ne podelaesh'. Mne neskol'ko raz prixodilos' delat' bol'shoj perebor: nikakix somnenij, chto poluchen vernyj rezul'tat, no oshhushhenie neudovletvorennosti ostaetsa.
Otsjuda - populjarnoe i poleznoe zanjatie: prodolzhat' iskat' beskomputernye dokazatel'stva.

K tomu zhe, kogda otvet izvesten, legche ponjat', pochemu on imenno takoj. U menja est' mechta (uvy, nevypolnimaja, kompy ne potjanut): chtoby v rezul'tate bol'shogo perebora kompjuter vydal matricu smezhnosti gipoteticheskogo "grafa Aschbachera" (nikto ne znaet, sushhestvuet li on). I vot - prostynja 3250x3250, zapolnennaja nuljami i edinicami. I polzajut po nej matematiki, pytajas' ponjat', po kakoj prichine etot graf sushhestvuet. I ved' pojmut zhe! I ponimanie privedet k novym teoremam.

3. Iskusstvennyj intelljukt.
A vsjakie nadezhdy, chto kompjutery budut naxodit' dokazatel'stva novyx teorem, i straxi po etomu povodu - eshhe bespochvennee, chem moja mechta. Vot razve chto molekuljarnye biologi nauchat dlinnye belki sochetat'sa po pravilu Modus Ponens: togda budet interesno. No chto-to mne kazhetsa, chto dazhe takogo parallelizma (porjadka chisla Avogadro) - ne xvatit, chtob v rastvore stali pojavljat'sa novye i interesnye teoremy.

4. Monstry.
A tablichku "here there be tygers" nado vyveshivat' sovsem v drugom meste. Bez vsjakix komputerov pojavljajutsa dokazatel'stva gorazdo somnitel'nee, chem prostoj i ponjatnyj perebor v probleme 4x krasok.
Menja trevozhit sud'ba klassifikacii konechnyx prostyx grupp (v nej komputery ispol'zovalis' marginal'no). I ne to strashno, chto nekotorye kuski dokazatel'stva eshhe ne napisany. Xuzhe, chto ix, vozmozhno, tak i ne napishut. Eshhe xuzhe, chto sovsem malo narodu ponimajut strukturu dokazatel'stva v celom. Eshhe xuzhe, chto eto chislo umen'shaetsa (umerli Gorenstein i Suzuki).
A s objavleniem (v 79m?..) o tom, chto vse dokazano, interes stal padat', bol'shinstvo klassifikatorov razbrelis', novye ne pojavljajutsa. Eshhe let cherez 20 mozhet stat'sa, chto ni odin chelovek na zemle ne budet znat', pochemu zhe vse-taki net drugix konechnyx prostyx grupp. Budut rasskazyvat' legendy o "velikix drevnix", kotorye znali pochemu, i zapisali dokazatel'stvo, no ix znanie - i umenie eto dokazatel'stvo chitat' - bezvozvratno uterjany...

CFSG - eto krajnij primer, no ne edinstvennyj. U nas v grafax est' nedavnee dokazatel'stvo gipotezy Mengera (Robertson & Seymour), 17 statej po 50-100 stranic, i ja podozrevaju, chto ponimajut ego - to est', s chistoj sovestju mogut skazat' "Da, eto dokazatel'stvo" - vsego troe. Ja kak-to rasskazyval na seminare, v podrobnostjax, odnu iz etix 17 glav, i mogu za nee ruchat'sa. No skepticizma eto mne tol'ko pribavilo.


Voprosy, kommentarii?