在硅谷和华尔街风起云涌的AI创业热潮中，洪乐潼（Carina Letong Hong）是一位格外引人注目的年轻女性创业者。00后出生的她已经获取了斯坦福数学 博士，而她创立的Axiom公司目前尚无成品，也未正式拥有客户，却已获得数亿美元的估值，成为AI+数学创业领域的一匹"黑马"。这种惊人的市场认 可，背后是她一条极具传奇色彩的学术与创业之路。 从奥数小将到MIT双学位 洪乐潼出生于中国广州，父母虽未接受高等教育，却悉心培养她对知识的渴望。她的数学天赋早在青少年时期便崭露头角，加入免费的奥林匹克数学项 目，面对来自全球数学家的难题，她曾说："我在知识的世界里环球旅行。"高中时期，她是数学奥林匹克省队的唯一四名女生之一，站在竞赛顶尖的门槛 上。 怀揣对数学的热爱与渴望，洪乐潼14、15岁时便开始在笔记本边缘写下"MIT"，自我激励。三年内，她完成了麻省理工学院（MIT）数学与物理双学士学 位，期间发表9篇学术论文，涵盖数论、组合学、代数几何等纯数学前沿领域，这在本科生中极为罕见。她曾多次获得包括美国数学协会颁发的Alice T. Schafer奖和Frank & Brennie Morgan本科生研究奖等重量级 ...

明敏 鹭羽 发自 凹非寺 量子位 | 公众号 QbitAI 斯坦福华人数学博士AI创业， 0产品0用户 ，目标估值3亿美元。 0产品实现3-5亿估值 方向瞄准 数学AI ，要为量化和对冲基金公司提供可解决实际数学问题的模型能力。 （嗯，打造了DeepSeek的幻方量化，也是用AI来做投资量化） △ 来自个人主页 来自中国广州的 洪乐潼 （Carina Letong Hong）近期开启创业，立马一鸣惊人。 据The Information消息，她正在筹集目标为 5000万美元 的融资，公司估值预计 3-5亿美元 ——尽管目前公司还没有开发出一款产品。 为啥能实现如此估值？ 来看创始人兼CEO洪乐潼身上的标签： 3年时间完成麻省理工数学和物理本科双修 ，然后拿下斯坦福数学博士录取offer研究方向为数论、组合学和概率学，同时也进修了法律学课 程。 本科期间的论文已经发表在《美国数学会会报》、《拉马努金期刊》等刊物。2021年获得牛津大学罗德奖学金，成为仅有的4名中国获奖者之 一…… 如今，她开启创业，希望利用编程语言来训练模型，使其能掌握形式化证明的"语言"。 洪乐潼创立的公司名叫Axiom （公理） ，它的核心 ...

DeepSeek-Prover-V2发布 - 公司发布DeepSeek-Prover-V2模型，包含7B和671B两个参数版本，专注于形式化定理证明，专为数学AI编程语言Lean 4打造 [3] - DeepSeek-Prover-V2-671B基于DeepSeek-V3-Base训练，7B版本基于DeepSeek-Prover-V1.5-Base构建，支持32K tokens上下文长度 [3] - 模型在MiniF2F测试中达到88.9%通过率，解决PutnamBench数据集中658道题中的49道，性能达到业内最佳 [15] 技术实现 - 采用递归定理证明流程，使用DeepSeek-V3分解复杂问题为子目标并生成形式化推理步骤，融合非形式化与形式化数学推理 [9][4] - 通过7B模型完成子目标证明以降低计算开销，整合子目标证明与DeepSeek-V3生成的思维链构建冷启动数据 [11] - 采用两阶段训练：非思维链（non-CoT）模式优化快速生成Lean代码，思维链（CoT）模式强调透明推理步骤 [17] 性能与基准测试 - DeepSeek-Prover-V2-671B在ProofNet-test上通过率37.1%（1024样本），PutnamBench解决49/658题，显著优于Goedel-Prover-SFT和STP等竞品 [23] - 7B版本在ProofNet-test通过率29.6%（1024样本），PutnamBench解决11/658题，展示小模型的高效性能 [23] - 发布ProverBench基准数据集，包含325道题目，涵盖AIME竞赛题及本科数学内容，支持高中至本科难度评估 [25][26] 行业影响 - 模型开源并公开技术细节，HuggingFace平台提供7B和671B版本下载链接，推动数学AI领域发展 [6][16] - 用户实测显示模型效果优于o4-mini和Grok-3，尤其在数学奥林匹克问题解决中表现突出 [31] - 子目标分解与推理融合的设计被类比为初级工程师问题解决技巧，潜在适用于代码生成等场景 [32]