Because it takes a lot of extra time and work to formalize a proof to the level where it can be automatically checked.
Because it takes a lot of extra time and work to formalize a proof to the level where it can be automatically checked.