更新：OpenMath 从Shentu v2.17.0 开始，OpenMath 现在将 Rocq 和 Lean 证明的奖励分开。 目前，贡献者使用以下系统提交证明： • Rocq • 倾斜 形式化验证工作采用不同的证明系统、独立的奖励机制和明确的归属机制。