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

Ідея націлена на конкретну прогалину: штучний інтелект дедалі частіше видає великі блоки автоматичних доказів швидше, ніж їх могла б написати вручну будь-яка команда людей, проте небагато хто здатен швидко підтвердити, що саме ці докази встановлюють.

Мова для читачів ШІ-доказів

Lean — це асистент доказів, програма, за допомогою якої математики та інженери пишуть докази, що їх комп’ютер перевіряє рядок за рядком. Дослідники Ethereum уже використовують його для верифікації криптографічного коду та логіки консенсусу. Асистенти доказів існують майже 60 років, але ця галузь лишалася нішевою.

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

ШІ пише докази, люди перевіряють твердження

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

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

Джерело: BeInCrypto