注意深く校正された論文であっても、証明や前提に小さな隙間が残ることがある。PaperFormalizer は、Lean を基盤としたエージェント型パイプラインによって、著者自身がそうした隙間を見つけて埋め、論文を Lean で検証済みの版へと変えることを支援する。本論文は Jiyuan Tan らによって 2026 年 10 月 22 日に arXiv に投稿された。
出発点は論文の LaTeX ソースである。PaperFormalizer はまず論文を陈述の依存グラフへと書き換え、定義・補題・定理・系などのあいだの依存関係を明示する。続いて各陈述を自然言語のレベルで監査し、原文への忠実さ、曖昧さの有無、正しさを確認する。この段階では形式化を急がず、自然言語の記述そのものが検討に耐えるかを確かめる。
監査の後、パイプラインは陈述を Lean で形式化し、証明を試みる。前提となるライブラリには Mathlib、任意の領域ライブラリ、そして著者個人のツールキットが含まれる。形式化された論文が増えるにつれて、著者のツールキットも育っていくことが期待されている。
論文が強調するのは、ある陈述が何を意味するのか、また結果に生じた形式化の隙間をどう埋めるのが最善かは、著者だけが知っているという点である。そのためパイプラインは、意味の判断に関わる決定を著者に委ねるよう設計されている。陈述が複数の読み方を許すときは処理を止めて著者に尋ね、修正案はすべて自然言語と TeX 記号で提示し、著者はそれを承認・却下・方向転換できる。論文の主張を変えうる決定も、すべて著者に委ねられる。
最終的な成果物は三つある。注釈と改訂を施した論文、変更点をまとめたレポート、そして Lean コードである。Lean コードでは各宣言が形式化対象の陈述にリンクされ、対応関係をたどれる。著者は検証済みの論文を共有でき、それを基に研究を進める研究者は Lean コードを再利用できる。
PaperFormalizer は Claude Code や Codex といったコーディングエージェント上で動作する。コードは GitHub で公開されており、利用者が Lean コードを共有した論文は paperformalizer.org で公開されている。検証済みの論文を現実的に生み出せるようにすることで、数学的証明に依拠する研究をより堅牢にすることが狙いである。