Buterin proponuje język ułatwiający czytanie twierdzeń AI

Współzałożyciel Ethereum Vitalik Buterin zaproponował 21 lipca 2026 r. stworzenie nowego języka programowania, który kompilowałby się do asystentów dowodów Lean lub HOL. Celem ma być zwiększenie czytelności definicji i twierdzeń generowanych przez systemy sztucznej inteligencji.

W wpisie na Twitterze pojawił się fragment: „nowy rodzaj języka wysokiego poziomu… ma być jak najbardziej przyjazny dla człowieka do czytania definicji i twierdzeń. Nie dowodów.” Autor argumentował, że wewnętrzne kroki dowodów wymagają jedynie poprawności matematycznej, podczas gdy czytelnicy koncentrują się na specyfikacjach i gwarancjach przedstawianych przez twierdzenia.

Propozycja zbiega się z planami prac nad mapą drogową Lean Ethereum. Zespoły badawcze używają Lean do formalnej weryfikacji kodu kryptograficznego i logiki konsensusu. Prace obejmują także projekt formalnie zweryfikowanego ZK-EVM, czyli maszyny wirtualnej Ethereum z dowodami zerowej wiedzy.

Duże modele językowe już generują dowody w Lean. Buterin wymienił jako przykłady modele Claude i Deepseek 4 Pro oraz mniejszy model Leanstral. Jako praktyczny przykład przytoczono implementację evm-asm, zweryfikowaną względem czytelnej specyfikacji. W jednym z wyzwań AI uczestnicy rozwiązali zadanie w kilka godzin, co ilustruje przyspieszenie automatyzacji pisania dowodów.

Badacze bezpieczeństwa odnotowali wzrost prób ataków z wykorzystaniem narzędzi AI. Formalna weryfikacja kodu ma ograniczać ryzyko takich ataków. Według propozycji, język przyjazny do czytania specyfikacji umożliwi deweloperom i audytorom szybsze sprawdzenie, jakie gwarancje daje oprogramowanie bez konieczności przeglądania szczegółów dowodu.

Na razie nie istnieje prototyp ani ustalona składnia nowego języka. W społeczności toczy się dyskusja, czy wypracować jeden standard, czy dopuścić kilka niekompatybilnych dialektów. Wybór ten może wpłynąć na tempo wdrażania rozwiązań w środowiskach produkcyjnych.

Asystenci dowodów są używani od prawie 60 lat, jednak ich zastosowanie pozostaje ograniczone. Lean i HOL to przykłady narzędzi służących do tworzenia dowodów sprawdzanych przez komputer. W majowym wpisie na blogu przedstawiono model, w którym dowód matematyczny łączy wydajny, niskopoziomowy kod z czytelną specyfikacją, by weryfikacja obejmowała oba poziomy jednocześnie.

Buterin testował też koncepcje praktycznego wykorzystania dowodów zerowej wiedzy, prezentując demonstracje pokazujące możliwe zastosowania w rzeczywistych rozwiązaniach. Prace nad oddzieleniem specyfikacji od implementacji z użyciem formalnych dowodów trwają w środowisku badawczym.