LeanFlow: A Case Study in Workflow-Driven Lean Autoformalization

We present and evaluate \method, an LLM agent system specialized for translating mathematical papers into buildable \lean projects. Recent verifier-in-the-loop systems show that large formal artifacts can be produced, but it remains unclear which runtime mechanisms affect completion, auditability, or efficiency in document-to-project formalization. We study this question through case studies on two previously unformalized mathematical papers in number theory and measure theory, using model, proof-workflow, and toolset ablations with \kimi and \gpt; we report task outcome, API calls, input tokens, and output tokens. With \kimi, the full workflow completes both document-level projects within the 2000-call budget, while no-queue variants reach the budget limit; with \gpt, all document-level variants complete, and the full workflow has the lowest or tied-lowest input-token cost on both sources. As complementary calibration, \method reaches 75.7\% BEq+ on the PFR slice of RLM25 and solves all five ICML 2026 AI for Math TCS challenge projects in our \gpt runs.