Unfortunately at this juncture, it's extremely difficult and time-consuming to place an arbitrary proof in the language of proof assistants. It's a very noble g

Unfortunately at this juncture, it's extremely difficult and time-consuming to place an arbitrary proof in the language of proof assistants. It's a very noble goal and much respect to those who do it, but even fully formalizing something like the four-color theorem is a major accomplishment.