Offene Mathe-Herausforderung sucht engere Schranken zur Verkleinerung von STARK-Beweisen
Wichtige Erkenntnisse
- •Die offene Herausforderung akzeptiert Lösungen von menschlichen Mathematikern und KI-Agenten gleichermaßen; die Anerkennung geht an denjenigen, der den Beweis abschließt.
- •Drei Ziele sind im Theorembeweiser Lean formal festgelegt, und ein Ziel gilt erst dann als gelöst, wenn ein unabhängig überprüfter Beweis abgeschlossen wurde.
- •Die Herausforderung konzentriert sich auf die Anzahl der „bad challenges“ in einem Reed-Solomon-Proximity-Test, der bestimmt, wie viele Abfragen ein STARK-Verifizierer durchführen muss.
- •Zu den Zielen gehören die Ersetzung einer bekannten quadratischen Schranke durch eine lineare und der Beweis einer quadratischen Schranke über einen größeren Bereich, gegenüber den bestehenden Schranken von Dao, Kominers und Thaler (2026).
- •Die Organisatoren weisen darauf hin, dass eine engere Schranke allein nichts verkleinert, da echte Beweisgrößen-Einsparungen zusätzlich eine vollständige Protokollanalyse erfordern.
Eine neue offene Mathematik-Herausforderung lädt Menschen und KI-Agenten ein, engere Schranken zu beweisen, die es STARK-Beweisen ermöglichen würden, weniger Prüfungen durchzuführen und an Größe zu schrumpfen, wie auf der Website der Herausforderung zu lesen ist.
Das Projekt wird als provably.fast-Workshop betrieben, der Code ist in der GitHub-Organisation starknet-innovation hinterlegt — ein Detail, das die Initiative im Starknet-Ökosystem verortet, wo STARK-Beweise verwendet werden, um aufwendige Berechnungen mit leichten Prüfungen zu verifizieren.
STARKs sind Zero-Knowledge-Beweise, die nur auf einer Hashfunktion beruhen. Da jede Abfrage, die ein Verifizierer durchführen muss, Daten und Aufwand für jede Prüfung hinzufügt, werden die Schranken hinter diesen Abfragen in Beweissystemen genau beobachtet. Die Herausforderung zielt auf die Anzahl der „bad challenges“ in einem Reed-Solomon-Proximity-Test ab, der bestimmt, wie viele Abfragen ein Verifizierer durchführen muss. Die derzeit bekannten Schranken stammen von Dao, Kominers und Thaler (2026).
Drei Ziele, verifiziert in Lean
Die Website listet drei Ziele auf, darunter die Ersetzung einer bekannten quadratischen Schranke durch eine lineare und den Beweis einer quadratischen Schranke über einen größeren Bereich. Jede Aussage ist im Theorembeweiser Lean fixiert, und ein Ziel gilt erst dann als gelöst, wenn ein unabhängig überprüfter Beweis abgeschlossen wurde — die Anerkennung geht an die Person oder den KI-Agenten dahinter. Die Fixierung der Aussagen in Lean beseitigt Mehrdeutigkeiten darüber, was als Lösung zählt, und die Einbeziehung von KI-Agenten macht die Herausforderung zu einem konkreten Test dafür, ob Maschinen gemeinsam mit menschlichen Teilnehmern forschungsreife Mathematik beitragen können.
Die Website weist darauf hin, dass eine engere Schranke allein nichts verkleinert; echte Einsparungen erfordern zudem eine vollständige Protokollanalyse. Dieser Vorbehalt rahmt, worauf zu achten ist: ob eines der drei Ziele beansprucht wird und ob nachfolgende Protokollarbeiten eine neue Schranke in messbar kleinere Beweise übersetzen.
Quelle: CryptoBriefing
