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.

Gödel blocked the path to axiomatic derivation of a full consistent body of mathematics as far as I understand. Mathematicians and AI are not working in these constraints but rather with these constraints.