Desafío matemático abierto busca cotas más ajustadas para reducir el tamaño de las pruebas STARK
Puntos clave
- •El desafío abierto acepta soluciones tanto de matemáticos humanos como de agentes de IA, otorgando el crédito a quien complete la prueba.
- •Tres objetivos están especificados formalmente en el demostrador de teoremas Lean, y un objetivo se considera resuelto solo una vez completada una prueba revisada de forma independiente.
- •El desafío se centra en el número de bad challenges en una prueba de proximidad de Reed-Solomon, que determina cuántas consultas debe realizar un verificador STARK.
- •Los objetivos incluyen sustituir una cota cuadrática conocida por una lineal y demostrar una cota cuadrática en un rango más amplio, frente a las cotas existentes establecidas por Dao, Kominers y Thaler (2026).
- •Los organizadores advierten que una cota más ajustada por sí sola no reduce nada, ya que los ahorros reales en el tamaño de las pruebas también requieren un análisis completo del protocolo.
Un nuevo desafío matemático abierto invita tanto a personas como a agentes de IA a demostrar cotas más ajustadas que permitirían a las pruebas STARK realizar menos verificaciones y reducir su tamaño, según el sitio web del desafío.
El proyecto se ejecuta como un taller de provably.fast, con su código alojado en la organización de GitHub starknet-innovation, un detalle que ubica el esfuerzo dentro del ecosistema Starknet, donde las pruebas STARK se utilizan para verificar cálculos pesados con verificaciones ligeras.
Las STARK son pruebas de conocimiento cero que se basan únicamente en una función hash. Dado que cada consulta que debe realizar un verificador agrega datos y trabajo a cada comprobación, las cotas detrás de esas consultas son seguidas de cerca en los sistemas de pruebas. El desafío apunta al número de "bad challenges" en una prueba de proximidad de Reed-Solomon, que determina cuántas consultas necesita realizar un verificador. Las cotas conocidas actualmente provienen de Dao, Kominers y Thaler (2026).
Tres objetivos, verificados en Lean
El sitio enumera tres objetivos, incluida la sustitución de una cota cuadrática conocida por una lineal y la demostración de una cota cuadrática en un rango más amplio. Cada declaración está fijada en el demostrador de teoremas Lean, y un objetivo se considera resuelto solo una vez que se ha completado una prueba revisada de forma independiente, con el crédito correspondiente a la persona o agente de IA detrás de ella. Fijar las declaraciones en Lean elimina la ambigüedad sobre qué cuenta como solución, y extender el crédito a los agentes de IA convierte el desafío en una prueba concreta de si las máquinas pueden contribuir con matemáticas de nivel de investigación junto con los participantes humanos.
El sitio señala que una cota más ajustada por sí sola no reduce nada; los ahorros reales también requieren un análisis completo del protocolo. Esa advertencia marca qué observar: si alguno de los tres objetivos es reclamado, y si el trabajo posterior en el protocolo traduce una nueva cota en pruebas mediblemente más pequeñas.
Fuente: CryptoBriefing
