PaperFormalizer：基于 Lean 的研究论文作者在环自动形式化工具

PaperFormalizer 是一款基于 Lean 的智能体流水线，通过作者在环机制帮助作者修补证明漏洞，将 LaTeX 论文转化为经 Lean 验证的版本。系统构建命题依赖图并结合 Mathlib 等库进行定理证明，在出现歧义或关键修改时向作者提议并由其裁决。该工具可在 Claude Code 或 Codex 中运行，输出修订论文、变更报告及关联命题的 Lean 代码。