What Has Actually Been Proved? Auditable Paper-to-Lean Alignment with LeanTrail

Compiler feedback certifies that Lean accepts a declaration, not that the declaration captures the intended result: a repository can compile while a central theorem is weakened, merely auxiliary, or transitively dependent on sorry. Formalization progress should instead be measured against the source paper, in terms of its paper items: definitions, lemmas, and theorems. LeanTrail implements this view as a post-hoc, tool-agnostic audit: deterministic retrieval proposes candidate counterparts for each paper item in the Lean repository and, when available, the Blueprint; a language model judges statement-level correspondence, only among those candidates; and proof completeness comes from a deterministic transitive dependency audit never exposed to the model. Fusion assigns each item one of five coverage states, from Formalized to Missing, each backed by inspectable evidence. On consensus annotations of 98 items from three Lean projects, with three runs of each of two judge models, LeanTrail assigns the correct coverage state to 91.8% (Gemini 3.8 Flash) and 92.5% (GPT-6 Sol) of items. 96–97 of the 98 states are identical across runs, and GPT-6 Sol never reports a Partial item as Formalized. Uncovered items form a natural task queue for formalization agents, anchored to the specification rather than the compiler.