斯坦福 PaperFormalizer：把论文自动转成 Lean 验证版本
StanfordUniversity · hf · 2026-10-27
斯坦福团队推出 PaperFormalizer，一个基于 Lean 的 agentic 流水线，帮助论文作者发现并填补证明与假设中的小缺口，把论文变成 Lean 验证版本。已在 Claude Code 或 Codex 中运行，代码开源。
- 从 LaTeX 源码出发，把论文转写成陈述的依赖图；
- 用自然语言审计每条陈述的忠实性、歧义与正确性；
- 在 Mathlib、可选领域库和作者个人工具集下形式化并证明各陈述；
- 遇到有多种解读的陈述会停下来询问作者，每个修复以自然语言+TeX 符号呈现为可接受/拒绝/改向的提案；
- 输出标注修订版论文、变更报告和逐条链接到陈述的 Lean 代码。
作者工具集随形式化论文增多而增长，作者可共享已验证论文供后续研究者复用 Lean 代码。项目地址：github.com/Jiyuan-Tan/PaperFormalizer，已验证论文见 paperformalizer.org。
「编程与Agent」频道最新
- Agent Field Kit 上线：为生产级 Agent 提供 $29 起的安全应急手册 — alvelda · 2026-10-27
- 用去审查版 GLM 绕开 Claude 拒答： SS7 威胁建模工作流 — l4rz · 2026-10-27
- Cloudflare Durable Objects 被验证为 AI agent 高并发场景优选架构 — tristanbob · 2026-10-27
- GitHub Next 发布 Chopin:实时多人的 Agent 协作规划环境原型 — max__drake · 2026-10-27
- TMLR 论文：更强推理不等于更充分披露，Agent 思考越多未必告知越全 — SharonYixuanLi · 2026-10-27
- 作者称全由 LLM 编写的 Rust 库 bbtree 实测：快是真的，省内存翻车 — lmoroney · 2026-10-27