CIC+LEM 竟可证明 Con(ZF)，Mario Carneiro 用 AI 工具获突破
leloykun · x · 2026-09-21
- 数学家 Elliot Glazer 转发称，在 CIC（构造演算的归纳类型论）加排中律（LEM）的体系中竟能证明 Con(ZF)（ZF 集合论的一致性），这在类型论元数学里是出人意料的进展。
- 该发现由 Mario Carneiro 借助 AI 工具 Fable 做出，并且给出了一条在无公理 Lean + LEM 中证明 Con(ZF) 的路径。
- 作者感叹这是类型论元数学“大问题”上久违的实质进展。
「研究」频道最新
- Aletheia's Quest 竞赛落幕：19 支团队 478 份提交角逐 5 万美元测谎奖 — gsarti_ · 2026-09-21
- IntBMoE 提出 block 级稀疏执行 MoE,已上线高德推荐服务数亿用户 — Ran Cheng · 2026-09-21
- 干细胞成像模型量化实测：W4/W8 混合压缩 6.76 倍零失败 — capicu-ai · 2026-09-21
- 新论文：在扩散模型潜空间实现基于物理的渲染 — ssh4net · 2026-09-21
- 陶哲轩谈 AI 加速科研：净收益为正但瓶颈在验证 — paulabartabajo_ · 2026-09-21
- Adaptive Color Grading：KNN 预测影调分区超越端到端模型 — ssh4net · 2026-09-21