[jstogin]

I have wondered this as well. In theory, I want to say yes. But in practice, at least in this subfield, there are so many unimportant details that might make this really difficult.

It's not a perfect analogy, but some parts of the proof feel more like neural networks than procedural algorithms. So instead of verifying the composition of two procedural algorithms g(f(x)), you have something more like g(nn(f(x))), where nn is some sort of ML model / neural network. Interestingly, we are starting to see progress in importing ML models as libraries (eg Huggingface), so maybe that can carry over someday? I don't know.

Another challenge is simply a practical one. You would need someone heavily interested in both black hole mathematics and formal proof verification to be able to do this. Both of these require years of training.