One doesn't need to be an expert in machine readable mathematics, to understand how to formalize it to a machine readable form.

If one takes the time to read the free book accompanying the metamath software, and re implements it in about a weekend time, you learn to understand how it works internally. Then playing around a little with mmj2 or so you quickly learn how to formalize a proof you understand. If you understand your own proof its easy to formalize it. One doesn't need to be "an expert in machine readable mathematics".