Parent is referring to something a bit different - Hilbert’s program was about all of mathematics, even that which hadn’t been discovered yet, whereas the parent is talking about formalizing existing mathematical knowledge in some HoTT-enabled programming language or proof-checker (hence the emphasis on verifying and the problem of siloed knowledge).

Obviously true theorems with existing proofs don’t apply to Godelian incompleteness.