Đồng sáng lập Ethereum, Vitalik Buterin, đã đề xuất phát triển một ngôn ngữ lập trình cấp cao mới nhằm nâng cao khả năng đọc hiểu các bằng chứng do AI tạo ra. Ngôn ngữ này sẽ biên dịch sang các hệ thống chứng minh định lý như Lean và HOL, tập trung vào việc làm cho "định nghĩa và định lý" trở nên dễ hiểu hơn thay vì quá trình chứng minh. Mục tiêu là giúp con người có thể hiểu rõ ràng những gì các bằng chứng do AI tạo ra đã thiết lập chính thức, từ đó tạo điều kiện thuận lợi cho việc kiểm tra và xác minh các khẳng định toán học và logic.