正文：谷歌DeepMind团队在Nature上公开了其IMO金牌模型AlphaProof的技术细节。核心团队仅10人，开发历时一年，生成8000万道数学题用于AI训练。AlphaProof基于Lean定理证明器构建强化学习环境，将数学证明过程转化为游戏关卡，使用30亿参数的Transformer模型作为核心，并结合改进的树搜索算法。2024年IMO比赛中，AlphaProof成功解决三道难题（包括最难的P6），最终夺得金牌。系统通过测试时强化学习生成变体问题并进行针对性训练，展现了强大的解题能力。尽管依赖Lean定理证明器且在处理全新定义时存在局限性，但其反证功能和形式化能力受到数学家高度评价。谷歌已开放AlphaProof供科研使用。

斯坦福数学博士洪乐潼（Carina Letong Hong）以0产品0用户估值达3-5亿美元创业，目标为量化和对冲基金提供数学AI解决方案。这位来自中国广州的女孩，曾用3年完成MIT数学和物理双学位，并发表多篇顶级数学论文。她的公司Axiom致力于训练AI掌握形式化数学证明语言，帮助解决复杂金融数学问题。尽管尚未推出产品，Axiom已吸引B Capital等知名投资机构关注，计划融资5000万美元。洪乐潼的学术成就和跨学科背景被认为是其估值的关键因素。