Log in to follow projects

Following a project allows you to receive updates via email. It also lets the owner know that you like them.


Formalizing Leibniz

By Tim Smith

A proof of God by Leibniz, formalized in the Oak proof checker.

100% complete
1 follower 2163 views
About Log (0) Discussion (0)

Formalizing Leibniz


Leibniz's De Arte Combinatoria ("On the Art of Combination"), published in 1666, contains a proof of God, which I thought would be fun to formalize in my proof checker Oak. The proof is a "first mover" argument, with a twist to avoid an infinite regress. It was already organized into premises and numbered steps, with each step citing earlier steps or premises, but the logic was not always clear.

The main challenges were consistently rendering his terms (e.g. keeping straight the Latin words for "moves", "mover", "is moved"), making the premises and body of the proof fit together, and filling some gaps. I had to carefully interpet his argument, and add a few premises of my own, to make it come out right, but I am happy with the result.