A proof checker will accept an AI's math translation without knowing whether it says what the original sentence meant.

This explores the gap between a formal statement that is *valid* (it compiles, type-checks, and can be checked by a tool like Lean) and one that is *faithful* (it captures what the original English sentence meant). The short version is that a verifier can only check the formal object it is given. It has no way to know whether that object is the right translation. The corpus suggests the hard part of autoformalization sits in exactly that blind spot.

The most direct evidence comes from work showing that LLMs reliably produce well-formed logic that means the wrong thing Can large language models translate natural language to logic faithfully?. The errors cluster in predictable places. One is scope ambiguity: does 'every student read a book' mean one shared book or possibly different ones? Others are quantifier precision ('some' vs. 'at least one' vs. 'exactly one') and predicate granularity (how finely a concept gets split into logical parts). Each of these produces a statement that passes every syntax check and may even be provable, but it proves something nobody asked about. The same work found that models read formal language better than they write it. So checking a translation may be easier than producing one, which is a useful asymmetry if you build pipelines around it.

A second, less obvious point is that faithfulness may not be judgeable one statement at a time. One note argues that autoformalization has to target whole theories, because even a single theorem depends on a web of definitions, axioms, and lemmas Can autoformalization work on individual statements alone?. Statement-level systems look successful partly because they borrow those definitions from prebuilt libraries like Mathlib. That means a statement's meaning depends on what its terms are defined as elsewhere. A formalization can be locally correct and verified while resting on a library definition that doesn't quite match the mathematician's intent.

The same split between 'formally guaranteed' and 'semantically right' appears well outside mathematics. In multi-agent validator systems, the protocol can deterministically guarantee that validators *agree*, but whether they agree on something *correct* can only be bounded statistically Can validator consensus guarantee both agreement and semantic correctness?. The verification-from-policy work has the same exposure: when an LLM turns prose policy documents into provably correct Lean or z3 checkers, the checker is sound only relative to the translation the LLM made Can we automatically generate formal verifiers from policy text?. Formal machinery moves the trust problem to the translation step. It doesn't remove it.

If faithfulness is the bottleneck, the corpus points to some practical moves. Structured 'semi-formal' templates borrow the discipline of formal methods, such as forcing every case to be covered and blocking unsupported claims, without full formalization Can structured templates replace formal verification for code reasoning?. That suggests faithfulness checks could be scaffolded the same way. And because models over-trust their own outputs Why do models trust their own generated answers?, the model that produced a formalization is a poor judge of whether it is faithful. Comparing it against alternative translations, or putting more inference-time effort into verification Can verification accuracy scale without training models?, is more promising. One caveat: the corpus has only one note that measures the faithfulness gap directly. The rest is adjacent framing, not a body of autoformalization benchmarks.