I actually prototyped a system like this, mostly as an exercise to learn about crypto. You can't feasibly host or verify proofs on-chain, so you need external trusted verifiers (e.g. oracles). Making sure the oracles can't front-run proof submission is a challenge. Standard formal proof system (like Lean) are sufficiently expressive, although they weren't built for this and need to be modified to make sure a proof hasn't introduced any additional axioms, as you note. The proof system also becomes a point of attack, so you'd probably want multiple, independent verifiers (which themselves have been formally proved correct). I believe these exist for some proof systems, although I'm not sure about Lean's kernel.
Ultimately, I don't think this is really practical, and investing in AI proof agents is the way to go.
Ultimately, I don't think this is really practical, and investing in AI proof agents is the way to go.