David Bessis 认为，随着自动化证明助手和形式化的兴起，传统的定理证明经济正在衰落，数学正转向直觉和可视化。文章批评了系统对定理证明优先权的病态痴迷，而真正的进步往往发生在这一循环之外。 这很重要，因为它标志着数学实践和评估方式的转变，AI 和形式化工具正在挑战学术数学的核心激励结构。它可能将优先权重塑为洞察和理解，而非纯粹的生产定理。 Bessis 指出，在 Lean 等系统中 AI 编写的证明往往无法传达有用的人类洞察，但它们正被越来越多地使用。他主张，从证明过程中获得的直觉比证明本身更有价值。
背景
证明助手是一种软件工具，通过人机协作帮助人类开发形式化证明。形式化验证使用数学方法证明系统的正确性。'定理经济'一词指的是将证明新定理作为数学成就主要货币的学术文化。
参考链接
社区讨论
评论引用了 Greg Egan 小说《Diaspora》中的'真理挖掘'概念，预见形式化之后数学将演变为可视化和洞察。另一条评论将其与软件测试类比，认为数学家可能采用'经过实战检验'的信心文化而非形式化证明。有些人注意到该文章之前在 Hacker News 上的提交记录。