Dietterich：Lean 检查器加持下 LLM 证明仍非插值

在 LLM 能否产生新数学结果的争论中，Thomas Dietterich 回应「计算无法产出超过输入信息」的信息论质疑，指出 Lean 证明检查器可为 LLM 提供外部信息来源。他进一步让步讨论称，即使将检查器视为系统内部、没有新信息进入，整个过程也只是把检查器中隐含的知识通过计算显式化，因此依然不属于对既有数据的插值。

2026-10-11 ~ 2026-10-11 · 2 条相关

• Dietterich:Lean 证明检查器提供外部信息,LLM 证明不是插值 — tdietterich · 2026-10-11
• Dietterich 补充:即使 Lean 检查器在系统内,也不是插值 — tdietterich · 2026-10-11