数学家应了解的 Lean 定理证明器:关于可靠性与人工智能的... 笔记

数学家应了解的 Lean 定理证明器:关于可靠性与人工智能的问题

[本文来自托马斯·黑尔斯的客座文章。本博客文章最初以不同的文件格式撰写,并使用人工智能进行了转换。— T.] 数学家们一直在阐述他们重视的数学特质。对我而言,至关重要的是数学的一致性,以及其在支撑科学与文明方面无与伦比的可靠性。[……]