Currently transforming a new piece of maths from its "standard" form (i.e. what working mathematicians actually use) to something a computer can understand is a big task that usually takes a team of experts something of the order of years.

Maths is really hard and proofs require a tonne of steps. For this reason mathematicians have to be comfortable jumping over the standard pedestrian intermediate steps in proofs and just focusing on the important stuff. This is necessary because including all the details would obscure the important stuff (imagine directions for driving somewhere with steps like "now walk up to the car", "now click the opener", "now open the car door", "now sit down in the drivers seat").

Computers (currently) are way too dumb to skip these steps so you have to walk them through it.