LLM 让符号 AI 老问题复活：自动证明的旧传统值得重读
Amichayg · reddit · 2026-09-07
作者认为当下 AI 话语过度被 ML/LLM 视角塑造，而不少看似全新的进展其实是老想法重新变得可行。
以数学为例：LLM 可能让自动定理证明与形式化方法适用于远更广的数学工作，但其思想脉络可以追溯到《数学原理》、Logic Theorist 与整个符号 AI 传统——许多基础问题很早就被提出，只是被更实用的方法暂时取代。
作者主张重访这些旧传统：自动证明助手这类概念提出的问题，并不因 Lean 或 Agda 加上 LLM 跑通就穷尽。即便 LLM 极擅长操作这些工具，也不会自动浮现关于它们在做什么的最有意思的问题——最好的解释框架可能早已存在于逻辑、自动推理与数学哲学的旧传统中。他总结：当下与其说是 LLM 开创全新智识纲领，不如说是让原本边缘、不可行的纲领重新变得可行。
「漫话AGI」频道最新
- 194 位专家预测:2050 年前重大 AI 灾害事件概率过半 — ben_j_todd · 2026-09-07
- 可解释性研究员：mech interp 必须大幅提速，不能等 8.5 年 — ArthurConmy · 2026-09-07
- AI 风险派回应质疑：如果真相信灭顶之灾，当然要拼命示警 — nabla_theta · 2026-09-07
- AI 检测器把作者原文判 100% AI 生成，非母语者成重灾区 — austinc3301 · 2026-09-07
- 经济学人：AI 在美国净创造超百万岗位，就业末日论推迟 — QuintinPope5 · 2026-09-07
- Hameroff 重提微管量子意识论: aromatic 氨基酸构成「量子地下世界」 — JosephJacks_ · 2026-09-07