Can autoformalization work on individual statements alone?

Autoformalization translates informal natural language into machine-verifiable formal languages, and almost all of it operates statement-by-statement. This position paper argues that framing is a category error: real formalization is inherently theory-level. Before a target theorem like Pythagoras can even be stated, you need an entire "tower" beneath it — axiomatic primitives, derivative definitions, notations, examples, supporting lemmas, proof tactics, and all their inter-dependencies — assembled as a coherent formal library. Statement-level autoformalization only looks tractable because it silently borrows that scaffolding from a prebuilt context like Lean's Mathlib.

The evidence is the sheer cost of real efforts: formalizing the Kepler conjecture — a single statement — took 11 years, almost all spent constructing the web of definitions and lemmas needed to support it. Which means the interesting bottleneck is not translating one sentence faithfully but building and maintaining a self-consistent library of interdependent formal objects.

This sharpens the vault's autoformalization thread. Since Can large language models translate natural language to logic faithfully?, per-statement translation is already unreliable; theory-level formalization compounds that risk because dependency errors propagate — a mis-formalized definition silently corrupts every lemma above it, so semantic-loss failures no longer stay local. It also reframes the trade-off behind Can structured templates replace formal verification for code reasoning?: if full theory-level formalization is this expensive, structured-but-informal scaffolding is not a stopgap but a rational point on the cost curve for most reasoning tasks.