Gibt es Grenzen für mathematische Computerbeweise ?

[ralfkannenberg]

Hallo zusammen,

ich möchte diesen Beitrag mal als Anlass nehmen, einen neuen Thread zu eröffnen:

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

[ralfkannenberg]

Hallo zusammen,

der Vollständigkeit halber will ich auch noch den Ausgangspunkt benennen:

Wenn du schon unbedingt offtopic gehen willst dann beantworte mir mal, was für eine Art von Aufgaben man heutzutage noch ohne Computer löst. Ich käme mir dabei so vor wie ein Schmied ohne Hammer, oder wie ein Pferd ohne Hufeisen. Du musst ja eine gar stählerne Faust haben!

Na dann beweise mir mal die Unmöglichkeit der Quadratur des Kreises mit Zirkel, Lineal und Einheitsdmassstab mit Hilfe eines Computers

Wir wollen vielleicht erst mal klein anfangen: beweise mir mit Hilfe eines Computers, dass die Quadratwurzel aus 2 irrational ist.

Freundliche Grüsse, Ralf

[Herr Senf]

Hallo Ralf,
ich habe zwar eine "Matheallergie", trotzdem lese ich gern den Thilo - so jeder 10. Beitrag dort ist noch was für mich, 90% hinterm Tellerrand.
2009 hat er mal die verschiedensten Beweisarten gepostet und das es bis dato schon 80 PC-Beweise gab, die meisten "17" für Wurzel 2.
Hier http://scienceblogs.de/mathlog/2009/02/ ... in-beweis/ hat er zur "PC-Tendenz" auf http://www.cl.cam.ac.uk/~jrh13/ verwiesen.
Den Harrison gibt's für mich auch auf russisch Grüße Senf

PS: Mathegeschichte ist ja auch interessant http://www.mathematik.uni-wuerzburg.de/ ... eschim.pdf zu den Beweisen seit der Antike

[ralfkannenberg]

Hallo Herr Senf,

ich mag ja Tomaten auf den Augen haben, aber ich kann in Deinen Links den Beweis, dass die sqrt(2) irrational ist, nicht finden.


Freundliche Grüsse, Ralf

P.S.:

PS: Mathegeschichte ist ja auch interessant http://www.mathematik.uni-wuerzburg.de/ ... eschim.pdf zu den Beweisen seit der Antike

Interessanter Link