Proof Assistants being seriously useful for everyday garden variety serious mathematical developments
Timothy Y. Chow
tchow at math.princeton.edu
Thu Feb 25 21:30:25 EST 2021
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:
More information about the FOM