文章核心观点 - 数学研究正经历一场由AI和形式化证明语言（如Lean）引领的“工业革命”，传统“手工业”模式濒临崩溃 [1] - 形式化工具与AI的结合将数学证明拆分为可独立验证的原子步骤，从根本上改变了数学的协作、思维和生产方式，有望显著加速数学研究进展 [2][9][22][28] 数学研究的现状与加速 - 传统数学研究包含大量枯燥的重复性劳动，如文献综述、调整他人论文参数和繁琐计算 [6][7] - 形式化项目效率大幅提升：Peter Scholze的“液态张量实验”项目将一个重要定理形式化耗时18个月，而20世纪的类似项目动辄需几十年 [7] - 大语言模型（LLM）现已能自动形式化单个证明步骤，实时减轻形式化过程中的苦力活 [9] 形式化对数学思维的影响 - 形式化迫使数学家更清晰地思考，暴露“隐形假设”和习惯性默认成立的条件，从而精简写作 [11] - 形式化催生了新的证明写作风格：从传统的线性推导，转变为提供一组相关事实，由自动化工具找出正确组合来完成证明 [12] - 形式化帮助清理低效或错误的思维习惯，例如通过自动化工具发现定理中未被使用的冗余假设，从而可能扩展工具的自然适用范围 [14][15] 形式化改变协作方式 - 形式化具备高度模块化结构，允许围绕非常具体的局部问题进行原子级的精细讨论和修复，无需理解整个系统 [21] - 在形式化项目中，修改已有证明比传统方式高效得多：例如，将PFR猜想证明中的常数从12更新为11，在一天内完成，而首次完整形式化耗时三周 [19] - 形式化工具与AI实现了不同技能背景人群之间的无缝协作，数学研究首次具备了真正分工协作的可能性 [27][28] 数学研究的“工业化”与角色演变 - 未来的数学研究将出现类似软件工程的分工模式，进行规模化、工业化的数学成果生产 [2][28] - 数学家的角色将被拓宽：一部分人将成为大型项目的“架构师”或项目经理，负责协调；另一部分人可能专精于形式化工作或使用AI工具，而非特定数学领域专家 [24][29] - 新的协作方式将降低研究门槛，允许“公民数学家”（非专业领域专家但具备特定技能的人）参与前沿研究，释放庞大潜在研究力量 [2][30][31] AI在数学研究中的定位与应用前景 - AI和自动化的优势在于处理人类不擅长或不愿做的枯燥、机械性任务，如大量数值计算、枚举和组合筛选 [34] - 在解析数论等领域，大量研究时间（例如超过70%）花费在繁琐、机械性的工作上，这构成了主要瓶颈 [35] - 自动化工具链有望将解析数论中非显式的常数计算结果变为显式并可自动更新，从而动态维护领域前沿状态，将原本需十年一次的更新工作缩短至几分钟 [36][37][38] - 形式化验证系统（如Lean）有望构建一个尽可能无错误、可互操作、可规模化扩展的可靠数学研究基础设施 [39] 新工具对研究路径的潜在影响 - 历史上，计算机的引入已催生结合数据和实验的新数学研究方式（如高斯通过手工计算素数提出分布猜想） [42][43][45] - 当前数学论文中“苦工”比例看似不高，是因为研究者下意识地避开了计算繁重的路径；若工具到位，研究者将能直接“碾过”这些障碍，实际可被自动化的潜在工作量远高于表面所见 [46][47] - 形式化工具通过提供基于可验证结构的信任，将极大消除因人际信任与沟通成本造成的研究瓶颈，释放生产力 [47][48][49]

公司核心事件 - 世界级顶尖数学家小野肯（Ken Ono）辞去终身教职，全职加入AI初创公司Axiom，担任创始数学家[2][5][6] - 小野肯的加入标志着其从对AI持怀疑态度到积极投身AI数学领域的重大转变[12][17][18] - Axiom公司由小野肯的24岁学生、斯坦福数学博士辍学的华人女生洪乐潼（Carina Letong Hong）创办[2][7] 公司业务与目标 - 公司核心目标是为量化对冲基金公司开发能够解决实际数学问题的AI[24] - 具体方法是让AI学习严格的逻辑推理和数学证明过程，构建和验证形式化证明，保证结果的准确性和严谨性[24] - 产品旨在帮助对冲基金和量化交易公司快速解决投资、股市等金融领域的复杂数学问题[25] 公司技术成就与实力 - 公司近期在数学界表现亮眼，解决了Erdős问题 124和 481[26] - 对于124问题，AxiomProver模型将验证推进到了基础公理层面，超越了同行仅完成简化版证明和Lean形式化验证的工作[28][29] - 对于481问题，公司确实完成了解决工作，并借助Lean形式化完成了所有的类型检查，而此前OpenAI的GPT-5仅被指出是检索现有文献[31][32] - 公司团队规模小但精英云集，除小野肯外，还包括前Meta研究员François Charton等顶尖AI和数学专家[34] - François Charton的研究（如让Transformer模型解微分方程）被视为让神经网络理解数学结构的先驱成果[34] 公司融资与估值 - 公司在仅有0产品0用户的情况下，于首轮融资实现了3亿美元估值[7][36] - 公司的投资人中包括B Capital等顶级风险投资机构[36] 创始人背景 - 创始人洪乐潼是公认的数学少年天才，用3年时间完成麻省理工学院数学和物理本科双学位[7][42] - 本科期间发表了9篇涉及多个数学领域的论文，刊登在《美国数学会会报》、《拉马努金期刊》等顶级期刊上[42][43] - 曾获得2022年度中国罗德学者荣誉，是仅有的4名中国获奖者之一[7][45] - 在麻省理工学院期间师从小野肯，解决了拉马努金理论中的部分猜想，并获得了拉马努金精神奖学金[44][45] - 2024年获得斯坦福数学博士录取offer，但选择辍学创业[46][48] - 最近被评为2026年福布斯30位30岁以下的AI精英[49] 行业意义与展望 - 小野肯与洪乐潼的师生合作，被类比为数学史上的黄金师徒哈代和拉马努金，旨在携手逼近数学界的“GPT时刻”[52] - 公司致力于寻找数学公理，破解困扰人类数个世纪的难题[49]

核心观点 - 谷歌DeepMind研发的AI系统AlphaProof在国际数学奥林匹克竞赛（IMO）中取得28分（满分42分），达到银牌水平，距离金牌线仅差1分，这是AI首次在此类顶级数学赛事中获得奖牌级成绩 [3][4][18] 技术方法 - AlphaProof结合了预训练大语言模型的直觉和AlphaZero强化学习算法的探索能力，其核心是将AI思维“硬化”成可被计算机逐行检验的形式化证明语言Lean [8][6][7] - 系统首先利用谷歌Gemini模型将近一百万道自然语言数学题翻译成Lean代码，构建了约8000万条形式化数学命题的题库供AI练习 [10] - 训练过程分为两步：先通过监督学习微调掌握基本证明技巧，再进入强化学习阶段，通过类似AlphaGo的自我对弈在数百万次问题证明中不断进步 [10] - 在解题搜索中采用类似蒙特卡罗树搜索的策略，智能拆解复杂问题为子目标，避免了暴力穷举 [11][16][17] 竞赛表现 - AlphaProof与专攻几何的AlphaGeometry 2联手，在2024年IMO的6道题中解出4道，获得28分，处于银牌段顶端 [18] - AlphaProof单独解决了3题（包括2道代数题和1道数论题），其中整场最难的第6题在600多名顶尖学生中仅5人满分解决 [18] - 剩余1道几何题由AlphaGeometry 2完成，而两道组合数学题因难以形式化和搜索爆炸等原因未能攻克 [18] 当前局限 - 解题效率较低：人类选手需在4.5小时内完成3题，而AlphaProof解决3题耗费了将近3天时间 [21] - 通用性不足：未能解决两道组合数学题，这类高度非结构化创新思维的问题仍对AI构成挑战 [21] - 无法自主读题：需要人工先将题目翻译成Lean形式化表达，不具备自然语言理解能力 [21] 未来方向 - 研发方向包括让AI直接阅读理解自然语言表述的数学题，并给出形式化证明 [23] - 针对不同类别数学问题（如组合数学或几何）引入更专业策略，如融合符号计算、知识库或分领域训练模型 [24] - 未来可能实现数学家与AI证明助手协同工作，AI负责快速验证猜想和尝试思路，人类专注于提出问题和宏观构想 [24] - 其形式化推理能力对AI安全和可靠性有启发意义，输出的每一步推理可追溯、验证，有助于减少大模型的荒诞臆测 [25]