主要证据
- MizAR 40 for Mizar 40S1 · 主要研究来源 · 论文 · 2013-10-10
MizAR 40 将 AI/ATP 方法扩展到完整 Mizar Mathematical Library
系统把快速学习式相关性方法扩展到约 15 万条 MML 公式，并部署到 MizAR 在线推理服务。
发生了什么？
2013 年 10 月 10 日论文报告一个 AI/ATP 系统，在 14 CPU 机器上以 30 秒限制自动证明当时 Mizar Mathematical Library 中 40% 的定理。
为什么重要？
该工作使全库规模的形式数学成为机器学习与自动推理集成的实际目标，而不再只是小型 benchmark 实验。
重要性说明：MizAR 40 展示多种学习式前提选择与 ATP 方法能够在完整 Mizar Mathematical Library 规模上运行，把大型形式数学转化为在线 AI 辅助推理服务与全库评测面。
历史脉络
更早进展
—
后续进展
—
相关里程碑
—
证据与状态一览
- 重要性
- H2 · 领域里程碑
- 验证状态
- 论文已发布
- 证据等级
- E2 · 研究记录
- AI 角色
- AI 自主主导
- 形式保障
- 无形式保障
贡献与验证
- 数学新颖性
- 基准结果
- 接口
- 形式化, 符号
- AI 贡献
- 学习式相关性方法选择有用公式，ATP 系统在全库规模上自动尝试证明。
- 人类贡献
- 研究者设计并优化学习方法、ATP 组合、Mizar 翻译与在线服务。
- 验证状态
- 论文已发布 · E2 · 研究记录 · 无形式保障
- 最后审阅
- 2026-09-15
技术细节
- 系统
- mizar, mizar40, mizar-online-reasoning
- 机构
- university-of-innsbruck
- 数学问题
- large-theory-theorem-proving
- 方法
- machine-learning, premise-selection, automated-theorem-proving, large-theory-reasoning
全部来源与工件
- MizAR 40 for Mizar 40S1 · 主要研究来源 · 论文 · 访问于 2026-09-15
验证历史
- 2013-10-10 · 论文已发布 · E2 · 研究记录
arXiv 论文确认系统并报告全库评测；Chronicle 不把该百分比视为独立复现结果。
更正
当前没有记录的更正。