Formalizing anything in a proof assistant such as Coq multiplies the amount of work required by orders of magnitude. Proving something on a computer almost univ

Formalizing anything in a proof assistant such as Coq multiplies the amount of work required by orders of magnitude. Proving something on a computer almost universally requires way more ingenuity than proving it on paper. > Is anyone trying to fill the gap? I don't think that the state of things is likely to improve because automatic theorem proving is equivalent to the halting problem. What you're describing is work that is best suited for computer algebra software.