主要证据
- Mathesis: Towards Formal Theorem Proving from Natural LanguagesS1 · 主要研究来源 · 论文 · 2025-06-08
- Mathesis implementation and project resourcesS1 · 主要研究来源 · 代码仓库
- Mathesis — ICLR 2026 conference paperS1 · 主要研究来源 · 论文
Mathesis 将自然语言数学连接到端到端 Lean 定理证明
Mathesis 将非形式题目翻译为 Lean 4 命题，对候选形式化结果的语法与语义质量进行评分，并利用下游证明器反馈偏好能够支撑机器检查证明的命题。Gaokao-Formal 则提供数百道源自中国高考的高难度证明题，用于评测完整管线。
发生了什么？
Mathesis 论文发布了结合强化学习与偏好反馈的自动形式化—证明管线，并提出 LeanScorer 与 Gaokao-Formal 基准；论文报告称，将其自动形式化器与既有证明器配合后，自然语言题目的端到端形式证明准确率获得显著提升。
为什么重要？
该工作让形式数学系统更接近人类实际接收数学问题的方式——自然语言，并把自动形式化质量纳入端到端证明目标，而不是把它仅视为孤立的翻译任务。
重要性说明：Mathesis 针对神经定理证明的重要接口瓶颈，将普通数学语言的学习式自动形式化与后续 Lean 证明生成和反馈连接起来，不再默认任务必须从专家编写的形式命题开始。
历史脉络
证据与状态一览
- 重要性
- H2 · 领域里程碑
- 验证状态
- 论文已发布
- 证据等级
- E3 · 可检查工件
- AI 角色
- AI 自主主导
- 形式保障
- 机器检查
贡献与验证
- 数学新颖性
- 工具性进展
- 接口
- 非形式化, 形式化, 混合
- AI 贡献
- 学习模型自动生成 Lean 命题与后续形式证明，Lean 编译、语义评分和证明器反馈则约束并评估这一自动化管线。
- 人类贡献
- 研究者设计自动形式化训练流程、LeanScorer、Gaokao-Formal 与端到端评测协议，整理题目并分析系统表现。
- 验证状态
- 论文已发布 · E3 · 可检查工件 · 机器检查
- 最后审阅
- 2026-09-14
技术细节
- 系统
- mathesis, mathesis-autoformalizer, leanscorer, lean
- 机构
- huawei
- 数学问题
- natural-language-to-formal-theorem-proving, gaokao-formal
- 方法
- autoformalization, reinforcement-learning, preference-optimization, prover-feedback, lean
全部来源与工件
- Mathesis: Towards Formal Theorem Proving from Natural LanguagesS1 · 主要研究来源 · 论文 · 访问于 2026-09-11
- Mathesis implementation and project resourcesS1 · 主要研究来源 · 代码仓库 · 访问于 2026-09-11
- Mathesis — ICLR 2026 conference paperS1 · 主要研究来源 · 论文 · 访问于 2026-09-11
验证历史
- 2025-06-08 · 论文已发布 · E2 · 研究记录
arXiv 研究记录发布 Mathesis、LeanScorer 与 Gaokao-Formal，并报告端到端形式证明结果。
- 2026-09-11 · 论文已发布 · E3 · 可检查工件
Mathesis 公开仓库提供实现与项目资源，该工作后来发表于 ICLR 2026。machine-checked 指评测证明管线中的结果可由 Lean 接受，并不表示全部实验或语义等价判断均已获得独立重放。
更正
当前没有记录的更正。