오데일리에 따르면 비탈릭 부테린은 X에서 “시도해볼 만한 새 고급 프로그래밍 언어는 린(Lean) 또는 HOL 등으로 컴파일되며, 사람이 정의와 정리를 최대한 쉽게 읽을 수 있도록 해야 한다”고 밝혔다.
그는 증명은 정확하면 충분하지만 핵심은 정의와 정리 자체라며, AI가 긴 증명을 출력할 때 독자가 실제로 어떤 명제가 증명됐는지 쉽게 파악하는 것이 중요하다고 설명했다.
<저작권자 ⓒ TokenPost, 무단전재 및 재배포 금지>
많이 본 기사