Bislang galt: Computer können rechnen, aber mathematische Beweise bleiben Kopfarbeit. Doch ein neues Verfahren könnte die Lösung großer Probleme revolutionieren.
Das wäre anders, wenn es ein automatisiertes Verfahren gäbe, das mathematische Arbeiten auf ihre Korrektheit prüft – was nun so weit ist. Es heißt Lean, und der aus Brasilien stammende de Moura, zurzeit als Informatiker in der Forschungsabteilung von Amazon beschäftigt, hat es seit 2013 mitentwickelt. Große Teile des mathematischen Wissens sind für Lean bereits in eine Art Computersprache übersetzt worden. Wenn nun eine Mathematikerin oder ein Mathematiker einen neuen mathematischen Beweis vorschlägt und in Lean formuliert, kann das System ihn Schritt für Schritt nachvollziehen und nachher mit dem Siegel „stimmt“ oder „stimmt nicht“ versehen. Jeder kann dem Ergebnis trauen, sobald es erfolgreich überprüft wurde.
Bei der Arbeit mit Lean müssen die menschlichen Mathematiker noch selbst die Idee für einen Beweis haben. Schon bald aber könnten auch Computer neue Beweise vorschlagen. Nimmt man beides zusammen – die Beweisfindung und die Überprüfung –, dann bekommen menschliche Forscherinnen und Forscher einen mächtigen Gehilfen an die Hand. So mächtig, dass der sie sogar eines Tages überflügeln könnte.
weiterlesen
