PaperFormalizer: Author-in-the-Loop Autoformalization of Research Papers in Lean

Jiyuan Tan, Vasilis Syrgkanis, Jose Blanchet

Even a carefully proofread paper can leave small gaps in its proofs or its stated assumptions. We introduce PaperFormalizer, a Lean-based agentic pipeline that helps authors find a…