发表机构
DI ENS, ENS, PSL University, CNRS, Inria（法国高等师范学院、巴黎文理研究大学、法国国家科学研究中心、法国国家信息与自动化研究所）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文构建 Lean 库，以描述复杂性为基础，通过逻辑刻画和归约形式化计算复杂性，证明 73 个完备性结果及类间关系和无条件下界。
AI 中文摘要
我们表明，描述复杂性可以作为在证明助手中形式化计算复杂性结果的基础，通过构建一个以以下概念为中心的 Lean 库：决策问题是有限结构上的同构不变谓词；复杂性类通过其逻辑刻画来定义；成员资格通过可定义性见证来证明；困难性通过从已知困难问题的一阶归约来证明。我们还建立了与传统机器模型（如（非）确定性图灵机）的桥梁。该库证明了 73 个完备性结果，涉及 68 个问题或问题族，覆盖 14 个不同的类；类之间的关系在逻辑内部建立，而非通过机器模拟，其中包括 NL = coNL 和 Abiteboul-Vianu 定理；以及无条件下界，其中包括 $\mathrm{FO}(\leq) \subsetneq \mathrm{FO}(\leq, \mathrm{TC})$ 和无序 FO(IFP) 无法捕获 PTIME 的结果。
英文摘要
We show that descriptive complexity can serve as a foundation for formalizing computational complexity results in a proof assistant, by constructing a Lean library centered around the following concepts: decision problems are isomorphism-invariant predicates on finite structures; complexity classes are defined by their logical characterization; membership is shown by definability witnesses; hardness is shown by first-order reductions from a known hard problem. We also establish bridges to traditional machine models such as (non)deterministic Turing machines. The library proves 73 completeness results, on 68 problems or problem families, over 14 different classes; relations between the classes established inside the logic and not by machine simulation, among them NL = coNL and the Abiteboul-Vianu theorem; and unconditional lower bounds, among them $\mathrm{FO}(\leq) \subsetneq \mathrm{FO}(\leq, \mathrm{TC})$ and the failure of order-free FO(IFP) to capture PTIME.
Comments25 pages. Library available at https://github.com/PierreSenellart/descriptive-complexity
