SCOPE: Certified Theorem Proving with a Language Model as the Policy Planner.

arXiv:2610.08319v2 Announce Type: replace Abstract: In proof assistants such as Lean, a generated proof must pass machine compilation checks, so evaluation needs no human scoring. Direct generation fails on multi-step numeric propositions: a proof is valid onl