Not sure if this question even makes sense, or if it sounds hopelessly naive to someone in the know, my maths education ended in undergrad -
can this type of push towards formalizing mathematical proofs be seen as a sort of continuation of Hilbert's program? If no, what's the difference? If yes, how are the fatal issues in that program avoided?
It is essentially “the most one can do with Hilbert’s Programme”.
Actually Hilbert’s Programme was shattered when his great hope (the proof of the consistency and completeness of Mathematics FINITISTICALLY) was proved impossible (actually inconsistent).
But from the point of view of mechanizing Maths, it is more or less equivalent.
can this type of push towards formalizing mathematical proofs be seen as a sort of continuation of Hilbert's program? If no, what's the difference? If yes, how are the fatal issues in that program avoided?