Kimina-Prover-RL：开源 Lean 4 形式化定理证明训练管线发布

Numina 与 Kimi 开源 kimina-prover-rl，一个基于 DeepSeek-R1 推理范式、与 Verl 完全兼容的 Lean 4 形式化定理证明训练管线，采用 GRPO 强化学习并配套 kimina-lean-server 验证服务。