PANews 7월21일 소식, 이더리움 공동 창립자 비탈릭 부테린이 Lean, HOL과 같은 정리 증명 시스템으로 컴파일 가능한 새로운 고급 프로그래밍 언어를 탐색해야 한다고 제안하며, 증명 과정 자체보다는 “정의와 정리”의 가독성을 최적화하는 데 중점을 두어야 한다고 밝혔다. 비탈릭은 이 언어의 목표 시나리오는 AI가 대규모 형식 증명을 출력한 후, 인간이 그 증명이 구체적으로 “무엇을 형식적으로 증명했는지”를 명확히 이해하도록 돕는 것, 즉 독자가 AI가 제시한 구체적인 수학적·논리적 주장을 더 쉽게 검토하고 검증할 수 있게 하는 것이라고 설명했다.