I was surprised there weren't any "ambitious" wishes. Most, if not all, of the answers seem in response to practicality issues. Nothing along the terms of ML for math theorems or an accessible proof library for computers.
Scroll down:
"I'd like to have on a usb key a user friendly software that could parse a math article to check the proofs in it without having to learn how to use stuff like Coq and highlight the possible gaps. But this may sound unrealistic, at least for now."
