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

Matev, sigurno da izrek ni točen, 100 let velja, zdej si mu pa ti nasprotno dokazal ko si našu 5 držav, najbrž se še nihče ni spomnu tega...no dej, resno, vzemi 5 točk, in vsako poveži s vsako, brez da bi se kje povezave sekale. Potem izrek ne bo točen. Pa pozabte na zemljevid noo, se sploh ne gre za to.

To je pa že DRUG problem, ne vem kakšna je rešitev, niti če je znana.

V originalno zadanem problemu 4 barv nikakor ne. Stik se šteje po robu, v oglišču se lahko stika poljubno ploskev.

Dejmo ostat na originalno zadanem problemu, pa razumimo najprej to! Pol gremo mogoče naprej. OK?

Def: Barvanje vozlišč grafa G je pravilno, če sta vsaki dve sosednji vozlišči različe barve. Najmanjše število barv, ki je potrebno za pravilno barvanje vozlišč grafa G, je kromatično število grafa G - Crom(G).

Primeri:

Crom( K_n ) = n
K_n...polni graf = tak, pri katerem velja, da sta katerikoli (različni) vozlišči sosednji => povezani med sabo (n...št. vozlišč)

Crom( neg-K_n ) = 1
neg-K_n...velja obratno kot pri polnem -> graf brez povezav (n...št. vozlišč)

Crom( P_n ) = { 1 , če n = 1 oziroma 2 , če n >= 2 }
P_n...pot dolžine n-1
Primer:
P_3 .... 0----0----0

Crom( C_n ) = { 2 , če n = sodo št. oziroma 3, če n = liho. št }
C_n...cikel z n vozlišči
Primer:
C_3 bi bil ekvivalenten trikotniku, katerega ogljišča so vozlišča grafa...

Crom( Q_d ) = { 1 , če d=0 oziroma 2, če d>=1 }
Q_d...hiperkocka dimenzije d
Primer:
Q_3 je ekvivalenten kocki (ali kvadru) katere ogljišča so vozlišča grafa...

Izrek štirih barv
G ravninski => Crom(G) manjše_ali_enako 4

Kaj pomeni da je graf ravninski?
..da ga lahko narišemo v R^2 (R - realna št.) tako, da se povezave ne sekajo, razen v skupnih krajiščih.

Tako...upam da je vsaj malo bolj jasno kaj pomeni barvanje grafov. V nasprotnem primeru pa svnčnik v roke in preizkusit tiste primerčke, ki sm jih napisal..

Kaj pomeni "v real lajfu uporaben"?

Da nekdo, z njegovo pomočjo, nareže in skisa repo za zimske južine?

Čudenje, kako so štiri barve zadosti za vsak ravniski in krogelni zemljevid, pa ne šteje nič? Ni to repa, niti podstavek za srebrno posodico za extra trpke sire?

Where do you draw the line?

Tudi alokacija registrov pri kompajlerjih, ja?

V resnici obstaja nek ground breaking aspekt tega teorema 4 barv.

Namreč to je prvi matematični teorem, katerega bistveni del je bil narejen zunaj človeških možganov, v računalniku.

Prvotni dokaz je bil tako obsežen, da ga noben matematični recenzent ni bil sposoben preverit. Ga še danes ni.

Raćunalniški program pa ja.

V tem je zgodovinskost (in s tem praktičnost) te zadeve.

Dokazov je bilo kar nekaj, za primer (če te zanima) si lahko pogledaš tegale. Samo ne me potem gnjavit kaj pomeni kaka reč, kako je to in ono izpeljal..pa tak naprej ;)

Tale "zgodovinskost" je meni v veliko zadovoljstvo, kar kaže na to, da se folk, ki trdi "eh...spet BSoD, pa pravjo da bodo compu kdaj intelektualno presegli ljudi, bah...neumna kišta!" moti. Kateri intelektualni posel sploh še ostaja popolnoma v domeni človeka?
Z vsakim kubikom, ki steče po Bistrici, stroji prevzemjo več človeškega dela. Avtomaticacija all the way.

Smešno se sliši, ampak recimo če bi se mučil z nekim dokazom kak teden, potem bi ga predal v obdelavo compu, ki bi malo zamlel ter izpljunil brezhiben izdelek, bi lahko brez slabe vesti dvignil tisti klobuk na glavi (metaforično seveda :). Mal bi me sicer grizlo, kako me lahko (vsaj na tem področju) kišta potolče, vendar bi določeno spoštovanje vseeno pretehtalo. Res...zanimivo,.. kot bi bila kaj drugega kot navaden stroj ;)

Ali pa, da bi v Coq jeziku napisal dokaz, da Coq pravilno preverja matematicne dokaze, in bi potem preko tega pognal zadevo. Hmm....