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

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