斯坦福推出 PaperFormalizer，将论文自动转为 Lean 验证版本

斯坦福团队推出 PaperFormalizer，基于 Lean 的智能体流水线可将论文自动转为形式化验证版本。系统从 LaTeX 源码构建陈述依赖图，审计陈述的忠实性、歧义与正确性，并在 Mathlib、可选领域库及作者工具集下完成形式化和证明。