主要证据
- Numina-Lean-Agent: An Open and General Agentic Reasoning System for Formal MathematicsS1 · 主要研究来源 · 论文 · 2026-01-20
- Numina-Lean-Agent implementation and proof resourcesS1 · 主要研究来源 · 代码仓库
Numina-Lean-Agent 将通用 Coding Agent 转化为开放的 Lean 数学推理系统
该系统以通用 Coding Agent 循环作为 Lean 工作的控制器，并通过面向 MCP 的接口接入定理检索、非形式证明、验证和辅助推理工具。公开仓库提供安装说明、可运行的 Agent 工具以及 Putnam 形式证明产物。
发生了什么？
论文报告称，基于 Claude Code 与 Numina-Lean-MCP 的 Numina-Lean-Agent 在 Claude Opus 4.5 上完成了 2025 Putnam 的全部 12 道题，并与数学家协作完成 Effective Brascamp–Lieb 定理的形式化；Agent 实现与形式证明结果均已公开。
为什么重要？
该工作把快速发展的 Coding Agent 生态直接连接到形式数学，并表明通用 Agent Harness 与基础模型的改进有可能直接迁移到定理证明，而无需为每类任务重新构建专用证明栈。
重要性说明：Numina-Lean-Agent 展示了一种不同的形式数学架构：通用 Coding Agent 可以直接操作 Lean，并通过 MCP 自主调用专用工具，而不必依赖任务专用的证明管线或新训练的形式证明模型。
历史脉络
证据与状态一览
- 重要性
- H2 · 领域里程碑
- 验证状态
- 论文已发布
- 证据等级
- E3 · 可检查工件
- AI 角色
- AI 自主主导
- 形式保障
- 机器检查
贡献与验证
- 数学新颖性
- 工具性进展
- 接口
- 形式化, 混合
- AI 贡献
- Coding Agent 自主检查 Lean 目标、编辑证明代码并调用专用推理与检索工具；Lean 编译器反馈对被接受的形式输出进行机械约束。
- 人类贡献
- 研究者设计 Agent 与 MCP 工具接口、配置评测任务、公开实现及证明产物，并在研究级形式化案例中提供数学家协作与语义监督。
- 验证状态
- 论文已发布 · E3 · 可检查工件 · 机器检查
- 最后审阅
- 2026-09-11
技术细节
- 系统
- numina-lean-agent, claude-code, numina-lean-mcp, lean
- 机构
- project-numina
- 数学问题
- putnam-2025, effective-brascamp-lieb-formalization
- 方法
- coding-agent, model-context-protocol, compiler-feedback, theorem-retrieval, lean
全部来源与工件
- Numina-Lean-Agent: An Open and General Agentic Reasoning System for Formal MathematicsS1 · 主要研究来源 · 论文 · 访问于 2026-09-11
- Numina-Lean-Agent implementation and proof resourcesS1 · 主要研究来源 · 代码仓库 · 访问于 2026-09-11
验证历史
- 2026-01-20 · 论文已发布 · E2 · 研究记录
arXiv 论文发布面向形式数学的通用 Coding Agent 范式，并报告 Putnam 2025 与 Brascamp–Lieb 案例结果。
- 2026-09-11 · 论文已发布 · E3 · 可检查工件
Numina-Lean-Agent 公开仓库提供可运行工具并链接生成的 Lean 证明产物。machine-checked 表示形式输出可由 Lean 接受，并不表示 Chronicle 独立复现了全部报告运行或裁决非形式表述与形式命题之间的语义对应。
更正
当前没有记录的更正。