PHÂN TÍCH: Vitalik Buterin đề xuất một loại ngôn ngữ lập trình mới. Loại ngôn ngữ này được biên dịch sang các hệ thống chứng minh như Lean, với mục tiêu chỉ để các định nghĩa và định lý trở nên dễ đọc nhất có thể đối với con người.

Lập luận đảo ngược nút thắt thông thường. “Mọi thứ liên quan đến chứng minh chỉ là việc các chứng minh đúng hay không.” Máy móc sẽ kiểm tra phần đó. Thứ con người cần là hiểu “những khẳng định chính xác, cụ thể thực sự là gì mà đã được chứng minh.”
Các bộ chứng minh bằng AI hiện đã chạy qua Lean. AlphaProof, DeepSeek-Prover và Leanstral của Mistral đều dùng nó làm lớp phụ trợ hình thức. AWS cũng xác minh hình thức ngôn ngữ ủy quyền của mình trong đó, còn Microsoft xác minh mật mã dùng trong sản xuất bằng nó.
Mười tác nhân AI gần đây đã xây dựng một ngôn ngữ đã được xác minh với các tối ưu được chứng minh trong 1 cuối tuần, không có dòng mã nào do con người viết. Các chứng minh giờ đến nhanh hơn bất kỳ ai kịp đọc để xem chúng tuyên bố điều gì.
@VitalikButerin đã thúc đẩy xác minh hình thức trong nhiều năm như câu trả lời cho các lỗ hổng khai thác hợp đồng thông minh, và Quỹ Ethereum đang triển khai một nỗ lực xác minh chuyên biệt.
Lớp định lý theo cách dễ đọc đối với con người là mảnh ghép còn thiếu của kế hoạch đó; các bên kiểm toán cuối cùng có thể đọc được hợp đồng “được AI xác minh” thực sự đảm bảo điều gì.