Mathematiker warnen: KI-Formalisierung der gesamten Mathematik könnte bleibenden Schaden anrichten
How to Formalize All of Mathematics
In einem Gastbeitrag äußern sich führende Mathematiker um Jeremy Avigad, Kevin Buzzard und Johan Commelin besorgt über die jüngsten Rufe, die gesamte Mathematik so schnell wie möglich mit KI zu formalisieren. Sie befürchten, dass ein überstürzter, unkoordinierter Prozess nicht nur Ressourcen verschwendet, sondern nachhaltigen Schaden anrichtet. Am Beispiel eines fehlgeschlagenen Versuchs von Math, Inc., Viazovskas Kugelpackungsergebnisse zu formalisieren, zeigen sie: KI-generierter Code ist oft schwer zu bereinigen, und saubere Formalisierung bleibt unverzichtbar. Die Autoren plädieren für ein qualitätsorientiertes Vorgehen, bei dem formale Artefakte tatsächlich genutzt werden und die Mathematik bereichern.
Wenn man es gut macht, könnte eine groß angelegte, koordinierte Formalisierungsanstrengung die mathematische Erforschung und Entdeckung enorm erweitern. Macht man es schlecht, ist es bestenfalls eine Verschwendung von Ressourcen; wahrscheinlicher ist, dass es bleibenden Schaden anrichtet.