bebizonyitottak a negyszin-sejtest?

hat, kicsit levagyok maradva, mar ~1 honapos a paper, itten van az arxiv link. igazabol jol megirtnak nez ki, de en nem vagyok grafelmelet guru. :)

( timar | 2009. 12. 21., h – 10:09 )

... it is until 1976 with electronic computer that Appel and Haken first gave a proof by finding and verifying 1936 reducible unavoidable sets ...

33 éve be van bizonyítva.

:-D ez vicces :)

ha kozelebbrol erdekel esetleg a Riemann-hipotezis, akkor a Prime Obsession egy jo konyv, egesz erthetoen irja le meg nem annyira matematikusoknak is. :)

en anno mikor meg volt szep nagy tablam az egyetemi szombamban, nekiultem az eredeti paper nezegetesenek, de az egyik nem-elemi integralnal elakadtam (meg kellett volna forgatni valamit a +vegtelen korul :-)

A gepes bizonyirassal a kovetkezo a baj: nem volt bebizonyitva , hogy 1. a fordito altal generalt kod megfelel az algoritmusnak, 2. a generalt kod hibamentesen hajtodik vegre a gepben, 3. a kernelt is helyessegbizonyitani kellett volna.
Par honapja volt, hogy megcsinaltak az elso kernel-helyessegbizonyitast, szoval addig minden szamitogepes bizonyitas csak egy nagy valoszinuseggel igaz allitas, nem pedig biztosan igaz allitas.
Ezert nem fogadjak el sokan Appel es Haken bizonyitasat.

Azert ne feledjuk, hogy a kernel felel azert, hogy a programod egyaltalan futasi idot kap a processzortol, meg azert is, hogy a binarisbol o teszi a gep szamara kozvetlenul futtathatova a programot (relokalhatosag...), o felel a memoriafoglalasert, stb.
Pl. a malloc()-ot is helyessegbizonyitani kene, hogy tenyleg azt csinalja, amit csinal es soha nem hibazik. Kernelpanicot lattal-e mar?

Es te processzor hibat?
Processor mukodeset is be akarod bizonyitani ? RTL szinten meg mehetne is, de "gonosz" fizika is van a vilagon.

Lattal mar olyat, hogy kernel hiba miatt 2+2=5 lett ?
De mint mar mondam, szam daralashoz nem kell egy mai vedett modu csoda kernel. Nem volt mindig OS.

Es az a minimum, hogy tobbszor vegigszamolsz egy bizonyitast, mert meg kozmikos sugarzas is elbafhatja.

Amit nem lehet megirni assemblyben, azt nem lehet megirni.