舒尔数五

我们给出被称为舒尔数五（Schur Number Five）的百年难题的解：满足存在对从 1 到 $n$ 的正整数进行五色着色且无方程 $a + b = c$ 的单色解的最大（自然）数 $n$ 是多少？我们通过将问题编码为命题逻辑，并对所得公式应用大规模并行可满足性求解技术，得到解 $n = 160$。我们构造并验证了该解的证明，以增强对多 CPU 年计算正确性的信任。该证明大小为两拍字节，并使用一个形式化验证的证明检查器进行认证，表明可满足性求解器产生的任何结果——无论多大——现在都可以使用高度可信的系统进行验证。