Виталик предложил новый класс языков программирования — под проверку AI-доказательств человеком

Виталик Бутерин описал концепцию языка, который «действительно стоит попытаться создать»: высокоуровневый язык, компилируемый в Lean или HOL, максимально дружелюбный для чтения человеком — но только в части определений и теорем. Сами доказательства читаемыми быть не обязаны: с ними достаточно машинной проверки корректности.

Сценарий использования прямой: AI выдаёт массив доказательств, а человеку нужно быстро и точно понять, что именно доказано — какие конкретные утверждения стоят за формальной записью. Сегодня это узкое место: Lean-формализации читают единицы специалистов, и между «доказательство верифицировано» и «мы понимаем, что оно означает» остаётся разрыв, который такой язык и должен закрыть.

Это встраивается в главный технический сюжет недели. Сооснователь NEAR Илья Полосухин днём ранее заявил, что AI-хакинг уже обгоняет классические аудиты и индустрии нужен переход к формальной верификации, где AI генерирует доказательства, а человек их проверяет. Zcash в Project Tachyon так уже работает: AI-assisted верификация сжала годы работы до недель. Предложение Виталика закрывает последнее звено этой цепочки — интерфейс между машинными доказательствами и человеческим пониманием того, что именно гарантировано.

Источник:
https://x.com/VitalikButerin/status/2079582483243245850?s=20