Can a machine find the hole in a 350-year-old philosophical proof?

Michael Jagdeo 1Jeff Dumps

1 Exponent Labs LLC

Explore the experiment ↓Read the paper ↗Code on GitHub ↗

Spinoza built the Ethics like geometry: definitions, axioms, propositions, proofs.

In 2026, Yuki Nakamura translated its core argument into Lean 4, making the logic precise enough for a machine to check.

We took Nakamura's formalization, searched it automatically with Vampire, and found two-element counter-models in about 0.1 seconds.

Lean certified them against Nakamura's own library.

A 1677 proof. Nakamura's 2026 formalization. Tiny possible worlds that show exactly what the assumptions fail to rule out.

Background · Spinoza's Ethics

A theory of everything,
built like geometry.

Baruch Spinoza's Ethics was published in 1677, the year of Spinoza's death. It tries to explain everything, from God to human happiness, and it does so the way Euclid explained geometry: definitions, axioms, and proofs.

What it claims

Exactly one thing exists on its own: call it God, or Nature. Everything else — people, planets, thoughts — exists in it, as a way it is. From there the book works out what a mind is, where emotions come from, and how a person can live freely.

How it argues

Like Euclid's geometry. First define the terms. Then state axioms, assumptions taken as obvious. Then prove propositions one at a time, each proof citing the definitions, axioms and earlier propositions it uses. Its full title is “Ethics, demonstrated in geometrical order.”

Why that invites a machine

An argument laid out as definitions, axioms and proofs can be checked step by step: does this proposition really follow from what it cites? Readers have disputed some of those steps for three and a half centuries. Today that is a question software can answer precisely.

Part I · Concerning GodPart II · The nature and origin of the mindPart III · The origin and nature of the emotionsPart IV · Human bondage, or the strength of the emotionsPart V · The power of the understanding, or human freedom

How Part I reaches “God is the only substance”

Quotations from R. H. M. Elwes's 1883 translation.

Definitions

→

Propositions

Click a step. Highlighted: what its demonstration cites. Part I alone has 8 definitions, 7 axioms and 36 propositions; this is the thread that runs to P14.

Proposition 14

God is the only substance.

“Besides God no substance can be granted or conceived.”

Its proof cites: D6, P11, P5 · take away P5 and this proof loses a premise.

The proof that God is the only substance leans on Proposition 5: no two substances share an attribute. If that step fails, the conclusion loses a support. That step is where this story begins.

Background · Nakamura's Lean project

Checking Spinoza
with a proof checker.

In 2026, Yuki Nakamura translated the core of Ethics Part I into Lean 4, a language in which a computer checks every step of a proof. The project is open source, and every result in the rest of this page builds on it.

What Lean is

A programming language for writing proofs. You state a claim and its proof as code, and a small, carefully trusted part of Lean called the kernel checks every step. If it accepts, no step was skipped or hand-waved. Mathematicians use it to check research mathematics.

What Nakamura built

Spinoza's definitions and axioms for Part I, written as Lean code, with the propositions that carry the argument (II to XIV) proved from them, including a layer for necessity and possibility. Every assumption added beyond Spinoza's text is listed in a register, and any step left unproven is listed openly as a gap rather than hidden.

What it found

A weak version of Proposition 5 can be proved: substances with exactly the same attributes are the same substance. The strong version cannot, from the assumptions tested. The evidence is a counter-model: a small invented world where every assumption is true and the claim is false. Nakamura built two such worlds by hand, with 4 and 3 objects.

Nakammura/spinoza-ethica-lean ↗Paper · arXiv:2605.02331 ↗Software DOI ↗

Y. Nakamura, Bennett's Conjecture in Lean 4: Counter-Models for the PSR-Reducibility of Spinoza's Propositions V and XIV, 2026. MIT-licensed; this work uses it at commit 6d4c046.

Building those worlds by hand is slow, and it does not scale to every step of every argument. Could a machine find them on its own?

01 / The question

Two substances,
one attribute?

Spinoza argues that only one substance exists, and Proposition 5 is the step that rules out two. Whether that step works is an old dispute. Nakamura's Lean 4 formalization made it precise: a weaker P5 follows from his assumptions, the stronger one does not.

Ethics I, Proposition 5

Spinoza, 1677

“There cannot exist in the universe two or more substances having the same nature or attribute.” (Elwes translation)

The step toward one substance, God.

the objection

Bennett

The demonstration does not establish the full conclusion from the resources Spinoza provides.

Two substances could share one attribute and differ in another.

the reply

Della Rocca

The Principle of Sufficient Reason can supply the missing route.

Distinct things must differ for a reason.

the test

Nakamura, 2026

Formalize the commitments in Lean 4 and ask what follows from what.

Counter-models for what does not; built by hand.

What counts as an answer

M ⊨ assumptions, M ⊭ claim

Failing to find a proof proves nothing: the search may simply be too weak. A counter-model, a structure where every assumption holds and the claim fails, shows the claim does not follow from those assumptions.

Nakamura's two negative results

  • S-A12. A12, an attribute belongs to one substance, does not follow from Nakamura's stated axioms plus a principle of sufficient reason (A22). Their counter-model: 4 elements, built by hand.
  • S-A15. A15, every attribute of a substance is an attribute of God, does not follow from the stated axioms plus plenitude. Their counter-model: 3 elements, built by hand.

02 / The experiment

Could a machine
find them on its own?

Our first pass searched Ethics I with two automatic provers, Z3 and Vampire. They found counter-models in milliseconds but produced no certificates: trust rested on two provers agreeing. Nakamura's were certified by Lean but built by hand. The plan became search with Vampire, certify with Lean, and that needed a tool.

  1. 01

    Read

    Nakamura's Definitions.lean and Axioms.lean at commit 6d4c046: 13 primitive predicates, the defined Substance, Attribute and IsGod, a 12-field axiom register (4 fields are True placeholders), and the sufficient-reason principles.

  2. 02

    Transcribe

    Into first-order TPTP. Primitives become predicates, definitions become biconditionals, the 8 nontrivial register fields become axioms, the weaker principle is an axiom and the contested one is the conjecture. Each line cites its Lean source.

  3. 03

    Validate

    Before trusting a negative result, reproduce Nakamura's positive ones: weak P5 must follow from the register plus A22, and A15 from the register plus A25 and A26. Both do.

  4. 04

    Search, blind

    Vampire's finite-model finder runs on Nakamura's axioms only. We had read their A15 counter-model earlier, but not their A12 one, and the search is automatic either way. Two-element models come back in about 0.1 s.

  5. 05

    Certify, twice

    Once as a Lean certificate of the transcription. Then as instances of Nakamura's own classes, EthicaWorld and StatedAxioms, compiled against a fresh clone of the unmodified library.

03 / The models

Two elements
where the hand-built one had four.

Vampire's answer for S-A12 is a world with two substances that share one attribute and differ in another. Sufficient reason is satisfied, and A12 fails. Try to break it.

A world with two substances

Click a cell: is this an attribute of that substance?

attributeS1S2
1
2

In this world the two elements are both the substances and the attributes (attribute 1 is S1 itself), which Nakamura's axioms allow (and, through A8 and A10, require of any attribute). Everything else is as Vampire found it; with it fixed, A22 and A12 are the only axioms this table can change.

A22 · sufficient reason

holds

Two distinct substances must differ in some attribute.

Holds: they differ in attribute 1.

A12 · the target

fails

An attribute belongs to only one substance.

Fails: 2 is an attribute of both substances.

Verdict

A counter-model: A12 does not follow.

Every assumption holds and the claim fails. The substances share an attribute yet differ in another: the shape of the classic objection to Ethics I P5.

S-A15 · two gods

Two elements, both substances and both gods. Element 1 is an attribute of 1 and of 2; element 2 is an attribute of 2 only. Attribute 2 belongs to a substance but not to god 1, so A15 fails, while plenitude holds because every substance is itself a god. Nakamura's hand-built model has 3 elements and the same two-gods shape.

Side by side

ResultNakamura's, by handOurs, automatic
S-A124 elements2 elements, 0.1 s
S-A153 elements2 elements, 0.1 s

04 / The certificate

Checked against
Nakamura's own library.

A transcription can be wrong. So the same models are compiled into instances of Nakamura's own Lean classes and checked by Lean's kernel against a fresh clone of the unmodified repository. The axioms checked here are Nakamura's own Lean definitions, so this check does not rest on our transcription of them; the premise and target statements are restated in the file, and those remain ours to get right.
import Ethica   -- Nakamura's library, unmodified, @ 6d4c046

inductive T where | e0 : T | e1 : T          -- Vampire's two elements

instance world : EthicaWorld T where          -- Nakamura's 13 primitives, as tables
  inItself x0 := tbl_inItself x0 = true
  intellectPerceivesAsEssence x0 x1 := tbl_intellectPerceivesAsEssence x0 x1 = true
  …

instance stated : StatedAxioms T where        -- Nakamura's 12-field register
  ax1_inItselfOrInAnother := by decide
  ax_attribute_perSe := by decide
  …

theorem holds_nak_A22 : … := by decide        -- sufficient reason holds
theorem target_fails : ¬ (… A12 …) := by decide  -- the target fails

theorem result : StatedAxioms T ∧ A22 ∧ ¬ A12 :=
  ⟨stated, holds_nak_A22, target_fails⟩

#print axioms AutoCM.A12.result   -- [propext]

Their classes, not ours. EthicaWorld and StatedAxioms come from Nakamura's repository; every field of the register is proved by decide on the two-element tables.

One axiom. Both results depend only on propext, one of Lean's standard axioms.

Excerpt of nakamura/AutoCM/A12.lean; the full file is 89 lines. It builds with Lean 4.13, the version their library pins.

05 / The map

Which assumptions
do the work?

With the tool working, we asked a broader question: for each result, which assumptions are actually needed? Remove one at a time; if the result stops following, a certified counter-model proves it.

A12 does not follow from the stated axioms plus sufficient reason

4elements · hand-built (Nakamura)

2elements · found by Vampire in 0.1 s

Two substances that share one attribute and differ in another: the classic objection to Ethics I P5.

Checked against Nakamura's unmodified Lean library; axioms [propext].

A15 does not follow from the stated axioms plus plenitude

3elements · hand-built (Nakamura)

2elements · found by Vampire in 0.1 s

Two gods, one lacking an attribute of the other.

Checked against Nakamura's unmodified Lean library; axioms [propext].

Which assumptions does each result need?

36 experiments, 105 s. Definitions of substance, attribute and God held fixed.

Without ↓ · target →weak P5A12A15
nothing removed
follows
does not follow
follows
any of the 8 stated axioms
not needed
still does not follow
not needed
A22 · sufficient reason for substances
needed
still does not follow
not needed
A25 · plenitude
not needed
still does not follow
needed
A26 · God is unique
not needed
still does not follow
needed

None of the eight nontrivial fields of the stated-axiom register is needed for these results: the logical work is done by the added sufficient-reason principles. Weak P5 needs A22 alone; A15 needs A25 and A26. "Needed" is kernel-certified; "not needed" rests on Vampire proofs, which are not certified here. A counter-model shows non-derivability, not full independence.

A reconstruction, not Spinoza.

Every result is about this formalization with its definitions held fixed. Whether it is the right reading of the Ethics is interpretation, the step where the machine stops.

Smaller is not more faithful.

In these models one object is both a substance and an attribute. The register allows it, and through A8 and A10 requires it of any attribute; a sorted encoding would be a different reconstruction, not a refinement.

Non-derivability, not independence.

A counter-model shows a claim does not follow. Independence would also need its negation not to follow, which is not tested here.

The first-order layer only.

Nakamura's reconstruction also has an S5 modal layer, which this work does not touch.

“Not needed” rests on Vampire.

In the dependency map, “needed” is kernel-certified; “not needed” means Vampire found a proof, which is not certified here.

06 / From one question to a tool

Built for Spinoza. Tested on everything.

The pipeline that certified these two models is general. On 100 TPTP problems drawn and frozen before any result, Vampire found 67 finite models and Lean's kernel alone certified 59 of them (88.1%). It also certified a theory of a million facts.

See how the tool works →

Questions

Frequently asked

What is lean-countermodel?
An open-source tool that shows a claim does not follow from a set of axioms, with a proof Lean 4 checks. Vampire, an automated prover, searches for a finite counter-model; lean-countermodel turns it into a Lean 4 certificate; Lean's kernel checks it.
What is a counter-model?
A small structure, or world, in which every assumption is true and the claim is false. Exhibiting one proves the claim does not follow from those assumptions. Failing to find a proof does not: the search may simply be too weak.
Does Spinoza's Proposition 5 follow from his axioms?
In Yuki Nakamura's Lean 4 formalization of Ethics Part I, a weak version follows (substances with exactly the same attributes are the same), but the strong one does not: A12, an attribute belongs to one substance, does not follow from the stated axioms plus a principle of sufficient reason. Nakamura showed this with a 4-element counter-model built by hand; lean-countermodel found a 2-element one automatically in about 0.1 seconds and certified it against Nakamura's own library. The result is about that formalization, not a verdict on Spinoza's text.
Why not just trust Vampire's answer?
Vampire is treated as untrusted. Only Lean's kernel decides whether a model becomes a certificate, so a wrong model never yields one. The translation from TPTP into Lean is trusted code, tested against an independent evaluator of the original formulas.
How well does it work beyond Spinoza?
On three samples of 100 problems from the TPTP library, Lean's kernel alone certified 71 of 78, 55 of 62 and 59 of 67 of the models Vampire found: 185 certificates. It also certified a problem with over a million facts in a median of 5.2 minutes on an 8 GB laptop.
How is this different from Isabelle's Nitpick?
Nitpick has found counterexamples in Isabelle/HOL since 2010. Lean 4 can import proofs from automated provers, but had no general automated front end for finding and certifying finite counter-models of abstract first-order theories. lean-countermodel provides one for untyped first-order logic in TPTP.
Was it peer reviewed?
It received an iterative, AI-generated technical review by Manus AI, requested by the authors, covering both the paper and the code. The final review recommends acceptance as a scoped formal-methods tool-and-engineering contribution. It is not an anonymous human review or a journal decision.
How do I run it?
Install Lean 4.35 (via elan), Python 3.12 and Vampire 5.1.0, clone github.com/exponentlabshq/lean-countermodel, run lake build, then python3 cm.py problem.p > P.lean && lake env lean P.lean. The README's quick start lists every step and what each should print.

Code: github.com/exponentlabshq/lean-countermodel · Paper: whitepaper (PDF)