[6gvONxR4sf7o]

On a slight tangent, this line makes me think about aspects of automated provers that I don’t even know if we’ve begun thinking about:

> “It’s a sensational breakthrough,” says Alex Kontorovich, a mathematician at Rutgers University. “There are a bunch of new ideas going into this proof that people are going to be mining for years.”

Frequently, a proof of a thing is less interesting as a way to bring rigor than it is as a new way to look at a thing. I wonder if there’s been any work on that side of things in automated mathematics?