美团 LongCat 发布开源 560B 参数 MoE 模型 LongCat-Flash-Prover，主攻 Lean4 形式化推理

美团 LongCat 在 HuggingFace 发布 560B 参数开源 MoE 模型 LongCat-Flash-Prover，通过智能体工具集成推理（TIR）推进 Lean4 原生形式化推理，将任务拆解为自动形式化、sketching 和证明三项能力，并提出 HisPO 算法稳定 MoE 长程训练。