Risk-Controlled Lean-as-Judge for Natural-Language Mathematical Reasoning
arXiv:2605.28365v1 Announce Type: new Abstract: Lean is increasingly used to judge natural-language mathematical answers, but its signal is partial: many answers never formalize, and a failed proof ma