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.

Although this is a common way of stating what Godel's incompleteness theorem tells us, it's actually not correct. As was posted upthread, when you combine Godel's first incompleteness theorem with Godel's completeness theorem (all this in first-order logic), you find that, for any sentence that is not provable in a system of first-order logic (such as the Godel sentence for that system), there must be a semantic model of that first-order logic in which the sentence is false. (I gave an example of such a model for the first-order axioms of arithmetic upthread.)

Would the rules of said machine have statements they themselves cannot prove by parameters set in their ‘programmed(by humans, machines, or other machines)’ assumptions?

Like people saying Godel theorems "prove" LLMs could never invent new mathematics because being a software system Godel applies to their operation, but not to humans which are not axiomatic systems, and thus humans can go beyond them and beyond the limits of Godel, humans can "know" a result to be true even if Godel says you can't prove it.

This is just flatly untrue, in the strictest possible sense, and even in the generous definition of "statements that mathematicians care about", that is going to be very heavily biased towards questions that are decidable, because the questions that are likely to be decidable are the ones that they can even reason about to begin with.

If you're a computer programmer, the CS shadow of Godel comes up _all the time_ in practice, and undecidable situations are quite common and don't really need to be carefully constructed.

This is just the drunk-in-the-streetlight situation. Things seem to be decidable everywhere we look because we look where things are likely to be decidable.