主题：最近看到的笑话之五 -- 钛豌豆

计算机本身没其实没有算法，算法都是人设计好给计算机的。

大致看了一下那片论文，证明的思路很简单

首先，证明原命题等价于一个SAT问题，如果对应的SAT问题有解，则原命题成立；如果对应的SAT问题无解，则原命题不成立。然后，让计算机去解对应的SAT问题，反过来就可以知道原命题是不是成立。

结果c=2时计算机给出了成立的解，所以原命题在c=2时成立。但SAT是著名的np问题，计算机给出的解有13GB，无法人工验证计算机给出的解是否正确。

应该说，整个证明最最关键的是第一步。计算机完成的第二步就是个力气活，就是用人类设计好的算法进行运算即可。

当然这个运算本身很复杂，论文作者提到，原命题在c=3时，计算机算了一个月左右也没得出结果，所以该命题能证明还是证否仍然未知。