이더리움 공동 창립자 비탈릭 부테린은 AI가 생성한 증명의 가독성을 향상시키기 위한 새로운 고급 프로그래밍 언어 개발을 제안했습니다. 이 언어는 Lean과 HOL과 같은 정리 증명 시스템으로 컴파일되며, 증명 과정 자체보다는 "정의와 정리"를 더 이해하기 쉽게 만드는 데 중점을 둡니다. 목표는 인간이 AI가 생성한 증명이 공식적으로 무엇을 확립했는지 명확히 이해할 수 있도록 하여 수학적 및 논리적 주장에 대한 검토와 검증을 더 쉽게 하는 것입니다.