PANews 7月21日ニュース、イーサリアムの共同創設者であるVitalik Buterin氏は、LeanやHOLなどの定理証明システムにコンパイル可能な新しい高水準プログラミング言語を探求すべきだと提案した。この言語では、証明プロセスそのものではなく、「定義と定理」の可読性を重点的に最適化する。Vitalik氏は、同言語の目標とするシナリオは、AIが大規模な形式検証済みの証明を出力した後、それらの証明が「形式的に何を証明したのか」を人間が明確に理解できるようにすること、つまりAIが提示する具体的な数学的・論理的主張を読者がより容易に吟味・検証できるようにすることだと述べた。