[bolus]

First of all, mathematics is not about T/F. Think of the axiom of choice, the law of excluded middle, the axiom of inaccessible cardinals, etc.

For the second, understanding why and actually proving something can be related but they're not equivalent. Of course, the intuitive ideas can lead to the right formal technicalities but it is not always the case.

There are two aspects of mathematical proofs-communication of ideas and formal verification. Confusing these distinction can be dangerous and this is why mathematicians led to the area of type theory and formal proofs.

Voedovsky, you can google him to find who he was, lost his faith in "human proof checking" after some error on his peer-reviewed and published result was accidentally discovered after years of nobody doubting its validity.

He dreamed of the world where people do and enjoy mathematics freely leaving the boring parts to computers like mathematicians in nowadays don't worry about how their writing will be published and communicated. What we do is write a proof and leave actual typesetting to the computer. It's called (La)TeX.

What you're saying is like claiming this program is correct because its logic is correct without ever knowing whether the code itself would get compiled or not. More extremely, there's no value for having more and more pseudocodes that we don't know they'll ever terminate or not.