Sfida matematica aperta alla ricerca di limiti più stretti per ridurre le dimensioni delle prove STARK
Punti chiave
- •La sfida aperta accetta soluzioni sia da matematici umani che da agenti AI, attribuendo il merito a chi completa la prova.
- •Tre obiettivi sono formalizzati nel theorem prover Lean, e un obiettivo è considerato risolto solo una volta completata una prova revisionata in modo indipendente.
- •La sfida si concentra sul numero di bad challenges in un test di prossimità di Reed-Solomon, che determina quante query deve eseguire un verificatore STARK.
- •Gli obiettivi includono la sostituzione di un noto limite quadratico con uno lineare e la dimostrazione di un limite quadratico su un intervallo più ampio, rispetto ai limiti esistenti stabiliti da Dao, Kominers e Thaler (2026).
- •Gli organizzatori avvertono che un limite più stretto, da solo, non riduce nulla, poiché i risparmi reali sulle dimensioni delle prove richiedono anche un'analisi completa del protocollo.
Una nuova sfida matematica aperta invita sia le persone che gli agenti AI a dimostrare limiti più stretti che consentirebbero alle prove STARK di effettuare meno verifiche e di ridurre le proprie dimensioni, secondo il sito della sfida.
Il progetto è condotto come workshop provably.fast, con il codice ospitato nell'organizzazione GitHub starknet-innovation — un dettaglio che colloca l'iniziativa nell'ecosistema Starknet, dove le prove STARK sono utilizzate per verificare calcoli complessi con controlli leggeri.
Le STARK sono prove a conoscenza zero che si basano esclusivamente su una funzione hash. Poiché ogni query che un verificatore deve eseguire aggiunge dati e lavoro a ciascun controllo, i limiti alla base di tali query sono seguiti da vicino nei sistemi di prova. La sfida punta al numero di "bad challenges" in un test di prossimità di Reed-Solomon, che determina quante query deve eseguire un verificatore. I limiti attualmente noti provengono da Dao, Kominers e Thaler (2026).
Tre obiettivi, verificati in Lean
Il sito elenca tre obiettivi, tra cui la sostituzione di un noto limite quadratico con uno lineare e la dimostrazione di un limite quadratico su un intervallo più ampio. Ogni enunciato è formalizzato nel theorem prover Lean, e un obiettivo è considerato risolto solo una volta completata una prova revisionata in modo indipendente, con il merito attribuito alla persona o all'agente AI che l'ha realizzata. La formalizzazione degli enunciati in Lean elimina le ambiguità su ciò che costituisce una soluzione, e l'estensione del merito agli agenti AI trasforma la sfida in un test concreto della capacità delle macchine di contribuire alla matematica di livello di ricerca a fianco dei partecipanti umani.
Il sito osserva che un limite più stretto, da solo, non riduce nulla; i risparmi reali richiedono anche un'analisi completa del protocollo. Questa avvertenza delimita ciò che va osservato: se uno dei tre obiettivi verrà rivendicato, e se i successivi lavori sul protocollo tradurranno un nuovo limite in prove misurabilmente più piccole.
Fonte: CryptoBriefing
