Proof Assistants being seriously useful for everyday garden variety serious mathematical developments

[Timothy Y. Chow]

Harvey Friedman wrote:

> OVERALL OPINION. The prospects for Proof Assistants being seriously 
> useful for everyday garden variety serious mathematical developments 
> look extremely remote for the foreseeable future.

I don't think that "extremely remote for the foreseeable future" is true 
any more.  For example, undergraduates at Imperial College, working with 
Kevin Buzzard, are learning to use proof assistants and are building 
infrastructure for increasingly sophisticated mathematical content. 
Twenty years from now, I predict they'll be using proof assistants as 
routinely as today's mathematicians use computer algebra systems.

Harvey, you cite your own experience anecdotally, but to be honest, I 
think you're a rather atypical person to pick for an anecdote.  You don't 
even write your own manuscripts in LaTeX, you use the FOM mailing list 
whose technology was already creaky 20 years ago, etc.  To predict what 
the scene will be like in a couple of decades, one has to look at what the 
younger generation is interested in and comfortable with.

There are some interesting examples of "real math" being aided and abetted 
by proof assistants in this MathOverflow question:

https://mathoverflow.net/a/312661

Tim