&gt; But a proof assistant aides you by checking your abstract thinking; you are still responsible for doing all the thinking yourself.<p>This isn&#x27;t really true. Nowadays, Coq can automate much of the process of coming up with a full proof - which is exactly what requires “abstract thinking”. (Of course, you still need to identify “strategic lemmas”, but even these lemmas can often be proven mostly automatically.) The downside is that machine-generated proofs are often gibberish from the point of view of human intelligibility, but that&#x27;s okay if you&#x27;re only interested in the truth of what is being proven.<p>&gt; This kind of tool aides in reasoning via a concrete example<p>Actually, going from a concrete example to a more general abstract concept requires you to do the thinking yourself. At least if you want the result of the generalization process to be valid.