PaperFormalizer：作者参与的 Lean 研究论文形式化工具
PaperFormalizer 是一套基于 Lean 的智能体流程，帮助作者发现并弥补论文证明或假设中的漏洞。它从 LaTeX 源文件出发，构建各项陈述的依赖关系图，检查其清晰度和正确性，再用 Lean 进行形式化。如果陈述存在多种解释，或修订方案可能改变论文主张，系统会请作者作出决定。输出包括带注释的修订版论文、变更报告，以及与形式化陈述相关联的 Lean 代码。该工具可在 Claude Code 或 Codex 中运行。
本文来源：Hugging Face，仅供学习参考，版权归原作者所有。