大家好，我是大老李。不久前在大老李的微信群中，有一位听众转了我一篇文章，是关于2016年国外研究者发表的一篇论文，这位研究者开发出了一个电脑程序，理论上，可以在有限的时间内，验证包括哥德巴赫猜想和黎曼猜想的正确性。
这篇论文中的发现非常有意思，我很想介绍给大家。但是看懂这篇论文需要的准备知识比较多，好在多数准备知识在大老李之前的节目中都或多或少提过了，比如哥德尔不完备定理，ZFC公理体系等。但欠缺的有关图灵机（Turing Machine）的介绍，所以今天先给大家介绍下图灵机。
（图灵，1912年6月23日—1954年6月7日，英国科学家，数学家，被称为计算机科学之父）
照例，大老李在介绍一个概念前，要先介绍下为什么要有这个概念。图灵为什么要提出图灵机这个概念呢？目的之一是为了回答希尔伯特和他的学生阿克曼（Wilhelm Ackermann）在1928年提出的一个问题：
是否存在一个算法，对某种形式化语言（Formal Language）中的逻辑命题，能够判断该命题的真假，并最终输出判断结果。这个问题后来被称为“可判定性问题”（Entscheidungsproblem）。
我知道你听了这个问题后还是一头雾水，什么叫“形式化语言”，这里的“逻辑命题”和“算法”又是啥？那我继续回溯一段历史。这个问题最早可以追溯到17世纪的莱布尼兹。莱布尼兹在帕斯卡的发明基础上，改进设计并制造了一台用机械装置驱动的计算机械：
(莱布尼兹设计制造的机械计算装置的复制品)
莱布尼兹还进一步设想，如果将来有一个机器不但能做数学运算，还能做逻辑推理就太棒了。只要直接“告诉”机器你的数学命题，机器能告诉你这个命题正确与否。而且，莱布尼兹还意识到，要达到这一目标，首要的一步的就是需要有一种机器可以读取的“Formal Language”，现在被翻译成“形式化语言”。
我想听众中可能也有不少人有过这种设想：数学证明的过程，如果全部用符号表示出来，似乎就是一种符号游戏了，甚至于都不需要理解符号所表示的实际意义。如果能把数学命题的证明，变成一种有规律可循的符号游戏，那可以让计算机去全权处理，数学家也就都下岗了。
但目前离这一目标还相差很远，现在能做的最好的也就是让机器去检查一个“证明”。我之前介绍“开普勒猜想”的文章中提到过，黑尔斯为了证明他的证明完全正确，不惜再用11年时间，用群体协作的方法，把他原来的证明用形式化语言重写了一次，然后交给机器证明检查软件，最终确认了他的证明正确。
let BARV3_SET_OF_LIST4 = prove_by_refinement(
`!V ul. packing V /\ barV V 3 ul ==>
set_of_list ul = {EL 0 ul,EL 1 ul, EL 2 ul, EL 3 ul}`,
(* {{{ proof *)
[
REPEAT WEAKER_STRIP_TAC;
INTRO_TAC Bump.set_of_list4 [`ul`];
ANTS_TAC;
REWRITE_TAC[arith `4 = 3 1`] THEN MATCH_MP_TAC Marchal_cells_3.BARV_LENGTH_LEMMA;
BY(ASM_MESON_TAC[]);
BY(MESON_TAC[])
]);;
(* }}} *)
(形式化证明代码的例子，摘自 https://github.com/flyspeck/ ，黑尔斯关于开普勒猜想的证明代码库)
说句题外话，关于现在闹得沸沸扬扬的日本东京大学望月新一教授所发表的，多数人看不懂的“abc猜想”的证明。如果有人能把望月教授的证明改写为形式化证明，交给机器检查，那么所有争议就都解决了。只是这个工作量，大概要以几十年起步，所以不知道有没有人肯这么去做。当然要去做，也只有懂望月那套理论的人去做了。这是题外话。
(京都大学的望月新一教授，2012发布了天书般的有关“abc猜想”的证明。关于他的证明是否成立，目前仍是数学界的一大争议。)
总之，莱布尼兹提出了有关机器证明的初步设想，并提出需要确立一种形式化语言。到十九世纪末，二十世纪初，数学家在数学公理化的工作方面做了很多工作，主流数学家接受了以策梅洛-弗兰克尔集合论，加选择公理所构成的ZFC公理系统，作为数学的逻辑推理基础。把皮亚诺算术公理作为数学研究对象的定义基础。这两套公理构成了数学大厦的地基。
1900年，德国数学家希尔伯特发布了他著名的“二十世纪重大的23个数学问题”，从他发布的问题来看，希尔伯特对构建完美的数学基础是充满希望的。其中第10个问题是：
对于一般的丢番图方程，能否通过某个确定的算法，经过有限的步骤，判定这类方程是否有整数解。
丢番图方程就是那种未知数比方程个数多的那种方程，一般这种方程都有无穷多个解。但是我们经常会加入只考虑整数解得情况，比如“费马大定理”所考虑的也是一种丢番图方程。看得出，希尔伯特的这个问题就是对机器证明问题的一个特例。
