主要证据
- LeanConjecturer: Automatic Generation of Mathematical Conjectures for Theorem ProvingS1 · 主要研究来源 · 论文 · 2025-06-27
- LeanConjecturer generation and evaluation repositoryS1 · 主要研究来源 · 代码仓库
LeanConjecturer 在 Lean 中扩展 LLM 数学猜想生成
该管线从 Lean 文件提取定义与定理上下文，让 LLM 提出新的形式命题，再通过 Lean 检查生成结果，并把更困难的候选分离出来供后续训练。论文还报告若干非平凡拓扑学示例，用以说明系统可以产生具有数学用途的命题，而不仅是表面扰动。
发生了什么？
LeanConjecturer 论文报告从 40 个 Mathlib 种子文件生成 12,289 条大学层次 Lean 猜想，其中 3,776 条通过语法有效性检查且无法被所采用的 `aesop` 非平凡性过滤器直接证明，并展示这些生成问题可用于面向特定领域的定理证明强化学习。
为什么重要？
形式定理证明器高度依赖可用的定理命题与训练任务。LeanConjecturer 提供了从形式数学库本身扩展问题分布的可复现路线，并把猜想生成直接连接到强化学习数据构造。
重要性说明：LeanConjecturer 将猜想生成从定理证明的偶发副产品推进为可扩展的形式数学管线，把 Mathlib 上下文抽取、LLM 生成与 Lean 过滤结合起来，大规模产生候选训练问题。
历史脉络
证据与状态一览
- 重要性
- H2 · 领域里程碑
- 验证状态
- 论文已发布
- 证据等级
- E3 · 可检查工件
- AI 角色
- AI 自主主导
- 形式保障
- 有形式化工件
贡献与验证
- 数学新颖性
- 工具性进展
- 接口
- 形式化, 符号
- AI 贡献
- 语言模型根据抽取出的数学上下文生成候选 Lean 定理命题，Lean 与规则过滤器检查语法和选定的非平凡性标准，再将候选用于后续训练。
- 人类贡献
- 研究者设计上下文抽取与过滤管线，选择种子文件与评测标准，开展强化学习实验，并分析代表性的生成命题。
- 验证状态
- 论文已发布 · E3 · 可检查工件 · 有形式化工件
- 最后审阅
- 2026-09-11
技术细节
- 系统
- leanconjecturer, lean, mathlib
- 机构
- auto-res
- 数学问题
- formal-conjecture-generation, theorem-proving-data-scarcity
- 方法
- conjecture-generation, synthetic-formal-data, context-extraction, reinforcement-learning, lean
全部来源与工件
- LeanConjecturer: Automatic Generation of Mathematical Conjectures for Theorem ProvingS1 · 主要研究来源 · 论文 · 访问于 2026-09-11
- LeanConjecturer generation and evaluation repositoryS1 · 主要研究来源 · 代码仓库 · 访问于 2026-09-11
验证历史
- 2025-06-27 · 论文已发布 · E2 · 研究记录
arXiv 研究记录发布 LeanConjecturer，并报告生成猜想数量、过滤流程与定理证明训练结果。
- 2026-09-11 · 论文已发布 · E3 · 可检查工件
LeanConjecturer 公开仓库提供生成与评测管线；生成数据目录并未提交到仓库，因此 E3 表示实现可直接检查，而不是对论文中的新颖性主张或每一条生成定理完成独立验证。
更正
当前没有记录的更正。