极简 Lean agent 走红：现代模型只用 bash 就能干重活
wellecks · x · 2026-10-21
tomasortega 开源的 mini-Lean-agent（一个极简的 Lean 定理证明 agent harness）正在受到关注。其核心观点：需要复杂搜索工具和大量脚手架的系统如今可能是过度设计，现代模型只给它一个 bash 访问权限就能表现很好。
- wellecks 转发并推荐了这个项目，认为 mini harness 的流行是个好趋势
- 这与「极简 agent harness」（如用 bash + REPL 替代重型编排框架）的思潮相呼应，对做定理证明/数学类 agent 的人有直接参考价值
所属事件:极简 Lean agent 仅用 bash 在 Putnam 获满分(2 条相关)→
「编程与Agent」频道最新
- 用 Claude 制定方案：实测廉价 SG90 舵机建模 MuJoCo 模型 — _Stocko_ · 2026-10-21
- 决策模型主诊+LLM 复核:SREGym 实验把故障诊断通过率提到 89.5% — tianyin_xu · 2026-10-21
- Autonomous 实测:Opus 规划+DeepSeek 执行的本地混合 agent 策略 — dee_hw · 2026-10-21
- Cloudflare「重造 GitHub」挑战赛决赛明日举行，冠军获 2.5 万美元额度 — dinasaur_404 · 2026-10-21
- 开发者打造共享修复库 yarrow:用沙箱验证与投票防 Agent 知识库变垃圾场 — Significant_Camp4148 · 2026-10-21
- mini-Lean-agent：纯 bash 最小 agent 在 Putnam 2025 拿 12/12，单题成本 1.28 美元 — wellecks · 2026-10-21