Proof autoformalization aims to generate formal proofs from natural-language (NL) statements. While large language models (LLMs) show promise, they struggle with accuracy on complex proofs, and their size and cost limit broader use. We evaluate the LLM mistral-large-2411 on the Herald dataset, a large collection of aligned informal and formal Lean proofs. Our analysis reveals common model errors and structural issues in the dataset, including data leakage. Using iterative prompt refinement and practical fixes, we improve formalization quality. This work highlights both the potential and current limits of prompt-based autoformalization.