KI für Beweisformalisierung: Schönere Mathematik oder Kauderwelsch?
Inhalt
Dieser Golem-Plus-Text ist 24 Stunden lang frei verfügbar.
Die Firma Math, Inc. hat mit Einsatz von generativer KI einen preisgekrönten mathematischen Beweis formalisiert. Der Code der KI namens Gauss ist die erste Formalisierung eines Beweises, der die Field-Medaille gewonnen hat – auch bekannt als Nobelpreis der Mathematik. Damit knüpft Math, Inc. an eine alte Tradition an und stellt gleichzeitig viele neue Fragen.
Unter anderem, was aus einem Projekt wird, in dem ein Team den Beweis nicht nur formalisieren wollte. Denn Kevin Buzzard, Professor und Experte für mathematische Formalisierung am Imperial College London, und seine Kollegen wollten ihn "noch schöner machen", um damit "ein brillantes Stück Mathematik" zu bewahren.
Die Zukunft von schlanken Beweisen
Beweise zu formalisieren, sei bisher "sehr langsam und anspruchsvoll gewesen", sagt Chris Birkbeck, Doznet für Zahlentheorie an der Universität East Anglia. Das sei "bei Weitem mehr", als von den meisten Mathematikern erwartet werden könne. Dank KI dauere so ein Projekt jetzt statt Jahren oft nur noch "Wochen oder Monate".
Laut Birkbeck wäre es außerdem "eine großartige Sache" wenn Mathematiker in Zukunft jede neue Arbeit von KI formalisieren lassen könnten. Das wäre aus seiner Sicht der nächste Schritt in der Evolution der "Beweis-Assistenten", also Programmen, die Mathematiker seit den 1960er Jahren verwenden, um zu prüfen, ob sie jede Annahme und jeden Schritt in einem Beweis belegt haben.
Einerseits bietet KI also viele Möglichkeiten. Bei genauerer Betrachtung ergeben sich aber Probleme.
Am Anfang waren Raleighs Kanonenkugeln
Bei dem Beweis, den Math, Inc. formalisiert hat, handelt es sich um eine Erweiterung der sogenannten Keplerschen Vermutung. Johannes Kepler stellte sie im Jahr 1611 auf, nachdem er Schneeflocken, Bienenwaben und Granatäpfel untersuchte. Fasziniert von deren natürlicher Struktur, spekulierte er, was die dichteste Art sei, Kugeln in drei Dimensionen anzuordnen.
Praktisch geht die Frage sogar noch weiter zurück, auf den englischen Mathematiker Thomas Harriot, der mit Kepler korrespondierte. Harriot kam auf die Idee mit den Kugeln, als er von Sir Walter Raleigh die Aufgabe erhielt, Kanonenkugeln möglichst platzsparend in dessen Schiffen zu verstauen(öffnet im neuen Fenster). Mathematisch betrachtet, seien solche Probleme "sehr einfach zu beschreiben", sagt Birkbeck. "Aber die Lösungen sind sehr knifflig."
Bildlich kann man sich eine rechteckige Box vorstellen, in die man möglichst viele Kugeln packen will. Kepler vermutete, dass es keinen besseren Weg gebe, als eine von zwei bestimmten Anordnungen abzuwandeln: entweder eine Pyramide aus Kugeln mit viereckiger oder mit hexagonaler Basis. Die sogenannte mittlere Dichte beider Anordnungen beträgt 74,05 Prozent. Das sei der größtmögliche Anteil der Kiste, den man jeweils mit Kugeln vollpacken könne, so die Vermutung.
- Anzeige Hier geht es zu Künstliche Intelligenz: Wissensverarbeitung bei Amazon Wenn Sie auf diesen Link klicken und darüber einkaufen, erhält Golem eine kleine Provision. Dies ändert nichts am Preis der Artikel.