The Helix Center has now posted the video of Saturday’s round table on “Mechanization of Mathematics”. The discussion was lively and everyone agreed that we should meet again, or even that we should organize a conference on the theme.
Since concern about correctness of proofs is one of the primary motivations of mathematicians who are active in automated proof verification, it was interesting to hear several colleagues at the IAS quote the following remark about Solomon Lefschetz:
He had marvelous intuition, and so far as I know, all of the results he claimed in algebraic geometry have now been proved. When I was a graduate student at Princeton, it was frequently said that “Lefschetz never stated a false theorem nor gave a correct proof.”
This is Philip Griffiths reminiscing, in his contribution to the biographical memoirs of Lefschetz (on p. 289). The Helix Center discussion did raise the question of mechanizing mathematical intuition, but didn’t reach any conclusions. The mathematicians I know would prefer to have correct proofs of correct theorems, but if our choice were between mechanical generators of false proofs of false theorems and false proofs of true theorems I guess we would pick the latter — especially if they were as consequential as the hard Lefschetz theorem.
And indeed, I was surprised to learn — but perhaps I should not have been — that Griffiths’s description of Lefschetz fits quite of few of the mathematicians I have most admired (I won’t name names).
Several people I admire were in the audience and others were watching the livestream. Kevin Buzzard congratulated me for finding a way to quote William Burroughs (at 53′). I repeat the quotation for the reader’s convenience:
[The] junk merchant does not sell his product to the consumer, he sells the consumer to his product. He does not improve and simplify his merchandise. He degrades and simplifies the client.
—William Burroughs, Naked Lunch
UPDATE: A point I was trying to make at the roundtable, and also in the middle of this article, and in this post, about the inevitability of mechanization of mathematics (and of everything else, and of the monetization of the resulting data by tech companies), is made much more clearly and forcefully by Rose Eveleth in an article published today on Vox.