第二章 当解题和证明能力进入工具
一、进入工具的不是同一种能力
人们谈论AI数学时，常把算出答案、写出推导、找到证明和确认正确混在一起。它们在实际工作中彼此联系，却承担不同任务。数值计算可以给出近似量，符号计算可以变换表达式，搜索程序可以发现候选对象，语言模型可以提出证明路线，证明检查器可以核对一个形式陈述的推导。任何一项取得进展，都可能影响研究，但不能由此推断其他环节已经同时完成。准确理解冲击，首先要拆开这些活动。
例如，要证明一类函数在给定区间非负，数值采样可以帮助研究者寻找负值，却不能仅凭大量正值确认普遍结论。符号系统给出因式分解后，仍须检查参数范围和除法条件。语言模型提出一个积分表示，可能打开证明，也可能把需要证明的性质暗藏在未经核验的等式中。形式化系统可以确认某个精确命题成立，却不会自动保证那个命题就是最初想表达的问题。研究链条中的每个成功，都有相应的边界。
封装使这些不同活动能够通过较简单的接口被调用。使用者不必每次重建全部算法与知识库，便可获得过去需要专门训练的部分能力。但封装没有消灭内部复杂性，而是重新分配了关注。用户从操作每个细节转向判断输入、解释输出和管理依赖。对数学家而言，这种转移尤其重要，因为一个细小的量词变化就可能改变命题。越方便的接口，越需要清楚说明它把哪些条件带入了结果。
二、两次竞赛结果说明了什么
Google DeepMind在二〇二四年的机构报告中介绍，AlphaProof与AlphaGeometry 2解出当年国际数学奥林匹克六题中的四题，得到二十八分，达到银牌分数水平。题目先经人工形式化，部分求解用时达到三天。二〇二五年该机构报告，高级版Gemini Deep Think用自然语言完成五题，得到三十五分，并获赛事协调方按比赛标准评分确认，报告称完成时间符合竞赛时限。两次结果不能被写成完全相同条件下的简单速度比较。（Google DeepMind，二〇二四；Luong与Lockhart，二〇二五。）
这组变化的重要性在于，工具能够承担的工作链条正在扩展。早期系统依赖人把题目转成特定语言，后来系统能够直接处理自然语言题面；专门形式系统与通用推理模型也展示了不同路径。然而，竞赛任务仍具有清楚题面、有限提交窗口和明确评分规则。研究数学还包括寻找问题、理解文献、选择对象、处理长期不确定性以及组织共同体。竞赛进展是研究能力变化的重要证据，却不是整个职业已经被替代的直接证据。
我们也不能从上述区别得出研究者因此安全。恰恰相反，输入转换、路线探索与证明表达曾经都被看作需要大量人类劳动的环节。当多个环节逐步被连接，职业所依赖的劳动组合就会变化。合理的反应既不是宣布终结，也不是不断寻找某种尚未被展示的能力作为永久防线，而是检视自己的研究链条，辨认工具已经能够可靠介入什么，介入以后又使什么活动成为可能。
三、证明搜索与证明核验
搜索与核验之间的差别，是理解数学封装的一把钥匙。寻找证明可能需要大量尝试，而检查一个给定证明可以沿着已经提供的路线进行。工具可以在候选生成上发挥很大作用，却仍需要独立的核验机制；也可以擅长检查而不擅长发现。把这两类能力连接起来，会产生比单独使用更强的研究系统，但连接本身包含设计问题：生成的命题与要证明的命题是否相同，转换是否保存假设，失败信息能否返回搜索过程。
Lean的官方说明明确区分证明被内核接受与形式陈述符合原意。一个通过检查的定理，依赖于其定义、既有定理和公理；对这些依赖以及陈述含义的检查仍然重要。由此，本书把形式化视为可靠性组织的重要方法，而不把它写成对任何输出无条件背书的装置。（Lean Language Reference，《Validating a Lean Proof》，检索于二〇二六年。）
这种区别可以通过一个简单例子理解。原问题要求证明所有正整数具有某性质，形式化时却误写为某个给定整数具有该性质；机器对后者的完美证明并未解决前者。错误不在推导链，而在问题接口。再如，为方便证明加入一个看似温和的前提，却使研究对象集合为空，结论便可能以失去实际内容的方式成立。因此，封装越深，研究者越要关注命题进入系统和结果返回研究活动的两个边界。
四、成本下降如何改变问题选择
数学家选择问题，通常不仅判断它是否重要，还判断自己能否承担探索成本。一个方向可能很有吸引力，却因为需要大量前置计算而被搁置；另一个方向未必更重要，但资料易得、技术成熟、成果期限可预期，于是更容易进入博士论文。工具改变成本，就可能改变这张问题地图。过去只能做少数例子的构造，可以被系统比较；过去需要跨越陌生领域才能验证的想法，可以先进行小规模试探。
不过，降低成本也可能使研究者更加集中地追逐热门题。若同一工具向大量人推荐相近问题，评价又只认可少数熟悉的成果形式，那么工具不仅不会自动扩展研究多样性，还可能加速路线趋同。人人都能生成更多候选引理，却都围绕同一类发表机会工作。所谓内卷，在这里体现为个体产出能力提高，却主要用于维持相对位置。问题不在能力增长本身，而在增长被引向怎样的活动集合。
因此，研究组织需要把一部分效率收益用于改变问题选择。例如，允许一个项目先比较三种对象定义，再决定哪个值得证明；允许研究者把否定结果整理为可复用的边界知识；允许团队为不容易立刻发表的新联系安排试验期。这些安排并不保证成功，却把封装释放的能力接入新活动。若节省的一切时间都被更高的同类产量要求收回，升级便失去了最基本的试探空间。
五、成果越多，理解为什么可能越难
证明生产的速度提高以后，数学共同体面临的不只是核验量增加。人们还需要知道不同结果之间的关系：哪个只是已有定理的改写，哪个给出新的统一，哪个揭示原先看不到的限制。一个数据库可以保存海量正确陈述，但数据库的规模并不等于研究者的理解规模。如果没有概念组织、问题谱系和适用条件，更多成果可能增加寻找关键联系的成本。
设想系统生成了一千个关于某类有限结构的正确命题。其价值不能仅由数量判定。有些命题可能通过一条简单的对偶变换相互导出，有些可能在同一个更一般的定理下被统一，另一些则需要不同的对象划分才能显示意义。此时，数学家的工作可以转向比较、压缩、组织与重新构造。但AI同样能够参与这些活动，不能把它们划成机器永远不可进入的领地。真正需要建设的是一个持续改进的复合研究过程。
理解也不仅表现为能用自然语言复述证明。更有力的观察是：研究者能否改变条件并预测后果，能否解释一个反例为何有效，能否把结果迁移到相近问题，又能否辨认迁移失败的原因。工具能够帮助完成这些动作，人的理解便应在互动中观察，而不是只通过一次脱离工具的记忆测试来判断。数学教育与职业评价若仍只测量旧操作，就可能看不见正在形成的新能力。
六、任务变化与职业变化之间
一种工具在某项任务上达到很高水平，不意味着整个职业只剩下这项任务。数学研究还需要提出可处理的问题，维护软件与资料，教学，交流，评审，合作和组织资源。反过来，一个职业包含许多任务，也不意味着它不会受到重大冲击。少数关键任务的成本变化，可能改变其他任务的价值和数量。例如，证明生成大量增加以后，阅读、分类与复核的需求可能扩大，同时以提供局部求解成果为主要依据的一些研究机会可能收缩。
职业是任务、责任、资源和身份的组合。学校是否愿意为某种新任务设置职位，基金是否认可一套公开研究基础设施，合作领域是否愿意持续支持模型维护，都会影响工具能力怎样转成职业机会。因此，本书不以“可自动化任务比例”直接计算数学家的剩余价值。这个比例即使能够测量，也不足以表示新任务如何出现、旧任务如何重组，以及收益由谁取得。
个人层面可以先做一种实际的工作记录：在一段研究中，哪些时间用于资料查找，哪些用于构造，哪些用于判断，哪些用于验证与表达。记录的目的不是把人的价值切成分钟，而是找到研究循环的真实瓶颈。若候选生成已经很快，继续追求生成速度可能毫无帮助；若主要困难在于缺乏可用定义，就应把工具用于比较定义及其后果。只有把能力增长放回完整活动，封装才可能转化为研究升级。
七、可靠封装需要能够重新展开
成熟工具之所以能够被放心调用，依赖反复使用、检测、修正和稳定的责任安排。数学工具也需要经历这一过程。一次令人惊叹的演示可以证明某种可能性，却不能独自建立日常研究中的可靠性。使用者需要逐渐知道：系统在哪类输入上稳定，哪些转换容易失败，哪些输出必须重新检查，版本变化是否影响已有结果。这些知识形成之后，才有理由把某些细节暂时交给工具。
封装与重新展开因而不是彼此排斥的原则。平时调用成熟步骤，使人获得更高层次的活动空间；当异常、边界任务或新的用途出现时，再把相关细节展开检查。这个过程类似研究者使用经典定理：无需每次重证，却要知道假设，并在推广时回到证明结构。区别在于，AI输出可能随输入和版本变化，因而记录与复现条件需要更加明确。可靠性的形成是一种持续活动，而非给工具贴上的永久标签。
当解题和证明能力进入工具，数学家获得的并非简单的额外劳动力，而是重新组织研究的机会和压力。已经封装的能力会改变哪些问题值得尝试、哪些贡献能够被看见，以及哪些训练需要调整。若这些变化只被用于提高旧轨道中的产量，竞争可能更加拥挤；若它们被用于展开不同对象与结构，数学活动则可能扩大。接下来，需要正面理解研究者为何会在这一过程中感到威胁，而不是把这种感受草率归结为保守。
这里还需要区分工具能力的公开展示与普通研究者的实际可用能力。一个系统在专门实验条件下成功，不意味着任何人都能以相同成本、权限和支持得到相同结果。算力、数据、接口、使用经验与验证资源都会影响可及性。讨论职业冲击时，应当同时问两件事：某种能力是否已经可能，以及这种能力是否正在成为广泛可调用的研究条件。前者改变对未来的判断，后者才直接改变大多数人的日常竞争。
两者之间的距离也可能构成新的权力关系。如果关键能力长期集中于少数平台，研究者虽然摆脱了一部分手工劳动，却增加了对平台的依赖。领域升级因此不能只谈模型性能，还要关心开放接口、成果可迁移和研究记录的可保留性。只有这些条件进入讨论，工具封装才不仅是技术展示，而成为可以共同建设的研究基础。