Numina-Lean-Agent 用通用 coding agent + MCP 直接充当 Lean 数学推理器，并在 Putnam 2025 上 12/12

Numina-Lean-Agent 提出一种更通用的 formal-math agent 范式：不依赖 task-specific proving pipeline 或专门训练的 formal prover，而是让 Claude Code 通过 Numina-Lean-MCP 自主调用 Lean、检索相关定理、生成 informal proof 与辅助推理工具。使用 Claude Opus 4.5 时，系统解决 Putnam 2025 全部 12 题；作者还与数学家合作完成 Brascamp–Lieb theorem 的形式化，并公开 agent 与全部解答。