There's an enormous amount of work to do before what you're saying can be possible. All of existing mathematics has to be encoded as a wikipedia-style library i

There's an enormous amount of work to do before what you're saying can be possible. All of existing mathematics has to be encoded as a wikipedia-style library in whatever flavor of theorem prover will win this round (Coq? Lean?) and as someone who has taken a decent run at encoding some theorems - it is non-trivial, both in terms of learning the theorem prover language, learning the math, and learning how to translate the math into the theorem prover language. The number of people worldwide who currently have the skills to do this probably number in the hundreds, and all of them are faced with the choice of contributing theorems or working incredibly lucrative finance/software jobs - or just researching novel mathematics! Even once the library is complete a huge amount of work remains to get using theorem provers to the same level of ergonomics as sketching things out on a chalk board.