It Compiles. Now What? Assessing Research-Level Autoformalization Beyond Correctness

While automated theorem proving has made significant progress recently, verifying the correctness of proofs is still a bottleneck. Proof assistants such as Lean are used to ensure correctness. However, kernel acceptance alone cannot guarantee that generated mathematics is readable, modular, or mathematically insightful. While AI can consistently generate kernel-accepted proofs, whether that code is intelligible, organized, and structurally sound remains an open question. To this end, we present a structural audit of 208 new autonomously generated solutions to the LeanEval benchmark. Spanning 4.2 million lines of Lean code and 210,000 declarations, this corpus represents one of the largest datasets of machine-checked research-level formal proofs studied to date. We evaluate proof style, dependency graph, import hygiene, documentation, code reuse, and computational efficiency against human-written formalization projects. Our analysis reveals two distinct categories of code defects. Hygiene issues like compiler warnings, monolithic imports, and thin documentation reflect permissive benchmark checkers and are easily fixed by CI linters. In contrast, persistent AI generation patterns like dense forward reasoning and term-mode avoidance cannot be easily detected by automated tools. We release our evaluation pipeline, arguing that structural audits must complement pass rates on formalization benchmarks.