ich möchte diesen Beitrag mal als Anlass nehmen, einen neuen Thread zu eröffnen:
Herr Senf hat geschrieben:ralf hat yukterez gefragt und hat geschrieben:Wir wollen vielleicht erst mal klein anfangen: beweise mir mit Hilfe eines Computers, dass die Quadratwurzel aus 2 irrational ist.
Der Beweis der Irrationalität der Quadratwurzel 2 benutzt nur elementare Eigenschaften ganzer Zahlen, kein Problem für einen Computer.
Mittlerweile gibt es dazu 17 Computerbeweise z.B. mit http://en.wikipedia.org/wiki/HOL_Light
In der "Ukraine" zwar nicht diskutieren wollend, aber mitlesend noch aufpassend - Senf
Zwar kann ich in dem genannten Link keinen solchen Beweis entdecken, es würde mich aber schon interessieren, wie man sowas macht.
Freundliche Grüsse, Ralf