**PaperFormalizer：人机协作将学术论文自动转化为 Lean 形式化证明**

_PaperFormalizer: Author-in-the-Loop Autoformalization of Research Papers in Lean_

> PaperFormalizer 是一款基于 Lean 的智能代理管道，旨在帮助作者发现并修复论文中的证明漏洞。该系统从 LaTeX 源码出发，自动构建陈述依赖图，并通过自然语言审计其准确性。在将论文形式化为 Lean 代码时，若遇到歧义或需人工干预的修复方案，系统会暂停并请求作者确认，确保最终输出的形式化版本忠实于原意，从而提升数学研究的严谨性与可复用性。

**来源信息**
- **来源**：HuggingFace Daily Papers（社区热门论文）
- **分类**：ai-models
- **发布时间**：2026-10-26 08:00（北京时间）
- **原文**：[打开原文](https://huggingface.co/papers/2610.31810)