Logic-Based Software like COQ and Lean
https://www.cxybb.com/article/Cbcwestwolf/84754714
软件基础
cpdt
mcb
Doron Zeilberger
观点184：在数学研究中使用像COQ和Lean这样的逻辑软件是错误的方向，但作为教学工具使用更糟糕
十二年前，我评论过，使用像Coq和Lean这样的逻辑软件来做数学，如Kevin Buzzard所倡导的
（参见Kevin在ICM 2022的精彩演讲，以及Gil Kalai的
精彩帖子）和
Georges Gonthier（参见Gonthier在ICM 2022的迷人演讲），
不是计算机和开发和使用它们的天才人类的最佳用途。
虽然我确实欣赏Avigad等人、Tom Hales、Gonthier和其他人的开创性工作，以政治观点和“闭嘴”所有传统的人类中心和
机器恐惧的怀疑者（例如Michael Harris），但够了！我们不需要更多“正式版本”的人类生成的数学。
形式化已知的证明就像猪拉丁语。一旦你做了几次，就不再有趣了。
虽然这既是智力上和技术上的挑战，否则这些聪明的人不会参与其中，但这些人是在浪费他们的才华。
确实，我们的硅仆人，很快就会成为我们的主人，可以被更有成效地使用。
COQ和Lean继续了有害的希腊传统，引入了公理化方法，使数学成为一种演绎的、以逻辑为中心的科学。
由于惯性，欧几里得的公理化方法延续至今。
当前，人类生成的主流数学之所以如此，是因为这是一个人工制品，历史事实是计算机最近才被发明。
由于人类不得不做点什么，他们发展了一种洛可可风格和内向的所谓“概念数学”知识体系。
如果一个外星人来到我们这里，试图阅读，例如，Langlands计划，它会非常无聊，看不到意义。
现在，Buzzard等人想要进一步推进这一议程，通过教计算机如何模仿，例如，Peter Scholze，并继续这一不幸的2300年传统。
计算机基于算法，所以现在我们有了它们，我们可以抛弃“希腊”、欧几里得、公理化、以逻辑为中心的传统，
如Lean和Coq及其同类所实施的，回到更有成效的传统，即古埃及、巴比伦、中国、印度、波斯和阿拉伯的传统。
换句话说，算法、建设性、明确和具体的数学。
这一传统的自然计算机继承者是计算机代数系统，如SAGE、Maple和Mathematica，而不是Coq和Lean。
数学应该再次成为一种物理科学，而不是对（通常是所谓的）完全严格的宗教狂热痴迷。
当然，所有科学都需要逻辑，但计算机化逻辑，虽然在
软件工程中非常有用，用于验证程序的正确性，但在实验性、经验性、“巴比伦式”数学中没有地位，
希望一旦我们摆脱了对希腊的痴迷，它就会出现。
但真正让我害怕的是，几个月前，我听到一个关于在本科数学课程中使用Lean和Coq的演讲。当前的数学课程已经够糟糕了，灌输我们的学生
希腊风格的数学，但在“引入证明”课程中使用Lean和Coq，
真的太过分了。
| 
