Kimina-Prover-RL 开源 Lean 4 定理证明训练管线

Hugging Face 开源 Kimina-Prover-RL，一个基于 Verl 的 Lean 4 形式化定理证明训练管线。该管线采用类 R1 的结构化推理范式，引入格式奖励与纠错机制，训练出 1.7B 和 0.6B 模型，在 MiniF2F 基准上刷新开源模型 SOTA。