Kimina-Prover-RL：开源 Lean 4 定理证明训练管线，兼容 verl

Hugging Face 发布开源训练管线 kimina-prover-rl，用于 Lean 4 形式化定理证明，基于 DeepSeek-R1 启发的"先推理后生成"范式，并完全兼容 verl 框架。