研究者提出仅用 bash 的 Lean 定理证明智能体

Tomas Ortega 等研究者提出 mini-Lean-agent，一个面向 Lean 定理证明任务的极简编码智能体：模型可见的工具只有 bash，最终结果由独立可信评估器验证。 该设计有意限制智能体可调用的工具范围，以考察在仅暴露 bash 的条件下模型完成 Lean 任务的表现。

AI 根据报道生成 · 1 小时前更新

还没有足够的连续观测数据，暂不绘制趋势。