[nutate]

Gotta love automatic theorem proving. I read the Shen language book on "logic, proof and computation" which got me into the idea of a theorem prover inside of your normal language.