更新：OpenMath 随着 Shentu v2.17.0 的发布，OpenMath 现在为 Rocq 和 Lean 证明分开奖励。 贡献者目前使用以下系统提交证明： • Rocq • Lean 不同的证明系统，独立的奖励流以及对形式验证工作的明确归属。