There's an important distinction (spectrum?) between automated theorem provers and proof assistants. Coq is a proof assistant, which means that any automation i

There's an important distinction (spectrum?) between automated theorem provers and proof assistants. Coq is a proof assistant, which means that any automation is there to try to help the programmer by clearing away the tedious parts and leaving only the creative, fun parts. At the end of the day, it's still a human writing a proof. Afterward, Coq ultimately verifies the proof's integrity, which is an easy mechanical operation.