Kimina-Prover-RL 开源训练管线发布，1.7B 模型刷新 MiniF2F SOTA

Hugging Face 开源 Kimina-Prover-RL 训练管线，基于 DeepSeek-R1 范式与 Verl 框架实现 Lean 4 定理证明。配套发布的 AI-MO/Kimina-Prover-RL-1.7B 在 MiniF2F 基准 Pass@32 达 76.63%，0.6B 版本达 71.30%，均创同尺寸开源模型新纪录。