Agentic autoformalization can produce provable Lean statements that are unfaithful to the source. Examples include changed domains, signs, or branch conventions, and contradictory hypotheses. Existing faithfulness checks rely mostly on LLM or trained-model judges.

A layered verification stack combines an LLM semantic check (direct inspection plus back-translation of comment-stripped Lean), a mechanical numerical check of statements, and a post-proof vacuity check. This is integrated into an Extract–Verify–Prove pipeline with a dependency DAG and human gates. The pipeline is used to build FLMF, a partial Lean formalization of the NIST Digital Library of Mathematical Functions. The method is evaluated on 1,810 informal–formal pairs from FLMF, ProofNet, Beyond Compilation, and RLM25.

The method had the lowest accepted-error rate of the evaluated methods on all three labeled datasets, for example 4.8% on FLMF versus 15.7% for GPT-5.5. Expert review found translation and source defects in existing datasets and misprints in DLMF itself.