根據 1M AI News 監測，美團 LongCat 團隊開源了 LongCat-Flash-Prover，一個 5600 億參數的 MoE 模型，專注於形式化定理證明語言 Lean4 的數學推理任務。模型權重以 MIT 協議發布，已上線 GitHub、Hugging Face 和 ModelScope。
模型將形式化推理拆解為三項獨立能力：自動形式化（將自然語言數學問題轉化為 Lean4 形式語句）、草圖生成（產出引理風格的證明框架）和完整證明生成。三項能力均通過 Agent 工具集成推理（TIR）與 Lean4 編譯器實時交互驗證。
在訓練方面，團隊提出 Hybrid-Experts Iteration Framework 以生成冷啟動數據，並在強化學習階段引入 HisPO 算法以穩定 MoE 模型的長程任務訓練，同時加入定理一致性與合法性檢測機制以防止 reward hacking。
基準測試顯示，LongCat-Flash-Prover 在開源權重模型中刷新了自動形式化和定理證明兩項 SOTA。在 MiniF2F-Test 上僅用 72 次推理即達 97.1% 通過率，ProverBench 和 PutnamBench 分別達到 70.8% 和 41.5%，每題推理次數不超過 220 次。