Hopefully someday, model checkers and proof assistants can help mathematicians to put these monster proofs into format that can be verified with computer.
When I was a student, I started making such a system. It would also be very beneficial for students for explaining complex proofs.
The main problem is not in model checker (there are plenty of them already), but to automatically convert between a model checker syntax (that looks rather like a programming language), and regular math paper syntax (which is free-form English, so you need general AI for reading that).
I was already quite experienced programmer at that time, but realized the UI/UX problem is too big for me alone, even if I'm going to parse some simplified English.
But with simplified English, the problem is definitely solvable, someone just needs to put their time/money in that. Once UX is good enough for mathematicians, professors or students, it will lift off and be the Wikipedia for Mathematics.
The space of proofs is enormous. Model checkers and proof assistants will probably become user friendly much sooner than they'll get good enough heuristics to navigate such spaces.
