Formalizing Leibniz

https://timlabs.org/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.