Vitalik: Các ngôn ngữ lập trình cao cấp mới đáng để thử nên giúp cho việc đọc định nghĩa và định lý trở nên dễ dàng hơn.

Odaily đưa tin Vitalik đã đăng trên nền tảng X rằng một loại “ngôn ngữ lập trình cao cấp” mới đáng để thử nghiệm là ngôn ngữ được biên dịch sang Lean (hoặc HOL, v.v.), với trọng tâm là giúp con người dễ đọc các định nghĩa và định lý nhất có thể. Không phải chứng minh, bởi miễn là chứng minh đúng là được, điều quan trọng nằm ở định nghĩa và định lý. Ứng dụng giả định là: AI xuất ra một đoạn chứng minh dài và người đọc cần dễ dàng hiểu được chính xác những luận điểm nào thực sự đã được chứng minh trong đó.