ヴィタリック：試す価値のある新しい高級プログラミング言語は、定義や定理をより読みやすくするべきだ。

VitalikはXプラットフォームで投稿し、新しい「高級プログラミング言語」がLean（またはHOLなど）にコンパイルされることを試す価値があると述べています。これは、定義や定理を人間ができるだけ読みやすくすることに重点を置いています。証明ではなく、証明は正しければよく、重要なのは定義と定理そのものです。その想定される用途は、AIが大量の証明を出力し、読者がそれらの出力の中で実際にどの正確な主張が証明されたのかをできるだけ簡単に理解する必要があるということです。