The complete Ethics.
Read, trace, formalize.
All five parts and all 259 numbered propositions, with their demonstrations, corollaries and commentary in Elwes’s English edition.
Return to the deduction workshop ↗Browse the work
The library contains source texts. Only explicitly marked reconstructions have Lean proofs. A textual demonstration is not a machine-checked deduction.
English is the complete source language. French entries appear only when their translation is stored in GitHub. Untranslated entries are hidden in French mode.
0 matching entries
Edition and formalization
Source: Benedict de Spinoza, Ethics. English translation by R. H. M. Elwes, Project Gutenberg eBook 3800. Original spelling is retained; HTML and whitespace are normalized. French passages are our translations.
Read the complete source edition ↗The complete work is indexed here. Formalizing all its demonstrations requires additional models of attributes, ideas, bodies, affects and knowledge. The catalog does not turn unproved propositions into axioms.
View the source register and formalization scope ↗