文章核心观点 - 人工智能（AI），特别是自动形式化技术，在数学证明生成领域取得了突破性进展，能够以远超人类志愿者的速度（从数周缩短至数小时）完成形式化证明任务，显著加速了如IEANTN这类大型数学形式化项目的进程 [2][11][12][13] - 然而，AI生成证明存在“阻抗不匹配”或“阻抗失配”的核心矛盾：AI在证明生成环节被加速了数个量级，但证明的验证、消化与整合环节仍严重依赖人类，因为AI生成的证明冗长、臃肿（比人类写的长出数百行），包含大量冗余步骤，且缺乏对项目全局结构的理解，这给项目的整体构建和代码库整合带来了新的挑战 [4][15][18][20] - 数学家的角色因此正在发生转变，从亲自执行证明转向成为证明工程的架构师，其工作瓶颈从“等待人力完成”转变为“设计任务以使AI产出能被有效整合”，需要提前规划并预判AI的产出，以确保其与项目全局架构兼容 [26][28] 根据相关目录分别进行总结 AI在数学形式化证明中的能力与影响 - AI工具近期跨过临界点，能快速完成形式化任务，陶哲轩发布的几乎每一个任务都能在数小时内被AI完成，导致项目中待认领的未解决任务队列基本清空 [11][12][13] - AI的介入极大提升了项目推进速度，使原本需要志愿者花费数周才能完成的形式化工作被大幅压缩 [2][9] - AI擅长处理局部、原子化的任务，例如进行局部的“代码精简”（code golf），能够在一定程度上压缩证明体积 [21][22] AI生成证明的局限性及“阻抗失配”问题 - AI生成的形式化证明比人类写的冗长数百行，包含大量冗余步骤，许多引理没有在合适的抽象层次上陈述 [15] - 虽然单个臃肿证明问题不大，但每个都会给项目总构建时间增加几十秒，累积效应不可忽视 [16][17] - “阻抗失配”体现在证明生成、验证、消化三个环节的速度差距拉大：生成端被AI加速数个量级，但验证和消化端仍依赖人类有限的认知带宽 [18][20] - AI无法进行全局性重构决策，例如无法自发发现文档中多处重复的论证并将其抽象为具有广泛用途的独立引理，也缺乏对项目全局结构的理解 [23][24] 数学家角色的演变与新挑战 - 陶哲轩在思考解析数论问题时，至少有70%的时间用于处理涉及大量繁琐数值验证和参数匹配的此类工作，而AI改变了这一工作模式 [7][8] - 当前挑战在于将包含数千行AI生成代码的中等规模文档，转化为结构优雅、适合提交到数学库的版本 [20] - 数学家需要花费更多时间提前规划形式化任务的范围，预判AI的快速产出，并设计任务使结果更易于审查和整合到项目全局结构中 [26] - 数学家的角色正从证明执行者转向证明工程架构师，负责确保每一部分（拼图块）在正确的抽象层次并以正确的接口标准存在，而AI仅负责快速生产这些“拼图块”，其形状是否匹配整体蓝图仍需人类判断 [28]