舒尔五号
Schur Number Five
摘要：
我们提出了一个世纪的老问题的解决方案称为舒尔数五：什么是最大的（自然）数$n$，使存在一个五着色的正数高达$n$没有单色解决方案的方程$a + b = c$？我们得到的解决方案，$n = 160$，通过编码的问题到命题逻辑和应用大规模并行可满足性求解技术的结果公式。我们构建并验证了解决方案的证明，以增加对多CPU年计算正确性的信任。证明大小为2 PB，并使用正式验证的证明检查器进行了认证，表明可满足性求解器的任何结果-无论多大-现在都可以使用高度可信的系统进行验证。
英文摘要：
We present the solution of a century-old problem known as Schur Number Five: What is the largest (natural) number $n$ such that there exists a five-coloring of the positive numbers up to $n$ without a monochromatic solution of the equation $a + b = c$? We obtained the solution, $n = 160$, by encoding the problem into propositional logic and applying massively parallel satisfiability solving techniques on the resulting formula. We constructed and validated a proof of the solution to increase trust in the correctness of the multi-CPU-year computations. The proof is two petabytes in size and was certified using a formally verified proof checker, demonstrating that any result by satisfiability solvers---no matter how large---can now be validated using highly trustworthy systems.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
