25岁创始人的AI公司完成「246定理」Lean4形式化验证
新智元 · wechat · 2026-08-22
8月17日，由 25 岁广州女孩洪乐潼创立的 AxiomMath 宣布，其系统 AxiomProver 完成了素数间距「246 定理」的形式化验证：证明成立、逻辑无误。246 定理是当前最接近孪生素数猜想的结果——从张益唐 2013 年的 7000 万差距，经 Maynard（600，获菲尔兹奖）和 Polymath8b（陶哲轩参与，246）逐步压缩，十余年无人再推进。
验证方式：AxiomProver 不证明新定理，而是把人类证明翻译为机器可检查的形式。它是一个多智能体系统：Auto-formalizer 补全跳步生成 Lean4 代码，Conjecturer 生成缺失引理，核心引擎搜索证明路径，Auto-informalizer 再把机器证明译回人话供审核。整个验证 14 章 132 页，核心是基于 GPY 方法与 Maynard 多维筛的 50 维优化问题（k=50、ε=1/25），关键变分常数 M₅₀,₁/₂₅≈4.0043>4，最终只依赖 Bombieri-Vinogradov 定理和素数定理两个外部结果。仓库已在 GitHub 开源，可本地运行验证。
公司背景：洪乐潼 MIT 数学物理双学位 3 年修完，获本科生最高荣誉 Morgan Prize，2025 年 3 月从斯坦福退学创业，把 MIT 导师、数论教授 Ken Ono 招为创始数学家。公司种子轮 6400 万美元，A 轮 2 亿美元，估值 16 亿美元；成绩单包括 Putnam 满分、IMO 42/42。Ono 强调，形式化验证的价值不止数学：AI 大量生成无人审查的代码，而数论是密码学基石，验证 AI 代码正确性的技术与验证数学证明同源——验证比创造容易，但价值同样巨大。
「公司和人」频道最新
- Zoom 悄然转型：从会议软件到创作者经济基础设施 — charitychaste · 2026-08-22
- 13 名学生因占领 OpenAI 华盛顿游说办公室被捕 — ImaginaryRea1ity · 2026-08-22
- 黄仁勋：英伟达是"只有在美国"的故事，可预期的规则是根基 — r0ck3t23 · 2026-08-22
- uv 作者入职 OpenAI，Codex CLI 启动速度暴增 25 倍 — teortaxesTex · 2026-08-22
- a16z 对话 Martin Casado：AI 时代的价值究竟流向了哪里？ — a16z Podcast · 2026-08-22
- 五角大楼将Palantir的Maven系统转为持久项目，锁定AI为美军核心 — emmanuelvivier · 2026-08-22