Lean 4

Open-Source Training Pipeline for Formal Theorem Proving in Lean 4 Released

A team has developed Kimina-Prover-RL, an open-source pipeline that trains large language models to solve formal proof goals in Le