就在前些日子（2021/2/3），一个以色列研究团队在Nature上发表了一篇有趣的论文[1，2]：他们开始用AI来给数学家出题了。
事情是这样的，这帮科学家写了一个称为“拉马努金机”（下面简称“拉机”）的程序，专业生产数学猜想。数学猜想大家都知道，就是对某种可能的数学规律的猜测，比如鼎鼎大名的“哥德巴赫猜想”，“费马大猜想”等等。这些猜想基本都是由一些天才数学家提出来的，不论证明与否，本身就需要顶尖智商和对数学结构的深刻洞察。“拉机”就做了这么件打破神话的事：它通过很暴力的方式去搜索数字中的规律，只要试的足够多，总能抓到一些新东西。当然，它也不知道抓到的东西到底是不是真的，不过没关系，抛出来给数学家嘛，让他们去证明嘛。于是，一个猜想狂“机”就诞生了。
当前这个“拉机”仅关注一些数学常数的猜想，这些常数包括自然对数的底e,圆周论π等等。这些常数绝大部分是无理数（无限不循环小数），或有理无理未知的数（如卡塔兰常数G）。“拉机”用一个无限嵌套的除式来表示这些常数，形式如下：
其中每个a和b都表示一个整数。对这些整数尝试不同的取值，并和标准方法得到的结果进行对比，就可以发现新的表达式。下面是“拉机”发现的一些猜想，这些定理已经被人们证明了：
另外还有些猜想没得到证明：
就这样，“拉机”硬是把数学猜想这件高大上的事变成了挖矿一样的苦力活，而且管挖不管埋，只管猜想不管证明。到目前为止，“拉机”还在不断猜想的路上，并不断把它新发现的猜想散布到网上（http://www.ramanujanmachine.com/），吸引数学家们去证明。
有趣的是，人工智能诞生后的第一件事就是去帮数学家证明定理，人来出题，机器来证明，这是AI的第一仗，而且赢的很漂亮。历史轮回，现在轮到AI出题，人来证明了。一个是利用了机器的演绎能力，一个是利用了机器的归纳能力，不论是哪种方式，都非常精彩。有人会问：机器又能提出猜想，又能做定理证明，那数学家们是不是要失业了？当然还没到那个时候，不过显而易见的是，未来AI会给数学家们提供越来越多的帮助。
最后解释一下“拉马努金机”这个名字。斯里尼瓦瑟·拉马努金，印度著名数学家，没受过正规的高等数学教育，沉迷于数论，特别是涉及各种数学常数的规律。他喜欢以直觉方式给出公式，不喜欢证明，但很多公式事后被证明是正确的。“拉马努金机”这个名字既是对这位天才数学家的纪念，也充分继承了他敢于挖坑，善于挖坑的行事风格，可谓恰如其分。
图1：斯里尼瓦瑟·拉马努金（1887年12月22日－1920年4月26日），印度著名数学家
图片来源于网络侵删
参考文献：
[1].AI maths whiz creates tough new problems for humans to solve， Nature News, 2021/2/3, https://www.nature.com/articles/d41586-021-00304-8
[2].Generating conjectures on fundamental constants with the Ramanujan Machine， Nature, 2021/2/3 https://www.nature.com/articles/s41586-021-03229-4