We describe a Lean~4 formalization revisiting NYU Courant Technical Report TR1995-711 on the average-case complexity of Multilevel Syllogistic (MLS). The development encodes Reischuk--Schindelhauer average-case classes, an axiomatic MLS/EMLS semantics layer, a partial Ferro--Omodeo--Schwartz decision procedure with proved soundness and partial completeness on a membership-free fragment, serialization and step budgets, and conditional NP-average completeness and non-AvP hardness corollaries modulo explicitly documented structural axioms. Full Lean sources are inlined in the appendix modules.

翻译：我们描述了一个Lean~4形式化工作，重新审视纽约大学库朗技术报告TR1995-711中关于多层三段论（MLS）平均情形复杂度的内容。该工作编码了Reischuk-Schindelhauer平均情形类、一个公理化的MLS/EMLS语义层、一个针对无隶属片段的部分Ferro-Omodeo-Schwartz判定程序（附带正确性证明和部分完备性）、序列化与步骤预算，以及基于显式记录的结构公理推导出的条件性NP平均完备性和非AvP困难性推论。完整的Lean源代码内联于附录模块中。