Wann können von Maschinen produzierte Ergebnisse als Beweis gelten ?
Das ist eine interessante Frage. Maschinen können bei der Beweisführung eine wertvolle Hilfe sein. Ich habe von jemandem gelesen, dass er in einem Induktionsbeweis den Induktionsschluss geschafft hatte, aber keinen brauchbaren Induktionsanfang fand. Ein Computerprogramm lieferte diesen dann.
Die Beweisidee stammte also vom Menschen. Die Beweislücke schloss der Computer. Gerade bei Induktionsbeweisen sind digitale Werkzeige eine große Hilfe. Soll z.B. eine Summenformel durch vollständige Induktion bewiesen werden, gelingen oft Schülern notwendige Termumformungen nicht. Diese können oft von Computer-Algebra geleistet werden.
Auch in diesem Falle stammt die Beweisidee vom Aufgabenlöser und der Computer klärt Teilfragen. Neue Frage: Haben Maschinen Beweisideen?