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。