Соучредитель Ethereum Виталик Бутерин предложил новый язык программирования, который компилировался бы напрямую в Lean или HOL — ещё один инструмент формальных доказательств.

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

Язык для читателей ИИ-доказательств

Lean — это ассистент доказательств, программа, с помощью которой математики и инженеры пишут доказательства, проверяемые компьютером построчно. Исследователи Ethereum уже используют его для верификации криптографического кода и логики консенсуса. Ассистенты доказательств существуют почти 60 лет, но область оставалась нишевой.

По мысли Бутерина, к внутренним шагам доказательства предъявляется лишь одно требование — математическая корректность, и читатели не изучают этот механизм напрямую. С определениями и теоремами иначе: их люди читают, чтобы понять, что именно гарантирует программа. Схожее разделение Бутерин разбирал в майской заметке, где математическое доказательство показывает соответствие эффективного низкоуровневого кода отдельной, читаемой спецификации, так что один аудит покрывает обе версии.

ИИ пишет доказательства, люди проверяют утверждения

Большие языковые модели уже способны писать пригодные Lean-доказательства. Бутерин назвал в числе подходящих инструментов Claude и Deepseek 4 Pro, а также Leanstral — меньшую модель, специально настроенную под Lean. Один из примеров — проект evm-asm, реализация EVM, верифицированная относительно читаемого эталона. Вместе с тем исследователи строят формально верифицированный ZK-EVM — версию виртуальной машины Ethereum (EVM) с доказательствами с нулевым разглашением.

Ставки выходят за рамки удобства: специалисты по безопасности зафиксировали в этом году рост числа попыток эксплойтов с помощью ИИ, и формально верифицированный код может стать одной из защит от этой тенденции. Бутерин продолжает публично проверять идеи — недавно он показал анонимный билборд на доказательствах с нулевым разглашением. Прототипа нового языка пока не существует, а точный синтаксис Бутерин оставил открытым: разработчики могут сойтись на едином стандарте либо остаться с несколькими несовместимыми диалектами.

Источник: BeInCrypto