2025年10月22日，著名数学物理学家何杨辉教授在物理西楼思源多功能厅作题为“AI助力的理论发现”的学术报告。论坛由6163银河线路检测中心朱华星教授主持，吸引了校内外众多师生到场聆听，并同步开启线上直播。

朱华星教授主持

报告现场

         何杨辉教授围绕“自下而上”、“自上而下”与“元数学”三条主线系统梳理了AI重塑数学和理论物理发现的范式，并以多学科案例展示人机协作的可能路径与边界。教授提出‘伯奇测试’（AIN：自动化、可解释、非平凡）作为衡量AI提出新猜想的标准，并强调目前尚无成果完全通过该测试。 

一、从“自下而上”出发

报告回顾了从《数学原理》（Principia Mathematica）到哥德尔不完备性定理对形式化的深远影响。  何教授重点介绍Lean/Mathlib生态，讨论其在定理验证、知识组织与复用中的作用；结合Project Xena与面向物理数学问题的实践，展示形式化与知识复用如何为研究者提供辅助。同时也坦诚其边界：形式化成本与语义建模的难点仍需人机协同优化。

二、聚焦“自上而下”

该路线强调在整体结构、对称性与物理直觉的引导下开展数学物理创造。报告跳出单一形式系统，讨论以“柏拉图式数据”驱动的数学作为艺术和直觉的范式：通过汇聚大规模结构化数据，借助机器学习算法识别模式、辅助人类提出猜想并反馈至严格证明。  

何教授以高斯对素数定理的实验性研究为例，并提及一个关于L函数的猜想，因其数据图像令人想起鸟群飞舞而被命名为“椋鸟群飞猜想”（murmuration conjecture），生动展示了从数据中发现模式并触发新猜想的路径。

三、元数学

该路线将数学与理论物理视为一种语言系统，从“元”视角（即系统之外）出发，利用大语言模型处理海量的文献与符号。报告指出，大模型通过学习海量数据，能够掌握“引用”、“权威”和“体量”等非标准证明方法，从而在看似没有严格推理的情况下得到正确结果。
围绕这一思路，报告展望了未来以大模型为核心的推演与解题路线（如AlphaProof、AlphaGeometry、Frontier Math Project等）如何取得可能的进展，逐步形成自动生成解题思路的人机共研新范式。何教授也强调物理形式化仍在探索其可达边界。

何杨辉教授

        在互动环节中，与会师生围绕“形式化与直觉的分工与融合”、“大模型在严谨性与可复现性上的约束”、“如何构建高质量数学数据集”、“AI在数论与几何中的落地案例”、“对理论物理的反哺作用”等展开深入讨论。  

何教授强调，AI应当服务于从提出好问题到给出可信证据到完成可核验证明的完整链条。人机协作的关键在于明确任务边界，合理配置人类与机器的优势，并持续迭代共同语言（formal language与research narrative）。

交流互动环节

 本次论坛吸引6163银河线路检测中心的教师与研究生广泛参与。现场学术氛围浓厚，跨学科交流务实而高效。论坛通过蔻享学术直播平台同步播出，观看量达五千余人次。 

本次活动得到6163银河线路检测中心高能物理研究中心和粒子物理前沿学科创新引智基地的资助。

报告人简介：

何杨辉教授长期致力于弦论、代数几何、数论与机器学习的交叉研究，是人工智能辅助数学发现领域的积极推动者之一。其代表性工作涵盖：

- 以数据驱动方式揭示数学结构与规律；

- 在形式化证明与自动化推理方法上的推动；

- 将机器学习范式引入数学物理问题求解。 

相关成果在国际顶尖学术平台产生重要影响，推动了数学与人工智能的深度融合，为构建“可计算、可验证、可复用”的研究路线提供了坚实基础。