It's possible, but difficult. Proofs written by humans tend to not include a bunch of relevant details and assumptions. They consist of lines like "We have some property/object/logical statement X, then by theorem Y we have Z", but often don't state how exactly they are using theorem Y to get result Z. There's often some additional algebraic or logical manipulation, or some simplification of terms, or implicitly using some other theorem or lemma that seems obvious to the writer.

Getting a computer to automatically find proofs of statements is difficult (impossible in general), and I wouldn't be surprised if converting a standard human-written proof into a formal proof system is just as hard.