arXiv cs.AI· Jiyuan Tan, Vasilis Syrgkanis, Jose Blanchet·· 8 天前AI 评分47
PaperFormalizer：基于 Lean 的作者在环论文自动形式化系统
PaperFormalizer: Author-in-the-Loop Autoformalization of Research Papers in Lean
AI 导读
PaperFormalizer 是一款基于 Lean 的智能体流水线，通过“作者在环”机制帮助研究者查找证明漏洞并将 LaTeX 论文转化为 Lean 验证版本。它将论文转录为命题依赖图并审计正确性与歧义，结合 Mathlib 推进形式化证明，并在关键修正时由作者把关决策。该工具可在 Claude Code 或 Codex 中运行，并输出关联 Lean 代码的修订论文与变更报告。
来源：arXiv cs.AI · arxiv.org