Wrt your update, > The idea that you can formally verify such a sequence of claims is .. mind boggling. Eh, if you're convinced that something's correct, it's

Wrt your update, > The idea that you can formally verify such a sequence of claims is .. mind boggling. Eh, if you're convinced that something's correct, it's not too mind-boggling that you can also explain it to a computer, given that it accepts all the same basic assumptions that you do. > There is a reason why very little progress has been made in formalizing math, and mistakes are sometimes discovered in even published proofs. Yep: it looks like Lean is making good progress on their goal of formalizing the "undergraduate curriculum," but that's only the tiniest sliver of math. Math is hard, and doing it formally is even harder, so all I'm saying is that contrary to your earlier statements, it's definitely possible.