Student World

Na New Scientistu se objevila velmi zajímavá informace o potvrzení důkazu čtyř barev, bohužel bez konkrétnějších údajů.
Viz
http://www.newscientist.com/article.ns?id=dn7286
Jakkoliv se na matematické články na Science Worldu obvykle spustí hromobití kritiky, přesto se pokusím o několik shrnujících poznámek. Předpokládám, že budu náležitě opraven a informace bude v diskusi doplněna :-).

Důkaz problému čtyř barev (jaký je minimální počet barev, kterými můžeme v rovině vybarvit každou mapu tak, aby se plochy stejné barvy nedotýkaly jinak než v bodě) byl pokládá za poměrně problematický proto, že při něm byly poněkud neobvykle použity počítače. Důkaz vyžadoval projít tisíce různých typů map – což bylo "automaticky" zrealizováno už v polovině 70. let minulého století. Kritici však namítali, že takový důkaz není korektní, nebo alespoň "esteticky uspokojivý" – co kdyby byla v počítačovém kódu programu ve skutečnosti chyba? Což kdyby nastala chyba při jeho provádění? (např. kolize hardwaru s částicí kosmického záření apod.)

Nyní vědci příslušný program otestovali na "logickou správnost/konzistenci" pomocí programu, respektive jazyka Coq, který umožňuje reprezentovat logické výrazy a kontrolovat správnost jednotlivých kroků původního důkazu. Optimisté se domnívají, že Coq by mohl výrazně změnit provádění matematických důkazů. Samotní tvůrci ale zdůrazňují, že převod složitějších matematických důkazů/problémů do odpovídající reprezentace v Coqu bude časově zdlouhavé. Výpočetně náročné pak navíc může být i samotné ověření.

Na uvedeném postupu je zajímavé, že se na něm podílel také zaměstnanci výzkumných laboratoří společnosti Microsoft v britské Cambridge. Příslušné postupy by se podle nich mohly uplatit nejen při matematických důkazech, ale i při automatizovaných testech konzistence/správnosti softwaru.

O roli počítačů v budoucích matematických důkazech viz také: Ian Stewart: Matematika v roce 2050
http://www.scienceworld.cz/sw.nsf/ID/FE065372CE594232C1256F430051D1D7

autor Pavel Houser