PaperFormalizer：作者在环的 Lean 论文形式化工具
PaperFormalizer: Author-in-the-Loop Autoformalization of Research Papers in Lean
AI 导读
PaperFormalizer 是一个基于 Lean 的智能体流水线，帮助论文作者发现并修补证明与假设中的漏洞，将论文转化为经 Lean 验证的版本。它从 LaTeX 源码出发，将论文转录为陈述依赖图，逐条审查忠实性、歧义与正确性，再基于 Mathlib 等库形式化证明；凡陈述存在多种读法即暂停并交由作者决定。
正文 · 原文
Abstract: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 and close such gaps in their own papers and turn each paper into a Lean-verified version. Starting from the LaTeX source, PaperFormalizer transcribes the paper into a dependency graph of statements, audits each statement in natural language for faithfulness, ambiguity and correctness, and then formalizes and proves the statements in Lean against Mathlib, optional domain libraries and the author's personal toolkit. Only the author knows what a statement is meant to say and how a formalization gap in a result is best fixed. The pipeline therefore stops and asks the author whenever a statement admits more than one reading, presents every repair, in natural language and TeX symbols, as a proposal that the author can accept, decline or redirect, and leaves to the author every decision that could potentially change what the paper claims. The output is an annotated and revised version of the paper, a report of the changes, and Lean code in which each declaration is linked to the statement it formalizes. The author's toolkit grows as more papers are formalized, and authors can share their verified papers so that researchers who build on them can reuse their Lean code. By making verified papers practical to produce, PaperFormalizer aims to make research that rests on mathematical proofs more robust. PaperFormalizer runs inside a coding agent (Claude Code or Codex) and is available at this https URL. Papers with Lean code shared by users are available at this https URL.
| Subjects: | Artificial Intelligence (cs.AI); Logic in Computer Science (cs.LO) |
| Cite as: | arXiv:2610.31810 [cs.AI] |
| (or arXiv:2610.31810v1 [cs.AI] for this version) | |
| https://doi.org/10.48550/arXiv.2610.31810 arXiv-issued DOI via DataCite (pending registration) |
Submission history
From: Jiyuan Tan [view email]
[v1]
Thu, 22 Oct 2026 18:46:53 UTC (1,452 KB)
来源：arXiv cs.AI · arxiv.org