Vitalik提议新语言提升AI证明可读性

BiRun 消息，以太坊联合创始人Vitalik Buterin提出一种可编译为Lean验证语言的新编程语言。该方案旨在降低技术门槛，使人工智能生成的数学证明声明更易于被人类理解和验证，从而增强AI推理过程的可信度与透明度，促进形式化验证在AI领域的广泛应用。