PaperFormalizer: author-in-the-loop autoformalization pipeline for Lean (arXiv:2610.31810v1)
PaperFormalizer is a Lean-based agentic pipeline that transcribes a paper's LaTeX into a dependency graph of statements, audits each statement for faithfulness/ambiguity/correctness, and formalizes and proves them in Lean against Mathlib and optional libraries. The system runs inside coding agents (Claude Code or Codex), asks the author to resolve ambiguities before changing claims, and outputs an annotated revised paper, a change report, and linked Lean code (repository: github.com/Jiyuan-Tan/PaperFormalizer; shared formalizations at paperformalizer.org).