I predicted, over 2 years ago, that theorem proving would fall way before other problems that people believe are harder.

https://news.ycombinator.com/item?id=41072330

There was a Wired Magazine article from either the late 90s or early 2000s that made a prediction that this sort of thing would eventually be possible, likely within my lifetime. I believe the context was "distributed computing" models of the time, like SETI.

I've never been able to find that article as an adult, but I would love to know who wrote it.

Fucking even called LEAN the “hottest shit under the sun”—which it is. You, legend you!