极客用 Lean 语言完整重写《毁灭战士》,还顺手加了形式化证明
akbirthko · x · 2026-10-04
受数学证明与 Lean 形式化启发的开发者 @145k4 发布了 (Lean)DOOM:用 Lean 语言(而非 C)完整实现的《毁灭战士》移植版。作者表示好奇数学证明和 Lean 形式化后,发现 Lean 也能做通用编程,于是用它写了整个游戏,并在合适的地方(目前已有几处)加入了真正可验证的形式化证明。项目已开源,是 Lean 通用编程能力的一次趣味展示。
「编程与Agent」频道最新
- Grok 驱动 codex 自主管跑 10 小时不间断,称任务需一周 — mazzaTalk · 2026-10-04
- 开源 Ramen 0.6.0:GKE/EKS 上多可用区自托管 MCP 服务 — Ok_Plum3595 · 2026-10-04
- 开源 proxy 配置让本地 Gemma 无缝接入 Codex 使用 — TheZachMueller · 2026-10-04
- Agent 大规模抓取网页三个月踩坑:IP 封禁与级联限流 — oatmealdaddy4 · 2026-10-04
- 开发者开源跨会话记忆 MCP 服务器 CRBRO,并用真实 Agent 实测 12/12 — AntonioJBer · 2026-10-04
- Simon Willison:AI 服务需要默认硬性预算上限 — elffjs · 2026-10-04