Well my whole point is that you have to build up a large codebase of formalized mathematics first, and you have to do it in an elegant way so it is easy to work

Well my whole point is that you have to build up a large codebase of formalized mathematics first, and you have to do it in an elegant way so it is easy to work with. Then verified programs is something we can start to realistically consider. But of course we can't do that yet (except in certain situations with great effort). It's really very similar to building up a whole software architecture. 30 years ago we were at machine code, now we are at maybe C. We want to get to the Figma of formalized mathematics. It will take many years but I don't see and conceptual hurdle, especially given the power of LLMs now.