从广州到硅谷：洪乐潼押注16亿美元，筑起AI逻辑校验防线

2026年4月，硅谷。

在人工智能浪潮高涨之际，代码生成能力正以惊人的速度攀升。但与此同时，潜在风险也在同步放大：这些愈发强大的系统，正越来越像一个“擅长编造”的幻觉制造者。它们能够在极短时间内写出成千上万行代码，却无法确保系统在真正运行到关键节点时，不会因逻辑缺陷而失效。

在这片“概率式繁荣”的迷障里，25岁的广州女孩洪乐潼（Carina Hong）选择了反向而行。她的目标并不是让AI更聪明，而是让它更可信。

洪乐潼的经历堪称天才模板，但更令人注意的，是她身上展现出的韧劲。

2001年出生于广州天河的她，17岁便拿到了麻省理工学院（MIT）数学与物理双学位。20岁时，她获得北美本科数学领域最高荣誉——摩根奖（Morgan Prize），并成为该奖项历史上首位获奖的华裔女性。在学界看来，她原本完全可以沿着数论或理论计算机科学的道路稳步前行，但她显然并不满足于探索“已知”。

“奥数带来的是即时刺激，而研究数学更像是不停碰壁的过程，”她在采访中说，“可我恰恰喜欢这种不断碰壁的体验。”

2024年，正在斯坦福大学攻读数学与法学双博士的洪乐潼，在一次晨跑途中决定退学。受到苏姿丰（Lisa Su）“人才密度”观点的启发，她意识到，与其留在象牙塔里继续证明古典定理，不如转身去解决这个时代最紧迫的硬核问题：AI的逻辑幻觉。

当下主流大模型，本质上仍是建立在概率机制上的预测引擎。它们依靠预测下一个字符来生成内容，这种方式在文学创作中表现出色，但在航空航天、量化金融等连万分之一误差都无法容忍的领域，这样的“概率”无异于埋下隐患。

Axiom Math 的核心产品AXLE（Axiom Lean Engine）正试图把数学家的严密性带入代码世界。

洪乐潼选择了Lean——一种用于定理证明的编程语言。AXLE 的思路不是让AI“认为”答案正确，而是要求AI给出完整的证明步骤，并交由机器进行100%的自动核验。这项被称作“形式化验证”（Formal Methods）的技术本身并不新鲜，但将其与最前沿的大模型深度结合，洪乐潼走在了前面。

在2025年的Putnam数学竞赛中，AxiomProver 顺利证明了全部12道难题。其逻辑链条之完整，甚至让资深人类专家也感到自愧不如。“数学就是AGI（通用人工智能）的语法，”洪乐潼表示。在她看来，唯有当AI具备自我证明能力，科学发现的加速器才算真正启动。

Axiom Math 的迅速崛起，不仅因为技术路线特殊，也源于其惊人的人才吸附力。

公司目前员工只有约20人，但团队配置足以让大型科技公司侧目。CTO Shubho Sengupta 曾是 Meta FAIR 的核心负责人；更让学界震动的是，57岁的数学名宿、美国数学学会前副主席Ken Ono（小野健）宣布放弃大学终身教职，前往硅谷加入这位25岁创始人的事业。

“这是我职业生涯里最令人兴奋的时刻，”小野健说。在他看来，洪乐潼正在推动的，是让数学从纸面推理变成驱动未来文明的底层程序。在面试中，洪乐潼常会抛出一个极具理想主义意味的问题：“你愿不愿意把这个问题当作你一生留下的事业？”

虽然16亿美元估值体现了资本市场的热情，但领投方 Menlo Ventures 的判断显然更为克制：“未来全球的代码都将由AI书写，而数学将负责证明它们的正确性。Axiom 正是那个独一无二的证明者。”

如今，Axiom 的技术已经开始进入顶级对冲基金的自动化交易系统以及高阶密码学领域。在每秒牵动数亿美元交易的竞争中，代码的“逻辑确定性”就是最可靠的屏障。

在2026年的硅谷，洪乐潼的故事被看作是一场权力迁移：最顶尖的人才，正从资源过剩的大型科技企业，流向那些真正攻克底层难题的实验室。

当多数人仍在讨论AI会不会取代工作岗位时，这位来自广州的女孩已经开始思考，如何让机器在推演高维空间猜想时，彻底告别“说谎”。科学发现的进程正被重新改写，而洪乐潼正握着那支修补逻辑的笔。

（完）