Claude 助力补全哥德尔未竟证明：AC 独立性缺口被 AI 辅助研究打通

aran_nayebi · x · 2026-11-14

研究者 arannayebi 透露一个数学史层面的细节：哥德尔当年尝试证明选择公理（AC）独立于类型论时，其证明缺少一个关键定义。据 Jan 的考证，哥德尔其实通过 Mostowski 1939 年的工作（他 1940 年曾研读并抄录）在技术上已经知道这个定义，但在自己的笔记中并未将其与该证明联系起来。

正是 Jan 借助 Claude 辅助完成的构造，首次把这两者连接了起来——即 AI 辅助研究补上了这一历史缺口。