Mechanical verification combined with LLM review catches formalization errors that either method alone would miss, enabling more reliable automated theorem proving pipelines.
This paper presents a verification method for Lean formalizations that combines LLM review with mechanical checks (numerical validation and vacuity detection) to catch errors that LLM judges miss. The authors apply this to autoformalize mathematical functions from NIST's library, creating a partially formalized collection and demonstrating lower error rates than existing verification approaches.