她是斯坦福00后数学才女，用AI撬动量化金融，零产品拿下3亿美金估值

　　00后中国女孩0产品创业实现3亿估值：斯坦福数学博士的AI量化野心

　　正在筹集5000万美元融资，目标估值3-5亿美元

　　方向瞄准数学AI，要为量化和对冲基金公司提供可解决实际数学问题的模型能力。

　　文章转载自：留学生研究社

　　作者：梁晓轩

　　“她是00后，没产品、没用户，却创造了3亿美元的估值——这听起来像童话，但它真的在发生。”

　　来自广州的洪乐潼（Carina Letong Hong），一位刚拿到斯坦福数学博士学位的年轻学者，近日低调成立了自己的AI创业公司Axiom（公理），并且很快吸引了市场的目光。据The Information报道，Axiom正在紧张地筹集5000万美元的首轮融资，估值预计高达3-5亿美元——而此时，此项目尚未推出任何实质性产品，甚至连第一位付费用户都还没有。

　　为什么一个“0产品0用户”的项目，能在如此早期就获得如此高的资本认可？

　　要回答这个问题，我们首先得了解洪乐潼的“学霸标签”到底有多亮眼。

　　一路“开挂”的广州学霸

　　洪乐潼从小在广州长大，父母并无高等教育背景，却从小发现女儿对数学有着异乎寻常的兴趣。年少时，她参加了当地的奥林匹克数学项目，遇到“超级有趣”的竞赛题后，一发不可收拾。高中期间，她在全国中学生数学奥林匹克（CMO）省选拔中脱颖而出，成为仅剩的四位女生之一，并开始将视野投向更高层次的数学研究。

　　2018年，年仅17岁的洪乐潼成功被麻省理工学院（MIT）录取，选择了数学与物理双专业。她在MIT只用3年时间就完成了两个学位，并在本科阶段发表了9篇学术论文，涉及模椭圆曲线与K3曲面上的L函数、“月光猜想”、theta函数与分区同余方程、堆栈排序算法、二部图染色的马尔可夫链等多领域课题。其中，不少成果是与当时就已刊登在数学四大顶刊的张盛桐合作完成的：这对“数学双剑客”在本科时代就跻身国际一流期刊，令人惊叹。

　　更令人侧目的是，她在MIT期间曾获得全美女性数学家最高荣誉——Alice T. Schafer数学奖（Schaefer Math Prize），并在2021年成为中国仅有的四位罗德学者之一，前往牛津大学继续攻读神经科学课程。她本人曾这样描述自己的跨学科视野：“数学虽是一门纯粹学科，但我也渴望理解生物医学，所以去牛津学神经科学，正是为了拓宽研究视野。”

　　而后，洪乐潼又横扫了哈佛、普林斯顿、斯坦福、麻省理工等顶尖项目，最终在斯坦福大学确定了数论、组合学和概率学方向的博士攻读计划，同时辅修法律学课程。斯坦福期间，她不仅在数论方面继续深耕，也开始关注人工智能与数学之间的交叉研究——在Sainsbury Wellcome中心的盖茨比部门（Gatsby Network）参与AI与机器学习研究，并思考“AI未来将如何与科学家互动”“应用科学家又如何借助AI完成更高层次的创新”等前沿问题。

　　正是在这一期间，她逐渐发现，当下主流的大语言模型（LLM）在数学推理层面仍明显不足：虽然能背诵定理、解答竞赛题，但一旦要求完整的“形式化证明”，准确率就骤降。她在社交媒体上直言：“模式匹配≠真正理解。我们需要的是会‘做证明’的AI，而不仅仅是会‘给答案’的模型。”

　　Axiom：打造“会证明”的数学AI

　　在清晰地意识到这一痛点后，洪乐潼于近期正式成立了Axiom——一家专注于“用AI解决高端数学问题”的初创公司。目前，Axiom的核心目标准确定位为：开发能够像数学家一样构建并验证形式化证明的AI系统，为量化对冲基金和金融机构提供极速、严谨的数学推理能力。

　　1. 技术切入点：形式化数学证明训练

　　Axiom的训练数据主要来源于已经被公认的“形式化数学证明”（formal mathematical proofs）。

　　形式化数学证明是指将数学定理、推导过程用高度严格的逻辑和编程语言描述，任何一步都可被机器验证。相比普通的“论文文本+Latex公式”数据，形式化证明具有可执行性和可验证性——适合给AI“灌输”真正的数学思维模式。

　　通过对这些证明数据的深度学习，Axiom希望让AI能够像人类数学家一样，不只是“找答案”，而是“推导答案”。

　　2. 商业模式：卖“数学大脑”给华尔街

　　Axiom并不打算推出一个面向大众的App，也不会去做ChatGPT式的通用AI对话。它锁定的目标客户是对冲基金、量化交易公司以及其他需要“高级数学证明能力”来加速投资决策的金融机构。

　　传统量化团队往往需要投入大量人力、时间和成本来搭建数学研究与工程化的管道：有人负责模型搭建，有人负责数学推导，有人负责算法实现，而这一切需要一个庞大的技术团队。Axiom的理念是：“你只要购买我们的AI能力，就相当于拥有了一个全天候的数学专家团队。”

　　在投资时，一旦遇到诸如风险度量模型（如VaR、CVaR）中的一个数学假设能否证明，或者在高频交易中某个定价公式的严谨性是否成立，这些场景都可交给Axiom的系统即时“给出证明+最优解”。

　　3. “0产品0用户”却能拿下高估值

　　据The Information报道，B Capital（曾投资过Perplexity等知名AI项目）正与Axiom洽谈本轮5000万美元融资，预计领投，Axiom估值达3-5亿美元。

　　这并非偶然。在过去一年里，行业里诸如Ilya Sutskever、Mira Murati等大佬牵头的“0产品0用户”项目频频拿到高额融资，投资者对专业垂直赛道非常“买账”。

　　对大多数VC而言，只要创始人的学术背景够硬，技术路径够清晰，就愿意押宝。对于Axiom而言，创始人洪乐潼在数学和AI领域的双重积淀，正是这样的“硬核背书”。

　　数学AI赛道：竞争与机遇并存

　　事实上，Axiom并非唯一瞄准“数学推理AI”赛道的玩家。要了解这条赛道的潜力与风险，我们不妨先看看几位主要对手与行业动态：

　　1. Harmonic：Robinhood CEO押注的AI初创

　　2023年，Robinhood CEO Vlad Tenev创立的AI公司Harmonic，目标同样是开发“能解高级数学问题”的AI系统。2024年秋季，该项目从红杉资本等知名机构融资7500万美元，估值高达3.25亿美元。

　　Harmonic的侧重点在于将AI嵌入金融工程模型中，尤其是衍生品定价与风险管理。但其技术路线更偏向“深度学习+金融数据”，与Axiom倚重形式化数学证明的思路并不完全相同。

　　2. 大厂“数学AI”实力：OpenAI、Google等纷纷布局

　　Google的DeepMind团队在国际数学奥林匹克（IMO）计算机辅导赛中曾拿到银牌，而在某些几何题目上甚至达到金牌水平；但他们在组合数学方面表现相对薄弱。

　　OpenAI的o4-mini模型在最近的FrontierMath评测中，已经超过了部分人类数学家团队的成绩；但在“正式证明”环节，准确率依旧偏低。种种迹象表明，通用大型模型虽然进步神速，却难以绕过“形式化推理”的关。

　　在这样的背景下，专注“形式化证明”的Axiom，看似弥补了大厂矩阵的一个空白。它不与ChatGPT等通用AI硬碰硬，而是选择与对冲基金赛道紧密绑定，用“可验证的数学逻辑”直击金融行业痛点。

　　洪乐潼的“AI量化”野心

　　在多次采访中，洪乐潼都强调：

　　“我们对当前大语言模型并不否定，但它们在‘数学证明’方面存在天然短板。Axiom要做的是，将编程语言和形式化数学紧密结合，让AI真正理解数学的本质，并能给出严谨的推理过程，而不仅仅是猜测或模式匹配。”

　　她曾举例，在美国数学邀请赛（AIME）测试中，最顶尖的LLM能拿下96%的选择题准确率，但一旦需要完整的“证明过程”，得分就缩水到5%。“这说明什么？说明我们训练它们的方式，还停留在‘海量文本+模式识别’阶段，缺少对‘形式化推导’的深度灌输。”洪乐潼说。

　　Axiom的长期愿景是：让AI成为“会思考、会证明、会创新”的工程师+数学家。

　　在金融领域，这意味着可以把复杂的衍生品定价、随机微分方程、风险度量等高端数学环节，通过Axiom“秒级”解决，而不是依赖传统的人工算法团队。

　　在学术研究层面，Axiom也计划将模型开源一部分，让更多数学家与工程师共同完善证明库，让AI更加贴近“人类数学家思维”。

　　洪乐潼坦言，目前团队规模尚小，核心成员主要由在斯坦福与麻省理工等顶尖实验室相识的数学与机器学习专家组成。她认为，保持“精英小团队”的研发效率和学术氛围，是Axiom在早期能迅速推动项目进展的关键。

　　行业前景与挑战

　　毋庸置疑，“数学AI+量化金融”是一个极具诱惑力的前沿赛道，但也面临诸多挑战：

　　数据稀缺与标准化难题

　　形式化数学证明毕竟仍是小众领域，目前公开可用的Formal Proof库较为有限，如何在保证质量的前提下“量产”训练数据，是摆在Axiom面前的第一道坎。

　　数学圈中常用的Coq、Lean、Isabelle等proof assistant工具各自有不同的语法与库，如何统一、打标签、清洗并迁移，均需耗费大量人力与时间。

　　模型泛化与性能考验

　　即使在训练集上能“做对”一部分形式化证明，也不代表模型能瞬间应对金融现场的“黑天鹅”式新命题。Axiom需要在算法层面不断优化，让模型具备一定的“零样本推理”能力，否则一旦遇到新系统公理、新金融概念，仍可能陷入“答不上来”的尴尬。

　　团队扩张与人才抢夺

　　顶尖的数学家和AI专家向来供不应求。Axiom要在硅谷与波士顿两大数学与AI人才聚集地抢人，竞争压力不小。相比“大厂”拿钱砸人，Axiom要怎样在早期维持高水平小团队，又留住核心成员，是摆在洪乐潼面前的又一道难题。

　　然而，正因为挑战存在，才更凸显机遇的可贵：

　　金融行业每年在量化研究上的投入规模以10%以上的速度增长，寻求一套能“秒级输出数学证明”的系统，若真能落地，势必撬动整个对冲基金服务链。

　　大型科技公司若想切入“量化数学AI”，也未必能轻易超越Axiom。毕竟形式化证明的“入门门槛”极高，需要创始人本人具备深厚的数学功底和对形式系统的深入理解，而洪乐潼在数论、组合数学领域的研究积累，正好贴合这一需求。

　　结语：高估值背后的“信仰”

　　在资本寒冬的当下，“0产品0用户”依然能拿到3-5亿美元的估值，看似“割韭菜”，实则是对创始人学术底蕴与技术远见的深度认可。洪乐潼用“数论+AI”这条小众且高门槛的赛道，告诉了我们一个道理：当下VC更愿意押注“硬核人才+垂直市场”组合，而不仅仅是“光喊口号、拼流量”的项目。

　　未来，Axiom能否真正将“形式化数学证明AI”推向市场、落地于华尔街？能否在Harmonic、OpenAI等大玩家的夹击下走出一条差异化路线？这些问题都还有待时间检验。

　　但有一点可以确定：洪乐潼这位00后数学才女，无论是从个人经历，还是从Axiom的技术路径来看，都已经为自己赢得了“垂直赛道创业新范本”的光环——她让我们看到了一条“数学+AI”赛道上的可能：即使暂时看不到产品和用户，只要技术够深、方向够明，就能让投资人产生真正的信心。

　　“我们所做的，不是让AI像人类背诵定理，而是让AI像人类证明定理。”——洪乐潼

　　放眼未来，当Axiom的AI能够真正流畅地完成一篇“形式化数学证明”时，也许就是真正打开金融技术新时代的大门。