AI、智力工作、人类与未来
在这篇发表于 2026 年 10 月 27 日的文章中，作者认为，大语言模型已不能再被看作只是一个更大的搜索引擎：对于形式化的先验问题，它们现在能帮助人类取得此前无法企及的成果，而最新一波进展与 Lean 4 密切相关。文章还讨论了 AI 安全——包括形式化验证与奖励作弊——以及在智力工作被自动化之际，价值与分配的社会问题。之所以值得读，是因为它是对大语言模型四年历程的一次反思性盘点，认为形式化领域将最先被改变，而更难的问题是经济与社会层面的，而不只是技术层面的。
报道来源
- Hacker News (AI)2026-10-27 14:31