[Cladode]

Yes, Coq has a tactics language. So does Isabelle. What I have in mind are primarily "Hammers", i.e. hooking in fully automatic theorem prover (e.g. MizAR for Mizar, Sledgehammer for Isabelle/HOL, HOL(y)Hammer for HOL Light and HOL4). As far as I'm aware, CoqHammer for Coq is work-in-progress and does not yet provide the level of automation that you get from Sledgehammer in Isabelle/HOL for years. But admittedly, it's been 4-5 years since I last used Coq. At the time, two core issues were the following:

- Existing automatic theorem provers often produced non-constructive proofs.

- Existing automatic theorem provers are mostly for FOL, so the gap to the much more powerful logics of Curry-Howard based provers is bigger than with weaker systems.

Have both problems been solved comprehensively as of January 2020?

[logicchains]

They have not been solved. My point was that automation via Coq's tactic language can serve as a decent substitute for "push-button" automation like Hammers, at least if one's continually working in the same domain and so can build up a library of tactics.