イーサリアムの共同創設者であるヴィタリック・ブテリンは、AI生成の証明の可読性を向上させることを目的とした新しい高水準プログラミング言語の開発を提案しました。この言語はLeanやHOLのような定理証明システムにコンパイルされ、「定義や定理」をより理解しやすくすることに重点を置いており、証明過程自体ではありません。目的は、人間がAI生成の証明によって正式に確立された内容を明確に理解できるようにし、数学的および論理的主張の検証や確認を容易にすることです。