비탈릭 “새 고급 프로그래밍 언어, 정의·정리 읽기 쉬워야”

오데일리에 따르면 비탈릭 부테린은 X에서 “시도해볼 만한 새 고급 프로그래밍 언어는 린(Lean) 또는 HOL 등으로 컴파일되며, 사람이 정의와 정리를 최대한 쉽게 읽을 수 있도록 해야 한다”고 밝혔다.

그는 증명은 정확하면 충분하지만 핵심은 정의와 정리 자체라며, AI가 긴 증명을 출력할 때 독자가 실제로 어떤 명제가 증명됐는지 쉽게 파악하는 것이 중요하다고 설명했다.