主要证据
- ProofNet: Autoformalizing and Formally Proving Undergraduate-Level MathematicsS1 · 主要研究来源 · 论文 · 2023-02-24
- ProofNet benchmark and replication repositoryS1 · 主要研究来源 · 代码仓库
ProofNet 建立本科数学自动形式化与形式证明基准
该基准覆盖分析、线性代数、抽象代数、拓扑等本科教材数学。
发生了什么？
ProofNet 引入 371 个本科层次样例，将自然语言定理陈述与证明和 Lean 3 形式陈述配对。
为什么重要？
它为衡量模型能否把普通数学文本转化为证明助手表示建立了共享目标。
重要性说明：ProofNet 把评测从奥赛题扩展到本科教材数学，并配对自然语言陈述、证明与 Lean 形式化。
历史脉络
证据与状态一览
- 重要性
- H2 · 领域里程碑
- 验证状态
- 论文已发布
- 证据等级
- E3 · 可检查工件
- AI 角色
- 仅计算支持
- 形式保障
- 有形式化工件
贡献与验证
- 数学新颖性
- 工具性进展
- 接口
- 非形式化, 形式化, 混合
- AI 贡献
- 模型在该基准构建的自动形式化与形式证明任务上接受评测。
- 人类贡献
- 研究者整理教材题目、自然语言证明与对应 Lean 陈述。
- 验证状态
- 论文已发布 · E3 · 可检查工件 · 有形式化工件
- 最后审阅
- 2026-09-14
技术细节
- 系统
- proofnet, lean
- 机构
- yale, carnegie-mellon-university
- 数学问题
- undergraduate-mathematics
- 方法
- benchmarking, autoformalization
全部来源与工件
- ProofNet: Autoformalizing and Formally Proving Undergraduate-Level MathematicsS1 · 主要研究来源 · 论文 · 访问于 2026-09-10
- ProofNet benchmark and replication repositoryS1 · 主要研究来源 · 代码仓库 · 访问于 2026-09-11
验证历史
- 2023-02-24 · 论文已发布 · E2 · 研究记录
Chronicle 依据所引 primary / official source 记录该事件；该状态不表示 Chronicle 已完成独立验证。
- 2026-09-11 · 论文已发布 · E3 · 可检查工件
本轮 corpus 刷新增补了由作者或发布机构维护、可直接检查的公开产物。E3 表示证据已达到可检查 artifact 层级，并不等同于底层科学或数学主张已获得独立验证。
更正
当前没有记录的更正。