This is more like the popular lay take that are more or less confused about the meaning and implications of the theorems. The fact is that the implications are real yet more nuanced than this - something the article touched on.

Hilbert’s program was to reduce math to a finite set of axioms and was indeed derailed by incompleteness theorems(Gödel) and undecidability (Church, Turing).

Formalizing math with automated theorem provers has little to do with the goal of Hilbert program. Also they aren’t related to the foundational research that it entailed.

Also, as the article mentions, the implications as well as Gödel was largely misunderstood.