主要证据
- Lean Workbook: A large-scale Lean problem set formalized from natural language math problemsS1 · 主要研究来源 · 论文 · 2024-06-06
- Lean Workbook dataset releaseS1 · 主要研究来源 · 数据集
Lean Workbook 发布大规模形式—非形式数学数据集
迭代式生成与过滤管线把自然语言数学问题翻译为 Lean 4 陈述，并进行反向转换。
发生了什么？
Lean Workbook 发布约 57,000 个形式—非形式问题对、搜索得到的证明以及 21 道新的 IMO 题目。
为什么重要？
该数据集缓解了训练大型 Lean 证明器的关键瓶颈——形式与非形式数学对齐数据稀缺。
重要性说明：Lean Workbook 扩大了自然语言数学与 Lean 形式问题配对数据的规模，为自动形式化和证明训练提供资源。
历史脉络
证据与状态一览
- 重要性
- H2 · 领域里程碑
- 验证状态
- 论文已发布
- 证据等级
- E3 · 可检查工件
- AI 角色
- AI 实质性支持
- 形式保障
- 有形式化工件
贡献与验证
- 数学新颖性
- 工具性进展
- 接口
- 非形式化, 形式化, 混合
- AI 贡献
- 模型参与用于构建数据集的合成翻译与证明搜索。
- 人类贡献
- 研究者设计迭代数据管线、过滤标准与公开发布。
- 验证状态
- 论文已发布 · E3 · 可检查工件 · 有形式化工件
- 最后审阅
- 2026-09-11
技术细节
- 系统
- lean-workbook, lean
- 机构
- shanghai-ai-laboratory
- 数学问题
- formalization-data
- 方法
- synthetic-data, autoformalization, proof-search
全部来源与工件
- Lean Workbook: A large-scale Lean problem set formalized from natural language math problemsS1 · 主要研究来源 · 论文 · 访问于 2026-09-10
- Lean Workbook dataset releaseS1 · 主要研究来源 · 数据集 · 访问于 2026-09-11
验证历史
- 2024-06-06 · 论文已发布 · E2 · 研究记录
Chronicle 依据所引 primary / official source 记录该事件；该状态不表示 Chronicle 已完成独立验证。
- 2026-09-11 · 论文已发布 · E3 · 可检查工件
本轮 corpus 刷新增补了由作者或发布机构维护、可直接检查的公开产物。E3 表示证据已达到可检查 artifact 层级，并不等同于底层科学或数学主张已获得独立验证。
更正
当前没有记录的更正。