https://www.zhihu.com/question/4534672056
大老李注：本文原为我对知乎问题：“据报道Grok3证明黎曼猜想是一个虚假案例。想问一下目前AI在破解数学难题上有哪些真实案例？”的回答。现转载于此。
说两个我知道的案例。
一个是陶哲轩最近组织的集体项目：等式理论[1]（Equational theories project）。这个项目的目标是搞清原群（Magma）中，4个运算符以内的等式关系之间的推导关系。
学过群理论的都知道有一系列群公理，其中有结合律：
抛开群的性质，仅考虑一个集合和某个运算 ，就构成一个“原群”。其中我们可以写出很多的“等式”，比如，借用陶哲轩在博客[2]上给出的例子：
等式1： 等式2： 等式3： 等式4： 等式5： 等式6： 等式7： 等式8： 等式9： 等式10： 等式11：
我们可以问，以上等式中，有何种蕴含关系？最终答案是这样一张哈斯图（Hasse diagram）：
其中 的意思，就是从a可以推出b。“x=y”的意思是任何两个变量都相等，群中也就只有一个元素，所以是最强的等式。其中有些推导关系并不那么明显，比如你可以试试看证明，从等式4： 证明等式7：（答案在陶哲轩的博文[3]中）。
以上等式中最多出现了3个运算符 。如果考虑最多四个运算符的等式，则可以计算出一共有4694个这样的等式，共产生 个可能的蕴含关系。
等式理论项目的目标就是通过群体协作方法，把每一个可能的箭头关系的证明任务分配到个人。与此同时，个人需要写出正确的[Lean proof verification](https://en.wikipedia.org/wiki/Lean_(proof_assistant "Lean proof verification")) code，证明每个箭头关系成立或不成立。过程中，可以利用AI进行代码补全，生成需要的Lean code。
此项目从2024年9月25日启动，到今天（2024年12月5日），完成进度已达99.99986%，仅剩30个关系未能证明：
产生的一个局部哈斯图如下，括号中是等式在项目中的序号：
以下是一个关于等式1692的未证明的蕴含例子。等式1692是：
已证明等式1692蕴含等式1：，证明代码是：
@[equational_result]
theorem Equation1629_implies_Equation1 (G: Type _) [Magma G] (h: Equation1629 G) : Equation1 G := by
intro _
rfl
但还未证明其是否蕴含等式23：。更多的项目成果可以浏览：https://teorth.github.io/equational_theories/
此项目不能完全算是AI的成果，因为AI的代码补全能力虽然很强，但很多细节还是需要人工干预和修正，人和AI的贡献大概各50%。所以，这是一个很好的人机合作领域，我觉得这种类型的工作也是近期AI能够在数学领域所能作的主要贡献。
第二个例子是2023年12月，Deepmind公司推出的Funsearch[4]。
Deepmind使用Funsearch，找到了一个新的算法，使得帽集问题（Cap Set Problem[5]）的下限从 提高到了 。
(上图：a中，可以看到在n=8时，Funsearch的算法找到了比已知结果更大的cap set。b是Funsearch产生的关键算法。c为由funsearch的算法启发，直接构建512个元素的Cap set的函数)
Funsearch也在bin packing，Admissible sets等问题上也有所突破。Funsearch的主要原理就是不停地让AI写代码，不断更新算法，以期找出比当前算法更好的版本。
它的局限性也很明显，即只能处理一些可以用算法解决的问题，并且它的结果只能产生更好的上下界，但无法得知是否是确界。
另外一个问题是，它很费钱。因为Funsearch需要不停调用LLM API，所以要么你有一个非常强劲的机器，可以在本地运行一个大语言模型API，要么就需要调用商用的API。无论哪种方案，都很费钱，不适合个人使用。
以上就是我知道的，AI在解决数学难题中，有所贡献的两个例子。目前AI所能解决的数学难题（指人类还不能解决的）的类型局限性非常大，距离AI能独立解决数学难题的目标还非常遥远。但是，在人机配合的情况下，现在的AI已经能发挥非常好的作用，特别是在当可以把某些大难题的划分为非常多的小问题时（比如等式关系项目），AI就会好用，可以大大节省时间。
等式理论: https://github.com/teorth/equational_theories
[2]博客: https://terrytao.wordpress.com/2024/09/25/a-pilot-project-in-universal-algebra-to-explore-new-ways-to-collaborate-and-use-machine-assistance/
[3]博文: https://terrytao.wordpress.com/2024/09/25/a-pilot-project-in-universal-algebra-to-explore-new-ways-to-collaborate-and-use-machine-assistance/
[4]Funsearch: https://deepmind.google/discover/blog/funsearch-making-new-discoveries-in-mathematical-sciences-using-large-language-models/
[5]Cap Set Problem: https://zhuanlan.zhihu.com/p/684485418
