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 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.