规模最优排序网络的形式化：提取一个认证证明集
Formalizing Size-Optimal Sorting Networks: Extracting a Certified Proof Checker
摘要：
自从1976年四色定理的证明以来，计算机生成证明在数学和计算机科学中已经成为现实。在过去的十年中，我们已经看到了正式的证明，使用验证证明助手被用来验证这种证明的有效性。在本文中，我们描述了一个形式化的理论的大小最优排序网络。从这个形式化，我们提取一个认证的检查器，成功地验证了计算机生成的最优性证明多达8个输入。该检查器依赖于一个不可信的预言机，以快捷方式搜索超过160万个NP完全子问题的证人。
英文摘要：
Since the proof of the four color theorem in 1976, computer-generated proofs have become a reality in mathematics and computer science. During the last decade, we have seen formal proofs using verified proof assistants being used to verify the validity of such proofs. In this paper, we describe a formalized theory of size-optimal sorting networks. From this formalization we extract a certified checker that successfully verifies computer-generated proofs of optimality on up to 8 inputs. The checker relies on an untrusted oracle to shortcut the search for witnesses on more than 1.6 million NP-complete subproblems.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
