更新：OpenMath 從Shentu v2.17.0 開始，OpenMath 現在將 Rocq 和 Lean 證明的獎勵分開。 目前，貢獻者使用以下系統提交證明： • Rocq • 傾斜 形式化驗證工作採用不同的證明系統、獨立的獎勵機制和明確的歸屬機制。