I thought that was from the outset the intent of the Hilbert program, to automate mathematics. And mathematicians were behind it. Cannot see why they would be concerned when a different way to do the same, not subject to Gödel incompleteness, is working out. Maybe the frustration is that they were not the ones building it.

Hilbert's program was ultimately about humans studying the nature of mathematics. People had different opinions about whether the idea even made sense and what would be a desirable outcome.

Gödel's incompleteness also constrains human and AI mathematicians. Both just strive to prove whatever can be proven in the system they are working in.

Why do you think Godel Incompleteness doesnt apply? By default mathematicians work in ZFC which is proven to be incomplete...