Dyskusja:Twierdzenie o czterech barwach

Z Wikipedii

Jakie są te dwa przypadki?

[edytuj] Komputerowy asystent

Wątpliwości te usunięto za pomocą jego modyfikacji w 1994, a w 2004 udało się dokonać sprawdzenia poprawności przy użyciu komputerowego asystenta

Co to znaczy ? Oryginalny dowód też był przeprowadzony przy pomocy komputera, więc w czym nowość ?

Doniesienie o sprawdzeniu poprawności dowodu za pomocą komputerowego asystenta Coq: http://www.maa.org/devlin/devlin_01_05.html

Na tej stronie wspomniano dwie książki ma ktośdo nich dostęp? Kuszi 23:55, 30 mar 2006 (CEST).

Prawdę mówiąc po przejrzeniu tej strony dalej nie potrafię napisać, w czym to podejście jest nowsze. Olaf 21:56, 30 mar 2006 (CEST)

Coś tu się nie zgadza, porównajcie np z: [Eric W. Weisstein. "Four-Color Theorem." From MathWorld--A Wolfram Web Resource.] albo Kubale M.: "Introduction to computational complexity and algorithmic graph coloring", GTN, Gdańnsk (1998) strony 108--109.

Nie wiem o co chodzi z asystentem. Kuszi 23:55, 30 mar 2006 (CEST)

Nie znam dokładnie tego problemu, więc mogę się pokusić jedynie o interpretację zdania które budzi waszą wątpliwość. Możliwe, że oryginalny dowód musiał po prostu rozwiązać dużo przypadków jakiegoś problemu kombinatorycznego (lub cos w tym stylu). Zaimplementowano więc specjalny program, który sprawdził przypadki i kwita. Sprawdzenie przy pomocy assytenta to coś innego: asystent to ogólny program wspomagający dowodzenie twierdzeń, zazwyczaj z wbudowanym systemem reguł dowodzania przyjętym ogólnie, o którym wiadomo że jest spójny. Zatem sprawdzenie przez asystenta ma inną wagę (między innymi uwiarygodnia ten starszy program, napisany celowo do tego dowodu). Oczywiście, nie wiem na pewno, bo nie znam historii. Zgaduję na podstawie wiedzy ogólnej. Wazow 11:17, 31 mar 2006 (CEST)

Rzeczywiście, en wiki pisze dokładniej: "In 2004, Benjamin Werner and Georges Gonthier formalized a proof of the theorem inside the Coq theorem prover (Gonthier, n.d.). This removes the need to trust the various computer programs used to verify particular cases — it is only necessary to trust the Coq prover." Informacja jest więc najprawdopodobniej prawdziwa, przydałoby się przeredagować i uzupełnić. Kuszi 14:59, 31 mar 2006 (CEST).