Lean Proof Assistant as Process Oracle Improves RL for Theorem Proving

Using Lean's elaboration engine as a tactic-level process oracle, this approach supplies dense, verifier-grounded credit signals during GRPO-style RL training rather than relying on a single binary outcome reward. First-error propagation and first-token credit methods balance outcome- and process-level advantages, improving formal theorem proving performance.