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

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