In A Study of Spinoza's Ethics (1984, §17), Jonathan Bennett argues that the demonstration of Proposition V of Spinoza's Ethica contains identifiable invalid moves and that, even granted those moves, "cannot yield more than the conclusion that two substances could not have all their attributes in common" -- while Spinoza concludes that they cannot share any. Bennett doubts that any valid reconstruction is available from Spinoza's stated resources without importing further commitments. Michael Della Rocca (Spinoza, 2008, ch. 2) responds that the proposition can be derived if the Principle of Sufficient Reason (PSR) is committed substantively. The debate has remained at the level of prose argument for forty years. This paper provides the first machine-checked evidence in the debate. We formalise Ethica Pars I in Lean 4, encoding Bennett's reading of Spinoza's stated axioms as a typeclass and Della Rocca's substantive PSR as an extension class. The derivation attempt yields a partial result -- substances sharing all attributes are identical -- but cannot reach the full "sharing-any-attribute -> identity" content of Proposition V, mechanically tracking Bennett's own all-attributes ceiling. A four-element counter-model satisfying both axiom sets while falsifying Proposition V's content establishes the irreducibility against this specific augmentation. A second counter-model establishes the analogous result for axiom A15, a load-bearing universality clause for Spinoza's Proposition XIV. Bennett's diagnosis receives its first kernel-checked counter-model against the Della-Rocca PSR-substance reconstruction (the non-derivability claim itself a meta-logical consequence of kernel consistency); stronger PSR variants and the broader narrative claim against the full Section I + II + A1--A7 register remain open as future mechanical projects.

翻译：在《斯宾诺莎〈伦理学〉研究》(1984, §17)中，乔纳森·班尼特指出，斯宾诺莎《伦理学》命题V的论证包含可识别的无效步骤，并且即使认可这些步骤，"也无法得出多于'两个实体不可能共有全部属性'的结论"——而斯宾诺莎的结论是它们不能共有任何属性。班尼特怀疑，在不引入额外承诺的情况下，斯宾诺莎所提供的资源中不存在任何有效的重构方案。迈克尔·德拉·罗卡（《斯宾诺莎》，2008年，第2章）回应称，若充分承诺充足理由律，该命题可被推导出来。四十年来，这场争论始终停留在散文论证层面。本文为这场争论提供了首个机器检验的证据。我们在Lean 4中形式化了《伦理学》第一部分，将班尼特对斯宾诺莎既定公理的解读编码为一个类型类，并将德拉·罗卡实质性的PSR编码为一个扩展类。推导尝试产生了一个部分结果——共享所有属性的实体是同一的——但未能得出命题V完整的"共享任一属性→同一性"内容，机械地追踪了班尼特自身提出的"全属性界限"。一个满足两套公理集同时证伪命题V内容的四元素反模型，确立了针对这一特定扩充的不可归约性。第二个反模型为公理A15（斯宾诺莎命题XIV中承载关键负载的普遍性条款）建立了类似结果。班尼特的诊断首次获得了针对德拉·罗卡PSR-实体重构的核检验反模型（不可推导性主张本身即为核一致性的元逻辑推论）；更强的PSR变体及针对完整第一、二部分加A1-A7总登记册的更广泛叙事主张，仍留待未来的机械化项目探索。