mini-Lean-agent：仅用 bash 工具的 Lean 证明基线
热点事件持续更新
mini-Lean-agent：仅用 bash 工具的 Lean 证明基线
1 篇报道1 个报道来源15 小时前更新
先了解这件事
AI 综述
Tomas Ortega 等作者发布论文，提出 mini-Lean-agent——一个只向模型暴露 bash 工具的极简 Lean 编码代理，用于定理证明任务，并由独立的可信评估器验证最终产物，相关结果已发布于 arXiv cs.AI。 研究者在 Putnam 2025 基准上将其与 AxProverBase、Numina-Lean-Agent 进行对比，以此检验定理证明任务是否真的需要专门的定理证明智能体，而不是通用编码代理。报道未给出对比结果。
AI 根据报道生成 · 1 小时前更新
最新进展10月15日 12:00
mini-Lean-agent：面向 Lean 的编码智能体基线，证明定理证明器是否需要定理证明智能体？报道时间线
沿着报道，了解事件的不同侧面。
10月15日
- arXiv：cs.AImini-Lean-agent：面向 Lean 的编码智能体基线，证明定理证明器是否需要定理证明智能体？
研究者提出 mini-Lean-agent，一个仅暴露 bash 工具的极简 Lean 智能体，由独立的可信评估器验证最终产物，并在 Putnam 2025 基准上与 AxProverBase、Numina-Lean-Agent 对比。
本事件热度走势
还没有足够的连续观测数据，暂不绘制趋势。