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