Google DeepMind 开源 cryptids:用 Lean 形式化验证小型图灵机难题
soumitrashukla9 · x · 2026-10-20
Google DeepMind 开源了 cryptids 项目(Apache-2.0),包含两个 Lean 4 形式化库,研究停机行为编码了深层数学问题或复杂动力学的小型图灵机。项目围绕 Busy Beaver 挑战展开,提供了形式化的猜想验证(conjecture-checking)框架、基线与验证脚本,目标是把「小型图灵机的停机行为」这类cryptid级难题变成可被 Lean 证明助手严格检验的对象。.
「研究」频道最新
- Axiom Math 联合经济学家开源 MathEconLib：用 Lean 4 机器验证经济学定理 — soumitrashukla9 · 2026-10-23
- 数学家 Ken Ono 呼吁社区共建 MathEcon：经济学定理的 Lean 4 机器证明库 — soumitrashukla9 · 2026-10-23
- IFM 开源 RL360:8192 并发沙箱、130 万 rollouts 的 RL 基建 — rupspace · 2026-10-23
- 号称匹敌 GPT-6.1 的 DNA 模型遭实测打脸：10 例 8 例不如随机 — anshulkundaje · 2026-10-23
- AI 揭穿阴谋论研究风波落幕：Science 撤回关注声明，结论不变 — DG_Rand · 2026-10-23
- Embodied First Exam：一行代码在 44 台机器人上考你的 Agent — ManlingLi_ · 2026-10-23