Vitalik提議新語言提昇AI証明可讀性

BiRun 消息，以太坊聯閤創始人Vitalik Buterin提出一種可編譯為Lean驗証語言的新編程語言。該方案旨在降低技術門檻，使人工智能生成的數學証明聲明更易於被人類理解和驗証，從而增強AI推理過程的可信度與透明度，促進形式化驗証在AI領域的廣氾應用。