Spinoza’s Ethics.
Follow the demonstration.
Explore all five parts of the Ethics. The complete source library is separate from the deductions already checked by Lean.
Five parts. One philosophical system.
Read all 259 propositions, their demonstrations, definitions, axioms and supporting texts. Search the work and see what has been formalized.
Explore the complete Ethics ↗Choose Spinoza’s starting points
ETHICS / VERIFIED FRAGMENTSThis workshop generates only Lean-checked deductions from explicitly encoded starting points in Parts I and III. The remaining source texts can be read in the complete library; they are not inferred here.
Twenty conditional formal results, including reconstructions related to ten numbered propositions and preparatory steps toward XIV and XV. These are partial reconstructions; no complete historical demonstration has been independently certified.
Compare the source and the formalization ↗
Generate your deduction map
ROOTS → RESULTSSelect your starting points, then generate a separate map to zoom and explore. Known contradictions are explained here without opening a map.
Select a starting point to grow the tree.
Open the generated map ↗Test a counterexample to Proposition III
This is an optional user test, not an axiom attributed to Spinoza.
With Axioms IV and V selected, this test replaces the tree with a contradiction proof.
Sources and interpretation
TRACEABLE RECONSTRUCTIONPrimary source: Benedict de Spinoza, Ethics, all five parts. English translation by R. H. M. Elwes, Project Gutenberg eBook 3800. French passages on this site are our translations.
Read the primary source ↗The intermediate conceptual-separation node reconstructs a step in the proof of Proposition III; it is not a separately numbered proposition by Spinoza.
For Definition III, we encode independence as absence of dependence on distinct entities. For Axiom IV, we use a causal-to-conceptual implication. These are explicit modeling choices. Lean verifies deductions within this encoding, not its philosophical fidelity.
The external-cause result follows the alternative demonstration of the corollary to Proposition VI. We do not claim to formalize the full proof of Proposition VI or all meanings of production.
Inspect the Lean formalization ↗The Part III results follow Definitions I and II for the same actor and event. They are definitional consequences, not separately numbered propositions. The complete source library remains distinct from the verified deduction map.