[eab-]

> Just insist on Lean (or some other formal verifier) proofs for everything

Lean is too inflexible for this, in my opinion. Maybe I'm not dreaming big enough, but I think there'll have to be one more big idea to make this possible; I think the typeclass inference systems we use these days are a severe bottleneck, for one, and I think it's very, very tedious to state some things in Lean (my go-to example is the finite-dimensionality of modular forms of level 1 - the contour integral is a bitch and has a lot of technicalities)

[ykonstant]

I agree, although I don't see a better solution: typeclass inference is trying to "quasi-solve" higher unification, which is unsolvable. The core tactics writers are already doing wizard-level stuff and there is more to come, but the challenge is immense.

By the way, if you are a meta-programming wizard and/or a Prolog wizard, please consider learning Lean 4 or another tactics based proof assistant. I think they will all welcome expert assistance in the development of better tactics and the improvement and debugging of current ones.