I still remain hopeful that this is a step change in capability and capacity that we can adopt and adapt towards our own purposes. What was taking decades for us to do has been reduced to days and dollars. So while we’re witnessing a forest fire consuming entire fields of open problems in math, the best upside would be finding new problems that come from learning how to work with the new tools.

This is what it seems like so far for software. The speed limit has changed. It’s interesting to explore what that means. Extending the analogy, long ago you could be a race car driver part time; that would be pretty laughable for an F1 driver. It’s a very specialized skill and the optimal athlete is quite different for driving a car than for running, for example. That feels like what I’m seeing in software.

The most effective folks are much faster and better with these tools than average. It’s a different skill set.

I think that formal verification makes Math much closer to code than many other fields. But I’m eager to see the first mathematicians that are dramatically more proficient with the new tools than average.