> This is all a depressing and bleak future that I don’t look forward to.

Or, for the vast majority of humanity who aren't professional mathematicians, it's a liberating and empowering advancement.

I'm sorry if the automated digital theorem looms are eliminating the market for your handwoven proofs.