Vitalik Buterin proponuje nowy język, który ma ułatwić weryfikację dowodów AI

Buterin stawia na formalną weryfikację: proponuje język, który ma sprawić, że dowody generowane przez AI będą czytelniejsze dla Lean i HOL. Pomysł wpisuje się w roadmapę Lean Ethereum oraz rozwój formalnie zweryfikowanego ZK-EVM.

Najważniejsze informacje

• Vitalik Buterin proponuje język programowania, który może kompilować się bezpośrednio do Lean lub HOL.
• Celem jest zwiększenie czytelności dowodów tworzonych przez AI i ułatwienie ich weryfikacji przez ludzi, a nie przyspieszenie samego pisania.
• Buterin nie zaprezentował jeszcze prototypu i nie ujawnił dokładnej składni języka.

Współzałożyciel Ethereum Vitalik Buterin przedstawił koncepcję nowego języka programowania, który mógłby kompilować się bezpośrednio do Lean lub HOL. Nie chodzi w nim o to, by AI szybciej tworzyła dowody, lecz o to, by zapisane w nich twierdzenia były bardziej przejrzyste i łatwiejsze do sprawdzenia przez człowieka.

Dlaczego Lean ma tu znaczenie

Lean to proof assistant, który umożliwia matematyków i inżynierom sprawdzanie dowodów krok po kroku przy wsparciu komputera. Narzędzie istnieje od wielu lat, ale długo pozostawało rozwiązaniem niszowym. Dziś społeczność Lean zgromadziła już ponad 210 000 twierdzeń i 100 000 definicji w mathlib, co czyni ten ekosystem jedną z ważniejszych baz dla formalnej matematyki.

Buterin zwraca uwagę na praktyczny problem: AI potrafi dziś generować rozbudowane, zautomatyzowane dowody szybciej, niż zrobiłby to zespół ludzi. Dla czytelnika oznacza to jednak trudność z szybkim ocenieniem, co taki dowód faktycznie pokazuje. Jego zdaniem sama logika dowodu musi być poprawna matematycznie, ale definicje i twierdzenia powinny przede wszystkim pozostać zrozumiałe dla ludzi.

Czas tej propozycji nie jest przypadkowy. Zbiega się ona z własnym procesem przebudowy Ethereum, znanym jako Lean Ethereum roadmap. W ramach tych prac rozwijany jest również formalnie zweryfikowany ZK-EVM, czyli wersja Ethereum Virtual Machine oparta na zero-knowledge i wykorzystująca podobne metody.

AI pisze, ludzie sprawdzają

Buterin wymienia między innymi Claude, DeepSeek 4 Pro i Leanstral jako modele, które już teraz potrafią generować dowody Lean. To wpisuje się w szerszy trend, w którym AI coraz częściej wspiera formalną weryfikację. W 2025 roku ACM SIGPLAN wyróżniło wpływ Lean na matematykę, weryfikację sprzętu i oprogramowania oraz AI, przyznając nagrodę software award kilku kluczowym twórcom projektu.

Znaczenie tego wykracza poza samo Ethereum. Formalna weryfikacja służy także do potwierdzania poprawności systemów krytycznych, od protokołów kryptograficznych po urządzenia medyczne. Dla twórców projektów crypto bardziej czytelny język może ułatwić audyt twierdzeń bez konieczności analizowania całej warstwy dowodowej.

Znaczenie dla deweloperów Ethereum

Dla europejskich czytelników crypto to ważny sygnał przede wszystkim dlatego, że formalna weryfikacja staje się coraz istotniejsza w infrastrukturze, gdzie błędy mogą bezpośrednio wpływać na pieniądze lub bezpieczeństwo. Ethereum, systemy ZK i kod kryptograficzny to obszary, w których nawet drobna pomyłka może mieć poważne konsekwencje. Język, który lepiej porządkuje wyniki pracy AI, może więc okazać się cennym narzędziem przy budowie bardziej niezawodnego oprogramowania, a nie produktem końcowym samym w sobie.

Buterin nie pokazał jeszcze prototypu i pozostawił otwartą dokładną składnię. Na tym etapie nie wiadomo więc, czy deweloperzy ostatecznie przyjmą jeden standard, czy też będą korzystać z kilku wariantów równolegle.