About this episode
本期讨论了Numina-Lean-Agent，一个通用的数学形式化推理系统。
Seventy3：借助NotebookLM的能力进行论文解读，专注人工智能、大模型、机器人算法、crypto方向，让大家跟着AI一起进步。 如果你想要解读自己的论文，获得更多曝光度。请联系小助手微信：seventy3_podcast 加群。合作邮箱：zhiwudazhanjiangshi#gmail.com 今天的主题是： Numina-Lean-Agent: An Open and General Agentic Reasoning System for Formal Mathematics Summary 智能体系统（Agentic systems）近期已成为形式化定理证明的主流范式，通过协调多个模型和工具实现了强劲的性能。然而，现有方法往往依赖于针对特定任务的流水线和经过专门训练的形式化证明器，这限制了它们的灵活性和可复现性。 在本文中，我们提出了一种直接将通用代码智能体（General coding agent）作为形式化数学推理器的范式。该范式的出发点在于：(1) 通用代码智能体为证明之外的各种推理任务提供了天然的接口；(2) 无需训练，仅通过更换底层基座模型即可提升性能；(3) 模型上下文协议（MCP）能够灵活扩展并自主调用专用工具，从而避免了复杂的系统设计。 基于这一范式，我们推出了 Numina-Lean-Agent ，它将 Claude Code 与 Numina-Lean-MCP 相结合，实现了与 Lean 的自主交互、相关定理检索、非形式化证明以及辅助推理工具的调用。在使用 Claude 4.5 Opus 作为基座模型时，Numina-Lean-Agent 解决了 Putnam 2025 的所有题目（12/12），达到了顶尖闭源系统的水平。 除了基准测试评估外，我们还通过与数学家交互并成功形式化了 Brascamp-Lieb 定理，进一步展示了该系统的通用性。我们已在上述网址发布了 Numina-Lean-Agent 及其全部解题方案。 原文链接：https://arxiv.org/abs/2601.14027
People in this episode
Host: 任雨山
Topics covered
- 人工智能
- 形式化推理
- 数学
- 算法
- 机器人
- 大模型
Keywords
- Numina-Lean-Agent
- 形式化推理
- 智能体系统
- 数学推理
- Claude Code
- Lean
- 算法
Mentioned in this episode
Organizations: Numina-Lean-Agent, NotebookLM, Claude Code, Lean
Books & works: Brascamp-Lieb 定理, Putnam 2025, Numina-Lean-MCP, arxiv.org/abs/2601.14027
More episodes of Seventy3
- 【第621期】多智能体大语言模型系统的多样性坍缩 · June 12, 2026 · 22 min
- 【第620期】MASS-RAG：多智能体合成检索增强生成技术 · June 11, 2026 · 20 min
- 【第619期】Learning Mechanics：大模型学习力学 · June 10, 2026 · 21 min
- 【第618期】无状态决策记忆：企业级AI智能体架构 · June 9, 2026 · 28 min
- 【第617期】自动演化EDA工具：多智能体自进化ABC · June 8, 2026 · 23 min
- 【第616期】原生智能：通向自主演化智能体的元学习范式 · June 7, 2026 · 17 min
Explore listener stats, chart rankings, contacts and more on the Seventy3 podcast page.