He got a lot of things right in that video despite being just 2 years involved with mechanised theorem proving. I thought it was a fantastic and inspiring talk.

For example, when he said at the end, that it is obvious to him that this will change how mathematics is done in the future. Yeah, thought the same when I encountered this technology, but I was just a 2nd year math student back then, and Isabelle was developed in the same building. Still, obvious.

When he said that math is more about structure, not so much about induction; yeah, said the same at some ITP more than a decade ago. Got a dismissive question from Andrew Appel when I said that. Tobias Nipkow seemed to agree with the dismissal, I never understood the question though. Didn't get a reply when trying to investigate further on stage :-)

Of course set theory can be automated. I would argue, it can be automated even better than dependent types. Just embed the set theory including Grothendiek universes in simple type theory. The problem here is how to keep the notation sane, as for example + could be defined only once.

Tactic style theorem proving is sooooo old. It is how interactive theorem proving was done from the very beginning. Tactic style proofs are not readable at all except maybe via experiencing them by stepping through them. Declarative proofs are much more readable. Writing declarative proofs with the machine bridging the intermediate steps is the obvious future.

I was always astonished how people can learn stuff. When taking Latin classes, I thought, sure, I can kind of learn to read it, but speak it in real time? No way! But of course, at some point in time people have. Without understanding how.

AlphaGo Zero kind of explains how people can do something really difficult, even strategy based, without exactly knowing what they are doing. This is not much different from how mathematics is done. I think we will have a deep mathematician solving at least one of the remaining millennium problems within the next 20 years. The path starts exactly with how Buzzard and Hales envision it: Bring enough mathematics into one system, so that the millenium problems can actually be stated in the system. Machine learn that stuff. Give feedback to users, they will find it easier to use the system interactively. Create more mathematics. Machine learn that stuff. Rinse repeat.

This can be done. Certainly with 100 million dollars in funding.