文章核心观点 - 数学研究正经历一场由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]