215 态图灵机 K215 停机当且仅当 ZFC 不一致,获形式化验证
teortaxesTex · x · 2026-10-24
数学家 Elliot Glazer 宣布完成一个经 Metamath Zero 机器验证的 Peano 算术证明:215 态图灵机 K215 停机,当且仅当 ZFC 集合论公理系统不一致。
- K215 由 @ereliuereteer 发现,编码了 Glazer 提出的单模式集合论 K
- 证明在 MM0 中形式化,定理陈述逐字复制自 pa-mm0 目标文件,并附 sha256 校验
- 「停机」被精确定义为:从空白纸带运行 K215 转移表,若干步后到达停机标签;「不一致」则编码为存在 ZFC 对矛盾的数值化证明
这类构造把图灵机停机问题与集合论一致性挂钩,是 Busy Beaver 风格研究向集合论强度推进的标志性成果。
「研究」频道最新
- Agima 智能体靠「想象未来」规划，硬任务成绩 2%→40% — RulinShao · 2026-10-24
- ID-TAP：用对决式老虎机在有限交互内实现 LLM Agent 实时个性化 — Jie Mao · 2026-10-24
- USC 论文揭「马赛克泄露」：LLM Agent 拼合多份机密文档泄露敏感结论 — UniversityofSouthernCalifornia · 2026-10-24
- 港中深等提出 IF-MAP：用影响函数定位多智能体系统最值得优化的 Agent — Jie Mao · 2026-10-24
- NYU 推出 AskChem：让化学论文中的发现可搜索并附证据链接 — kchonyc · 2026-10-24
- Realtime-Bench：最强模型也只能可靠完成 36% 实时任务 — EliasEskin · 2026-10-24