**论文称 Medvedev 逻辑不可判定，证明由 ChatGPT 完成、Claude 形式化验证**

_AI proves Medvedev logic is undecidable_

> arXiv 新论文（math.LO）证明有限问题逻辑 Medvedev logic 不可判定，解决了长期悬而未决的公开问题。核心方法是将周期性铺砌问题归约到该逻辑的非定理性；作者用类似技术将普通铺砌问题归约，得出 Skvortsov 无限问题逻辑同样不可判定，并证明两者不同——任何非周期平面铺砌都能区分它们。由于 Medvedev 逻辑涉及命题依赖逻辑的模式片段、拓扑斯内部逻辑等多个领域，该结果具有跨领域影响。论文共 32 页，作者在方法论部分说明主要结果由 ChatGPT Sol 5.6 得出，并由 Claude Opus 5 在 Lean 中形式化验证。

**来源信息**
- **来源**：Hacker News：AI 热帖
- **分类**：论文
- **发布时间**：2026-09-22 01:01（北京时间）
- **原文**：[打开原文](https://arxiv.org/abs/2609.13359)