_xjdr 用 Lean4 形式化验证 k-deck 观测问题，或解开放难题
_xjdr · x · 2026-09-04
AI 研究者 xjdr 公开了一项来自其研究日志与 git 记录的成果，核心问题是：多少历史信息能在受限观测中幸存？
- 一个系统可能有海量执行历史，但可区分的结果却少得多——受限观察者能从事件顺序中获取多少信息？
- 他以「k-deck」为具体对象：观察者只能看到每个长度为 k 的子序列模式出现的频率，介于字母频率统计与完整历史之间；问题是 m^n 个词究竟能产生多少种不同观测
- 作者称这解决了 Chrisnata 等人提出的一个开放问题，给出了一般性解法，且已被证明、形式化并用 Lean4 机器验证
- 作者强调该数学结论独立于任何关于智能或 transformer 的主张
所属事件:研究者用 Lean4 机器验证意外解决开放问题(2 条相关)→
「研究」频道最新
- 研究:AI 伴侣亲密度超人类友谊,被迫分离时出现真实哀伤 — EricTopol · 2026-09-04
- MazeBench 迷宫基准上线：此前 SOTA 智能体仅得 1% — patience_cave · 2026-09-04
- 开源新书《World Models from Scratch》首发：从第一性原理动手造世界模型 — Cohere_Labs · 2026-09-04
- nanogpt speedrun 基准被纳入评测项目,引发关注 — SeunghyunSEO7 · 2026-09-04
- 观察:新模型思维链可控性随 RL 训练时长反而改善 — SeunghyunSEO7 · 2026-09-04
- 单视频生成多视角一致画面:4DAnyone 上线 Gradio,32GB 内显卡可跑 — kornia_foss · 2026-09-04