形式化验证证明推箱子全程 3000-3064 步最优,悬赏挑战全球玩家

banteg · x · 2026-11-12

开发者 banteg 发起推箱子(Heroes of Sokoban)三部曲挑战:他声称用形式化验证证明全系列通关需要 3000 到 3064 步,自己卡在最后的 64 步上,公开悬赏——只要有人打破纪录(经原版游戏验证)或推翻其已证明的最小值,奖励归他。

有人随即给出 room III-20 两条达到 84 步的走法序列,感叹「形式化验证再次证明精英」。项目配套的 verified-bar 规范文档详述了「verified」一词的使用门槛:规格公开、独立评审批准、Lean 定理文件、SHA-256 锁定等,大部分检查项由机器完成。