Un défi mathématique ouvert recherche des bornes plus serrées pour réduire la taille des preuves STARK
Points clés
- •Le défi ouvert accepte des solutions aussi bien de mathématiciens humains que d'agents d'IA, le crédit étant attribué à celui qui achève la preuve.
- •Trois objectifs sont formellement spécifiés dans le prouveur de théorèmes Lean, et un objectif n'est considéré comme résolu qu'une fois une preuve examinée de manière indépendante achevée.
- •Le défi se concentre sur le nombre de bad challenges dans un test de proximité de Reed-Solomon, qui détermine le nombre de requêtes qu'un vérificateur STARK doit effectuer.
- •Les objectifs incluent le remplacement d'une borne quadratique connue par une borne linéaire et la preuve d'une borne quadratique sur une plage plus étendue, par rapport aux bornes existantes établies par Dao, Kominers et Thaler (2026).
- •Les organisateurs soulignent qu'une borne plus serrée seule ne réduit rien, car des économies réelles sur la taille des preuves exigent également une analyse protocolaire complète.
Un nouveau défi mathématique ouvert invite aussi bien les humains que les agents d'IA à prouver des bornes plus serrées qui permettraient aux preuves STARK d'effectuer moins de vérifications et de réduire en taille, selon le site du défi.
Le projet est mené sous forme d'atelier provably.fast, avec un code hébergé sous l'organisation GitHub starknet-innovation — un détail qui situe l'initiative au sein de l'écosystème Starknet, où les preuves STARK sont utilisées pour vérifier des calculs lourds au moyen de vérifications légères.
Les STARK sont des preuves à divulgation nulle de connaissance qui reposent uniquement sur une fonction de hachage. Comme chaque requête que le vérificateur doit effectuer ajoute des données et du travail à chaque vérification, les bornes derrière ces requêtes sont étroitement surveillées dans les systèmes de preuve. Le défi cible le nombre de « bad challenges » dans un test de proximité de Reed-Solomon, qui détermine le nombre de requêtes que le vérificateur doit effectuer. Les bornes actuellement connues proviennent de Dao, Kominers et Thaler (2026).
Trois objectifs, vérifiés dans Lean
Le site énumère trois objectifs, notamment le remplacement d'une borne quadratique connue par une borne linéaire et la preuve d'une borne quadratique sur une plage plus étendue. Chaque énoncé est spécifié dans le prouveur de théorèmes Lean, et un objectif n'est considéré comme résolu qu'une fois une preuve examinée de manière indépendante achevée, le crédit revenant à la personne ou à l'agent d'IA qui en est à l'origine. La spécification des énoncés dans Lean supprime toute ambiguïté sur ce qui compte comme solution, et l'extension du crédit aux agents d'IA fait du défi un test concret de la capacité des machines à contribuer aux mathématiques de niveau recherche aux côtés des participants humains.
Le site souligne qu'une borne plus serrée seule ne réduit rien ; des économies réelles exigent également une analyse protocolaire complète. Cette réserve délimite ce qu'il faut surveiller : savoir si l'un des trois objectifs est atteint, et si un travail protocolaire ultérieur traduit une nouvelle borne en preuves mesurablement plus petites.
Source : CryptoBriefing
