Hugging Face 开源 Kimina-Prover-RL 训练管线并发布 1.7B 与 0.6B 模型

Hugging Face 与 AI-MO 开源了 kimina-prover-rl 训练管线，用于 Lean 4 形式化定理证明，采用受 DeepSeek-R1 启发的先推理后生成范式，基于 GRPO 与 Verl 框架，训练配方以 recipe/kimina-prover-rl 形式随 Verl fork 发布。