mini-Lean-Agent：面向 Lean 的编码智能体基线

mini-Lean-Agent 是一个仅向模型暴露 bash 工具的极简 Lean 智能体，用于厘清定理证明智能体的性能增益来源。在 Putnam 2025 基准上，以 Gemini 3.8 Flash 为基座时它解决 7/12 题（每题 $2 上限），AxProverBase 为 4/12；以 Astra 为基座时解决 12/12 题，平均每题 $1.28。