Vaught 猜想反例获 Lean 形式化验证
roydanroy · x · 2026-10-12
Cameron Freer、Nate Ackerman 与 Robin Knight 合作，基于 Knight 未发表手稿构造出无穷逻辑中 Vaught 猜想的反例，并已在 Lean 定理证明器中完成形式化验证。Vaught 猜想是数理逻辑长期悬而未决的问题，反例若经同行审查确认将是重大成果，而 Lean 形式化为其正确性提供了机器可检验的保证。
「研究」频道最新
- Nature 深度报道:人脑终生新生神经元百年之争仍无定论 — AnnaCiaunica · 2026-10-12
- 论文数据一半是重复行:1168 行样本被指首尾几乎完全相同 — RexDouglass · 2026-10-12
- 独立研究者举报数据异常,复制机构公开承认“我们失败了” — RexDouglass · 2026-10-12
- 巴西数据“像随机生成”:举报者列出可疑相关性与离谱效应量 — RexDouglass · 2026-10-12
- 矩阵即图：线性代数里最被低估的事实 — TivadarDanka · 2026-10-12
- MetaKernelBench:跨DSL技能迁移提升GPU核优化最高29% — encodelab · 2026-10-12