[DerpDerpDerp]

Because until very, very recently, we simply haven't had the means to compute any proofs that mattered.

Rendering even relatively simple high level concepts in to low-level structures and then deriving them in the basic steps takes massive amounts of resources. At least one proof took over 15,000 pages of text (had you printed it).

A secondary problem (which we've been working on for a couple decades now) is that we lack the machinery to translate the results back in to something human readable. At some level, mathematics is about the ability of humans to understand the relationships between things, so computer proofs that only the computer understands don't really help us - especially if we can't relate them meaningfully to our other knowledge.

I mean, people have been trying for hundreds or thousands of years - it's just kind of a hard problem.