This paper introduces mini-Lean-agent, a minimal AI agent for Lean tasks. It uses a generic coding agent with a minimal harness and achieves strong performance on Lean benchmarks. The results motivate using mini-Lean-agent as a standard baseline for evaluating theorem-proving infrastructure.