A proof checker can confirm a formal claim is valid, but no checker tells you whether it says what you actually meant.

This explores whether machines can confirm that a formal statement matches the intended meaning, not just whether it is logically valid. The short answer from the corpus: verifiers are very good at the second job and offer no guarantee on the first. A proof assistant like Lean will tell you a theorem follows from its premises. It cannot tell you the theorem says what you had in mind. All the risk sits in the translation step, and that is where LLMs fail in a quiet way. They produce logic that is well-formed and type-checks, yet means something slightly different. The errors cluster in predictable places: which part of a sentence a quantifier covers, "some" vs. "all," and how finely concepts are broken into predicates Can large language models translate natural language to logic faithfully?. A wrong formalization that passes every check is arguably worse than an obvious failure, because the checker's approval makes it look trustworthy.

The same study turns up a useful asymmetry: LLMs seem to understand formal language better than they generate it. That suggests machines may be more reliable at reading a formal statement back and judging it than at writing it in the first place. The problem also runs deeper than single sentences. Meaning in mathematics depends on surrounding definitions and axioms. Translating one statement at a time only works because libraries like Mathlib already supply that context, which hides how much of the meaning lives in the wider theory Can autoformalization work on individual statements alone?. So checking intent means checking whether a whole system of definitions fits together the way you meant, not just one line.

Outside mathematics, the same gap appears in a more practical setting. The interwhen system automatically turns prose policy documents into code-based verifiers, including provably correct Lean and z3 checkers Can we automatically generate formal verifiers from policy text?, and runs them alongside a model's reasoning at almost no extra cost Can verifiers monitor reasoning without slowing generation down?. That works well, but notice where the trust has moved. The checkers are provably correct relative to the LLM's translation of the policy. If that translation misreads the policy, the system enforces the misreading rigorously. This matters because hallucination is formally unavoidable for any computable LLM, so outside safeguards are necessary Can any computable LLM truly avoid hallucinating?. A safeguard built from a model's interpretation inherits that model's blind spots unless something independent checks the specification itself.

This mirrors a pattern seen in reasoning research. Traces that look rigorous often don't reflect what the model actually computed, and invalid steps can perform about as well as valid ones Do reasoning traces show how models actually think? Can we actually trust reasoning model outputs?. Correct form and correct meaning keep separating. Two responses stand out. The Darwin Gödel Machine sets formal proof aside and judges self-modifications by whether they actually improve benchmark scores Can AI systems improve themselves through trial and error?. That swaps "does this mean what I intended?" for "does this do what I wanted?" The Leiden Declaration takes the human route: mathematicians who use AI keep sole responsibility for correctness, because a proof is meant to deliver both certainty and understanding, and formal verification can secure only the first Can AI-generated proofs ever replace human mathematical understanding?.

So the takeaway: formal verification doesn't remove the need for trust. It concentrates it. Everything after the formal statement can be checked mechanically, which makes the translation into that statement the one place where meaning can quietly go wrong. Today that point is protected by human judgment, by empirical testing, or by having a model check translations rather than write them.