Новый открытый математический челлендж приглашает людей и ИИ-агентов доказать более точные границы, которые позволят STARK-доказательствам выполнять меньше проверок и уменьшиться в размере, согласно сайту челленджа.

Проект реализуется как воркшоп provably.fast, его код размещён в организации starknet-innovation на GitHub — деталь, которая относит эту инициативу к экосистеме Starknet, где STARK-доказательства используются для проверки сложных вычислений с помощью лёгких проверок.

STARK — это доказательства с нулевым разглашением, опирающиеся только на хеш-функцию. Поскольку каждый запрос, который должен выполнить верификатор, добавляет данные и работу к каждой проверке, границы, стоящие за этими запросами, пристально отслеживаются в системах доказательств. Челлендж нацелен на количество «плохих вызовов» в тесте близости Рида — Соломона, которое определяет, сколько запросов должен выполнить верификатор. Текущие известные границы получены Dao, Kominers и Thaler (2026).

Три задачи, проверяемые в Lean

На сайте перечислены три задачи, включая замену известной квадратичной границы линейной и доказательство квадратичной границы на более широком диапазоне. Каждое утверждение формализовано в интерактивном доказателе Lean, и задача считается решённой только после завершения независимо проверенного доказательства, авторство приписывается человеку или ИИ-агенту, стоящему за ним. Формализация утверждений в Lean устраняет неоднозначность в том, что считается решением, а признание заслуг ИИ-агентов превращает челлендж в конкретный тест того, способны ли машины вносить вклад в математику исследовательского уровня наряду с людьми.

На сайте отмечается, что сама по себе более точная граница ничего не уменьшает; реальная экономия также требует полного анализа протокола. Эта оговорка задаёт ориентиры для наблюдения: будет ли достигнута хотя бы одна из трёх задач и переведёт ли последующая работа над протоколом новую границу в измеримо меньшие доказательства.

Источник: CryptoBriefing