Kimina-Prover-RL：开源 Lean 4 定理证明训练流水线，兼容 Verl

Kimina Prover 团队开源了 kimina-prover-rl 训练流水线，用于在 Lean 4 中训练形式化定理证明模型，基于 DeepSeek-R1 启发的"先推理后生成"范式，并完全兼容开源 Verl 框架。