真正复杂的计算在另一篇Platt自己写的论文里，我对此的贡献就是说服他去做这个计算 。其实在法国有很多公共资源，只要你能找到合适的人，跟他吃个午饭，这个计算就是这样子来的 。在这个论文里，Platt延续了他博士论文中的工作 。
还记得广义黎曼猜想吗?广义黎曼猜想涉及一类叫L函数的复变函数，它们在复平面上有无穷个非平凡零点 。要对这些无穷的东西搞验证似乎是不可能的 。但你可以考虑一个有限的问题，比如说先取十亿个L函数，然后对于每个函数，验证虚部绝对值小于十万的所有非平凡零点的实部都是1/2 。这是一个可以完成的验证 。类似的计算在十九世纪就有人做过，实际上黎曼在提出他的猜想时，就对黎曼ζ函数这个特殊的L函数验证过小于100左右的所有非平凡零点 。所以，从原则上，我们考虑的有限的验证可以用手算解决，不过一般还是靠计算机 。
Platt做的就是用计算机完成这样的计算，而且是以严格的方式 。对于数学验证而言，严谨性很重要 。我们知道，计算机只能表达有理数，它不能直接处理像圆周率这样的无理数 。所以，实际上计算机不能处理实数，它只能处理一个区间[a,b]，其中a和b都是有理数 。而你只能问你的计算机，能不能给出一个尽量短的区间[c,d]，使得区间[a,b]中的实数的正弦值(或者别的什么函数值)都落在区间[c,d]中 。这就是所谓的区间算术 。
有很多库可以处理区间算术，Platt他自己写了一个特别快的，不过网上也有不少类似的库 。我们需要用这些库，即使这意味着计算速度比直接用浮点数要慢上几倍，但计算的过程和结果是完全严谨的 。
问：您在证明中用到了计算机，那您对计算机在未来的数学证明中发挥的作用有什么看法呢?
答：这个问题挺有争议性的 。在我们的证明里，计算机做的就是验证一些有限的陈述，其实跟十九世纪那种手工验证也没什么区别，而且计算机出错的可能性比人要小多了 。你知道，把一串数字加起来可是计算机的强项 。基本上在计算机验证里发现的错误，罪魁祸首都是敲键盘的那个人 。
但计算机还能做别的东西 。现在，计算机能够独自证明一些简单的小引理 。最近有一篇论文，其中一个引理的证明就是计算机给出的 。那是一个很小的不等式，就像那些在高中数学竞赛中出现的不等式 。但这类不等式并不容易证明，所以它们才能出现在高中数学竞赛中 。但现在，有时候你可以将这种不等式直接输入计算机，然后计算机有可能直接给你一个证明，或者告诉你这个是对的 。这种计算机证明被接受了 。
这是一种新事物，因为计算机能处理这种问题也就是最近的事 。对付这种东西的算法还很原始，在实际操作过程中，为了能算出结果而又不死机，需要微调一大堆变量，在写代码时也要多花心思 。这类小引理的证明算是种偶尔会出现的新奇事物 。这也是个很有希望的方向，需要发展一下这方面的算法 。
不过要分清计算机证明与数值实验 。数值实验就是比如说我把某个东西验证到了一百万，然后我说它大概是对的，但这不是一个证明，而只是一种经验式的证据，告诉我们大概什么方向是对的 。而计算机证明，我们用到的就是对有限陈述的验证，原则上用笔和纸也能完成的那种 。这种有限的验证是不可避免的，因为在数学分析中，如果变量小于某个数值，主项和误差项相差不够远，这种情况就要一一验证 。要分清证明和证据，证据只能指引方向，而证明就真的是无误的逻辑证明 。
问：您的证明里用到了圆法，而张益唐的证明用到了筛法 。您能介绍一下这两种方法的异同吗?
答：筛法和圆法其实是很不同的，不过也有相似的地方 。有一种叫“大筛法”的，就跟圆法有关 。但这与张益唐主要用的“小筛法”很不同，当然他也稍微用到了一些大筛法 。圆法的本质就是应用在数论中的傅立叶分析，简单来说就是对圆周上的函数进行分析 。而筛法的目的则是给出素数分布的一种近似估计 。
在我的论文中就用到了大筛法和圆法的关系 。在大筛法中的一些技巧可以直接用到圆法中，反之亦然 。两者其实是同一枚硬币的正反两面 。张益唐的证明也用到了大筛法，因为他需要类似邦别里-维诺格拉多夫定理的结果，而那个定理是用大筛法的 。其实大约在八年前，大家就知道只要把邦别里-维诺格拉多夫定理的某个特殊情况推广一下，就可以得到张益唐的结论，而张益唐做的就是这一点 。八年来很多聪明人都铩羽而归，大家都觉得这是个很难的问题，但张益唐成功了 。我还没细读他的论文，但我感觉他虽然在这个意义上用到了大筛法，但他的改进并不在大筛法上，而是有关其它技巧的改进 。

• 哈洛德?贺欧夫各特：彻底证明弱哥德巴赫猜想(一)