Each proposition is a node; supports is an edge toward what it rests on. Proposition 1 is the root. The file proves:
download · paste into live.lean-lang.org to check it yourself.
loading…
the propositions of the Tractatus Logico-Blueskyicus, formalized. every theorem below is closed by decide.
Each proposition is a node; supports is an edge toward what it rests on. Proposition 1 is the root. The file proves:
download · paste into live.lean-lang.org to check it yourself.
loading…