Project Numina
法国非营利组织，构建开放的 AI 数学能力——NuminaMath 数据集、Kimina-Prover 以及用于形式化定理证明的 Numina-Lean-Agent。
1. 核心产品 / 服务
Project Numina 是一个法国非营利组织，也是推进数学 AI 的开放科研协作，依据公益使命公开发布全部研究成果 [1]。其产出分为三层：
- 数据集——NuminaMath，最大的公开数学题与证明语料库（约 86 万条），另有 NuminaMath Lean 100k 和 CombiBench；路线图目标是形式化多达 100 万道题目/证明 [1]。
- 模型——NuminaMath 7B，于 2024 年 7 月赢得 AIMO 首届进步奖（Progress Prize #1）；以及与月之暗面 kimi 团队联合开发的 Kimina-Prover 系列 [1]。
- 智能体——Numina-Lean-Agent，一个面向形式化数学（Lean）的开放式智能体推理系统，解出了 2025 年普特南竞赛的全部 12 道题，并完成了 Brascamp–Lieb 定理的形式化 [1][3]。
Numina 的战略分岔可以概括为自训练证明模型 vs. 公共算力基础设施——这是一条开放、依靠资助的路线，而非封闭实验室或风险投资押注 [1]。
2. 目标用户与痛点
- 研究型数学家与形式化方法社区，需要开放、可复现的定理证明工具。
- 奥赛 / 竞赛数学教育者——NuminaMath 和 fellowship 计划都明确面向教育普及。
解决的痛点：形式化证明的生成与验证成本高昂；Numina 的开放数据集和模型降低了入门成本，避免把数学验证锁在专有 API 之后。
3. 竞争格局
| 玩家 | 类型 | 模型 | 备注 |
|---|---|---|---|
| Numina | 开放的非营利组织 | NuminaMath、Kimina-Prover | 开放数据集 + 智能体；AIMO 首届进步奖 |
| google-deepmind | 封闭实验室 | AlphaProof / AlphaGeometry | IMO 银牌水平（2024） |
| axiom | 风投支持的初创公司 | AxiomProver | 普特南 12/12，融资 2.64 亿美元 |
| Kimi（月之暗面） | 中国实验室 | Kimi-Prover | Numina 合作伙伴 |
| ByteDance Seed | 中国实验室 | Kakeya | Numina 合作伙伴 [1] |
Numina 的差异化在于开放性与非营利治理，对比的是 DeepMind 的封闭前沿以及 axiom 的商业化"Verified AI"路线。
4. 独立观察
- "Kimina"这个名字就是联盟的写照。 Kimina-Prover 是 Numina × 月之暗面（kimi）联合开发的证明器；合作时间线把 Numina 同时与 Kimi（Kimi-Prover）和字节跳动 Seed（Kakeya）联系在一起，这是一个少见的跨实验室、跨国界的开放数学联盟 [1]。
- 资助经济学，而非风投经济学。 Numina 的资金来自 XTX Markets 的 300 万欧元研究资助，而非风险投资轮次，因此在结构上免受推动 axiom 类初创公司的基准测试炒作激励的影响——这是对"谁来资助形式化数学 AI"的一个真正不同的回答 [1]。
- 形式化验证作为公共品。 通过开源数据集和智能体，Numina 押注数学验证是基础设施而非护城河——与封闭的"Verified AI"初创公司的论点正好相反 [1][3]。
5. 财务 / 融资
- XTX Markets 的 300 万欧元研究资助（2024 年 12 月 17 日宣布）——用于形式化 10 万以上条目并开源推理模型 [1]。
- AIMO 首届进步奖 131,072 美元（2024 年 7 月），凭借 NuminaMath 7B 获得 [1]。
- Numina Fellowship——为期 12–18 个月的研究合作，每个项目提供 5 万至 20 万美元的算力和工具 [2]。
- 无披露的风险投资轮次或估值（非营利组织）。
6. 团队与关系
- 联合创始人 / 总裁：Yann Fleureau。
- 联合创始人 / 首席科学家：Jia Li（奥赛教练；整理验证集和训练数据）。
- 创始合伙人：Alexandre Momeni（前斯坦福 ML 研究科学家，前 General Catalyst）[4]。
- 早期团队 / 顾问：Hélène Evain；据称 Guillaume Lample（Mistral 联合创始人）和 Stanislas Polu 曾协助创立。
- 合作伙伴：月之暗面（kimi，Kimina-Prover）、字节跳动 Seed（Kakeya）[1]；资助方 XTX Markets。
- 竞争对手：google-deepmind、axiom。
来源
[1] Internal research notes — Numina core product, self-training vs public-compute route, Kimi-Prover + ByteDance Seed (Kakeya) cooperation and timeline, team. [2] Project Numina, "Numina Fellowship," https://projectnumina.ai/fellowship (2026-10-05) [3] "Numina-Lean-Agent: An Open and General Agentic Reasoning System for Formal Mathematics," arXiv 2601.14027, https://arxiv.org/pdf/2601.14027v1 (2026-10-05) [4] Crunchbase, "Alexandre Momeni — Founding Partner @ Project Numina," https://www.crunchbase.com/person/alexandre-momeni-20c4 (2026-10-05)
Project Numina（NuminaMath / Kimina-Prover）
法国非营利的开放数学数据与证明器，资产是数据加验证层
- 数据类型
- 数学题与解答；形式化 Lean 证明；推理轨迹
- 规模口径
- NuminaMath-CoT 约 86 万条、NuminaMath-1.5 约 90 万题；NuminaMath-LEAN 约 10.4 万条（项目口径）
- License
- Apache-2.0（NuminaMath-CoT 与 NuminaMath-1.5 数据卡标注）
内容与规模
Project Numina 是法国的非营利开放协作项目，在 AIMO 进步奖中以 NuminaMath 7B 夺得第一届冠军（2024-07）。NuminaMath-CoT 发布于 2024-07，NuminaMath-1.5 于 2025-02，约 90 万道竞赛级数学题（CoT 版约 86 万条），Apache-2.0 [1][2]。另有 NuminaMath-LEAN（形式化数据）。
与 Moonshot 合作
Kimina-Prover 由 Numina 与 Moonshot（Kimi）团队合作，基于 Qwen2.5-72B 与大规模 RL；配套的 Kimina Lean Server 在 RL 中充当奖励验证层。
谁在用
NuminaMath-TIR 的 64,312 条进入 tulu-3 SFT 混合；面壁等中国团队的 RL 数据也引用 Numina 题集；Skywork-OR1 的 RL 数据源自 NuminaMath-1.5 等公开集 ⚠️ 为第三方综述口径。
口径提示
项目由 XTX Markets €300 万资助 [3]；它不训练面向终端的大模型，价值在数据与验证层，见 rlvr。