The problem with Hilbert’s program was, loosely, that the power to construct propositions was stronger than the power to mechanically check proofs. That is, the

The problem with Hilbert’s program was, loosely, that the power to construct propositions was stronger than the power to mechanically check proofs. That is, the formal language of propositional logic + number theory can construct propositions that are not decidable in a finite number of steps. There are two responses to this discovery: tweak the formal system so you can’t accidentally run into these traps, or shrug and just be more careful about how you prove things. Now that the world is increasingly computerized, it’s become clear that the right choice is to stop using a default form of mathematical reasoning that causes major issues for mechanized proof assistants and instead build a new foundation that is friendly to computers (but can be extended to support the power of classical formalisms)