Paper2Lean: Agentic Autoformalization of Mathematical Research Papers at Scale

Formalizing a mathematical research paper requires more than translating isolated theorems: statements and proofs must remain semantically faithful to the source and globally consistent across long-range dependencies. We introduce Paper2Lean, an end-to-end agentic framework that converts mathematical research papers into integrated Lean projects. The framework extracts mathematical content into a dependency graph and coordinates specialized agents for statement formalization, semantic checking and repair, proof construction, and project integration. We evaluate Paper2Lean on 20 mathematical optimization research papers, using mathlib and a shared library of supporting results. All 20 automatically generated projects compile successfully without proof placeholders. Following human review and semantic repair, we introduce OptPaper-20, a corpus of 20 corrected paper-level formalizations comprising 494 Lean files and 110,910 lines of Lean code. All released projects pass clean builds, with no unresolved discrepancies identified in the audit. These results demonstrate the feasibility of agentic paper-level formalization while highlighting semantic fidelity as a central challenge beyond proof verification. The source code and dataset are publicly available at https://anonymous.4open.science/r/Paper2Lean-5A6D/.