If the tools are the same as the ones AlphaProof gets (i.e. a lean compiler) then no one would use them.
Well, hopefully that changes soon :)
This is the greatest idea ever. Why doesn't this exist?
This does sound like a lot of fun. Since this AI only reaches silver level, presumably such a contest could be quite competitive, with it not yet being clear cut whether a human or a tool-assisted human would come out on top, for any particular problem.