当人工智能开始从“整理知识”走向“提出候选答案并接受验证”，科学研究的工作方式正在发生变化。近期，AI科学发现模型在数学推理和材料设计两个方向连续取得进展：一边尝试搜索严谨证明，另一边按照目标性能生成新的晶体结构。它们的共同价值，不是替代科学家，而是扩大可探索空间，把研究人员从大量重复筛选中释放出来。🤖🔬
数学研究：从语言回答走向可验证证明
数学对AI的要求尤其严格。一个答案看起来合理，并不代表证明成立；只要某个推理环节存在漏洞，最终结论就可能失效。因此，数学类科学发现模型正在从普通自然语言生成，转向“神经网络提出思路、形式化系统检查步骤”的技术路线。
AlphaProof便是具有代表性的探索。该系统结合强化学习与形式化证明环境，把数学问题转化为机器能够检查的表达，再通过搜索不断尝试证明路径。在2024年国际数学奥林匹克竞赛相关测试中，AlphaProof与AlphaGeometry 2共同解决了六道题中的四道，达到银牌水平。需要注意的是，当时部分题目仍需人工转换为形式化语言，复杂问题的计算也可能持续较长时间，因此它距离独立开展数学研究仍有明显差距。相关过程可参考官方介绍[1]。
几何推理同样体现了“生成与验证结合”的优势。AlphaGeometry利用语言模型寻找辅助点、辅助线等关键构造，再交由符号推理引擎执行严格演绎。其早期版本在30道奥赛级几何题中解决了25道，明显超过此前方法，并接近人类金牌选手的平均表现。论文同时指出，该系统依靠大规模合成定理和证明训练，缓解了高质量形式化数据不足的问题，详见Nature论文[2]。
真正的突破不只是“做对题”
竞赛成绩只是容易比较的测试指标，数学研究更关注模型能否处理开放问题、给出新猜想，并形成可被同行复核的证明。当前模型最值得期待的能力，是在庞大的推理树中快速排除无效方向，发现人类不容易优先想到的引理、构造或反例。
不过，“形式化验证通过”也不等于数学发现已经完成。模型可能给出非常冗长的证明，或者依赖不自然的中间步骤；形式化系统只能确认推导符合既定规则，不能自动判断结果是否重要、解释是否清晰。未来更实际的人机协作模式，可能是数学家提出问题与评价价值，AI负责搜索候选路径，证明助手检查逻辑，最终由研究者整理为可理解、可传播的数学成果。🧠
材料研究：从数据库筛选转向按需生成
传统计算材料研究通常采用“先建立候选库，再逐个筛选”的路径。当元素组合、晶体结构和外部条件共同变化时，搜索空间会迅速扩大。生成式材料模型则尝试反向解决问题：研究人员先给出稳定性、化学组成、磁性、电子性质或力学性能等约束，让模型直接生成符合目标的候选结构。
MatterGen就是这一思路的代表。它采用面向无机材料设计的扩散模型，可在元素周期表范围内生成稳定且多样的晶体结构，并通过微调把生成方向引向指定化学体系、对称性及材料性能。相关研究发表于Nature论文[3]，代码与模型说明也已通过开源项目[4]提供。
这类模型带来的变化，是把AI从“性质预测器”推进为“结构提案者”。过去，模型往往只能回答某种已知材料可能具有什么性质；现在，它还可以根据需求提出新的原子排列方案。配合原子级模拟模型、量子化学计算和实验验证，研究团队有望建立“生成候选—计算筛选—实验合成—反馈优化”的闭环。⚗️
材料模型仍要接受现实世界检验
计算上稳定的结构，不一定能够在实验室中顺利制备。温度、压力、杂质、反应路径和设备条件，都可能影响实际结果；有些候选材料虽然性能理想，却需要昂贵元素或苛刻工艺。因此，AI生成结果应被视为高价值候选，而不是已经完成验证的新材料。
研究机构在引入此类工具时，可以采用以下流程：
- 明确目标：把性能范围、元素限制、成本和环境要求写成可计算约束。
- 多层筛选：依次检查结构合理性、热力学稳定性、目标性质和可合成性。
- 保留失败记录：将无效候选及失败实验纳入数据体系，避免模型反复探索同类错误。
- 实施人工复核：由材料、计算和实验人员共同判断候选方案的科学价值。
- 建立可追溯记录：保存模型版本、输入条件、随机种子和计算参数，方便复现结果。
两个领域正在形成共同范式
数学证明和材料发现看似距离很远，背后却呈现出相似的AI科学发现流程：模型先在巨大空间中生成候选，再由严格工具进行验证，最后由专家判断意义。数学中的验证器是形式化证明系统，材料领域则包括物理模拟、量子计算和实验装置。
AI最重要的作用，不是绕过科学方法，而是让“提出假设—验证假设—修正方向”的循环运行得更快。
总结：突破之后，更需要严谨协作
AI科学发现模型正在证明，它不仅能够总结论文和辅助写作，还可以参与证明搜索、晶体生成和实验候选筛选。但现阶段的突破应被理解为研究工具能力的提升，而不是机器已经可以独立完成科学发现。只要坚持可验证、可复现和人类负责的原则，AI就有机会成为数学家与材料科学家的“搜索放大器”，帮助研究团队更快找到值得深入探索的新方向。🚀
