Terence Taos Sicht auf Proof Checker und KI-Programme

KI wird zum „Copiloten“ von Mathematikern

Der Wandel der Mathematik

• Mathematik war traditionell eine einsame Disziplin.
• In jüngerer Zeit lassen sich viele Teile der Mathematik streng in einzelne Bausteine zerlegen und dadurch per Computer verifizieren.
• Terence Tao von der UCLA glaubt, dass diese Methoden neue Möglichkeiten der Zusammenarbeit in der Mathematik eröffnen.

Der Aufstieg automatischer Proof Checker

• Durch automatische Proof Checker können Mathematiker mit Hunderten von Menschen zusammenarbeiten.
• So bewies Tao beispielsweise die Polynomial Freiman-Ruzsa (PFR)-Vermutung in Zusammenarbeit mit mehr als 20 Personen.
• Dabei trägt jede Person Beweise für kleine Teilschritte bei, während die Gesamtrichtung zentral koordiniert wird.

Die Formalisierung der Mathematik

• Nicht jeder muss Programmierer sein; die Rollen können zwischen Menschen aufgeteilt werden, die sich auf die mathematische Richtung konzentrieren, und solchen, die formale Beweise erstellen.
• Durch die Entwicklung standardisierter Mathematikbibliotheken ist formale Mathematik praktisch nutzbar geworden.
• Ein Projekt namens Lean verfügt über eine umfangreiche Bibliothek, die grundlegende mathematische Sätze umfasst.

KI und die Zukunft der Mathematik

• KI könnte eine unterstützende Rolle für Mathematiker übernehmen.
• KI kann dabei helfen, Beweise zu formalisieren und sogar Arbeiten wie das Verfassen und Einreichen von Artikeln zu unterstützen.
• Denkbar ist eine Zusammenarbeit, bei der Menschen Ideen liefern und KI diese formalisiert.

Eine neue Art, Mathematik zu betreiben

• In Zusammenarbeit mit KI könnte eine neue Form des mathematischen Arbeitens entstehen.
• Mathematiker könnten ihre Rollen stärker wie Projektmanager aufteilen, während KI beim Beweisen unterstützt.
• Durch die Formalisierung von Mathematiklehrbüchern könnten interaktivere Lernwerkzeuge entstehen.

Grenzen und Möglichkeiten von KI

• KI kann helfen, große Probleme der Mathematik anzugehen, doch menschliche Intuition und Verständnis bleiben weiterhin wichtig.
• Möglicherweise braucht es einen neuen Typ von Mathematikern, der von KI gelieferte Beweise analysiert und versteht.
• KI könnte neue Bereiche der Mathematik erkunden und Menschen bei Aspekten unterstützen, die schwer zu verstehen sind.

Meinung von GN⁺

• Die Rolle von KI: KI kann eine wichtige Rolle als Werkzeug spielen, das Mathematikern hilft, größere Probleme zu lösen.
• Die Bedeutung von Zusammenarbeit: Die Kooperation zwischen KI und Menschen kann neue Möglichkeiten für die Mathematik eröffnen.
• Die Notwendigkeit der Formalisierung: Die Formalisierung der Mathematik kann mehr Wissen explizit machen und Zusammenarbeit fördern.
• Der Mathematiker der Zukunft: Es könnte einen neuen Typ von Mathematikern brauchen, der in Zusammenarbeit mit KI Beweise analysiert und versteht.
• Technologischer Fortschritt: Die Verbindung von KI und Mathematik könnte mit dem technischen Fortschritt noch mehr Möglichkeiten eröffnen.

[GN⁺]

Hacker-News-Meinung

• Text von Edsger Dijkstra: Erwähnt wird ein satirischer Text aus dem Jahr 1975 über die Art und Weise, wie Software produziert wird; im Kern ist er eine Kritik am geistigen Eigentum.

• Fähigkeiten von LLMs: Derzeit dienen sie als Hilfsmittel, könnten künftig aber Erkenntnisse auf höherem Niveau liefern. Zum Beispiel könnten sie Dinge erfassen, die Menschen übersehen, etwa das Verständnis der Beziehung zwischen Atombomben und Komposthaufen.

• Zusammenfassung des Interviews:

  • Mathematiker als Projektmanager: KI und Beweisassistenten könnten revolutionär dafür sein, mathematische Einsichten zu erzeugen.
  • Implizites Wissen: Weil Wissen aus Intuition und Fehlschlägen nicht in Aufsätzen enthalten ist, ist die Kommunikation zwischen Mathematikern wichtig.
  • Formalisierung der Mathematik: Beweisassistenten machen es nötig, die Mathematik stärker zu formalisieren, um das Verständnis zu fördern.

• Computergestützte Beweisprüfung: KI könnte für die Verifikation von Beweisen nützlich sein, ähnlich wie Schach-Engines. Der Umgang mit vielen Theoremen und Hilfssätzen ist schwierig, aber KI könnte das verbessern.

• Softwaregeschichte und Mathematik: Es wird ein Vergleich zwischen früheren Softwareprojekten und dem heutigen modularen Software Engineering gezogen, verbunden mit der Ansicht, dass die Mathematik einen ähnlichen Weg gehen könnte.

• Vortrag von Terence Tao: Empfohlen wird ein Vortrag, der genauer erklärt, wie man Lean in der mathematischen Forschung einsetzt.

• Mathematische Beweise mit GPT-4: Vorgestellt wird ein Fall, in dem GPT-4 erfolgreich einen neuen Hilfssatz bewiesen hat. Das könnte für die mathematische Forschung nützlich sein.

• Mathematiker am Anfang ihrer Laufbahn und Lean: Es wird die Ansicht geäußert, dass Mathematiker am Anfang ihrer Laufbahn ihrer Intuition vertrauen und eher Aufsätze schreiben sollten.

• Aus Fehlern lernen: Es wird die Ansicht geäußert, dass es sehr produktiv ist, aus den Fehlern anderer zu lernen.