主要证据
- LEGO-Prover: Neural Theorem Proving with Growing LibrariesS1 · 主要研究来源 · 论文 · 2023-10-01
- LEGO-Prover implementation and generated skillsS1 · 主要研究来源 · 代码仓库
- LEGO-Prover: Neural Theorem Proving with Growing LibrariesS1 · 主要研究来源 · 论文 · 2024-05-07
LEGO-Prover 在证明过程中持续扩展可复用的机器检查引理库
该系统通过共享技能库连接 prover 与 evolver：prover 利用检索到的和新生成的引理构造模块化证明，evolver 则对已验证技能进行变换，以提高其通用性、可复用性与复杂度。
发生了什么？
LEGO-Prover 将 miniF2F 问题分解为子目标引理，检索或生成可复用技能，通过 PISA 调用 Isabelle 进行验证，并在增长式技能库中积累超过 20,000 个技能；论文报告 miniF2F-valid 通过率达到 57.0%，且新增技能能够带来性能提升。
为什么重要？
它提供了较早的“累积式形式推理”具体设计：成功的证明片段不会在单个定理解决后消失，而是转化为后续证明可继续使用的持久资源。
重要性说明：LEGO-Prover 把持续增长的可复用、机器检查引理库直接纳入证明循环，从固定定理库和一次性证明轨迹迈向能够为后续问题积累形式技能的路线。
历史脉络
证据与状态一览
- 重要性
- H2 · 领域里程碑
- 验证状态
- 论文已发布
- 证据等级
- E3 · 可检查工件
- AI 角色
- AI 主导、人类核验
- 形式保障
- 有形式化工件
贡献与验证
- 数学新颖性
- 工具性进展
- 接口
- 形式化, 符号, 混合
- AI 贡献
- 大语言模型提出子目标引理、证明块和技能变换，Isabelle 则在技能进入可复用库之前对形式代码进行机械检查。
- 人类贡献
- 研究者设计 prover/evolver 架构、技能库生命周期、检索与提示流程，集成 PISA 和 Isabelle，并在 miniF2F 上评测系统。
- 验证状态
- 论文已发布 · E3 · 可检查工件 · 有形式化工件
- 最后审阅
- 2026-09-11
技术细节
- 系统
- lego-prover, isabelle, pisa
- 机构
- —
- 数学问题
- minif2f
- 方法
- theorem-proving, growing-skill-library, lemma-generation, retrieval, modular-proof-construction
全部来源与工件
- LEGO-Prover: Neural Theorem Proving with Growing LibrariesS1 · 主要研究来源 · 论文 · 访问于 2026-09-11
- LEGO-Prover implementation and generated skillsS1 · 主要研究来源 · 代码仓库 · 访问于 2026-09-11
- LEGO-Prover: Neural Theorem Proving with Growing LibrariesS1 · 主要研究来源 · 论文 · 访问于 2026-09-11
验证历史
- 2023-10-01 · 论文已发布 · E2 · 研究记录
公开研究记录提出增长式已验证技能库架构，并报告 miniF2F 评测结果。
- 2026-09-11 · 论文已发布 · E3 · 可检查工件
作者公开仓库提供 LEGO-Prover 实现、miniF2F 集成与生成结果。E3 表示产物可检查，并不表示论文实验已经获得独立重放。
更正
当前没有记录的更正。