People speak disparagingly about blowing one’s own trumpet. But who else can be relied upon to blow it? So here is my effort to explain how uncritically accepting mathematical folklore about proofs can lead of computationalism about mind: https://link.springer.com/article/10.1007/s11229-022-03812-w#Abs1
Thank you for pointing this out. If I had known I would have quoted your article extensively but I will do so in the future. I agree with almost everything and certainly agree with the original title of the draft, which diligent readers can still find online.
My first slight disagreement is with the name "Standard View"; I prefer "Central Dogma" because (a) it is catchier and (b) like the Central Dogma of Molecular Biology, this one is fruitful but also unnecessarily restrictive.
My other disagreement has to do with sampling bias. Practically no mathematicians have expressed opinions on the relation between informal and formal proofs. I interpret this to mean that most mathematicians have no settled opinion on the matter, and that the few who do speak up are unrepresentative. But overall I am grateful for your explication of the issues, which is much clearer than mine could have been.
Thanks for these kind words. Two points well taken. The second especially—this discussion (in philosophy) is still of the sort that begins “Here’s what The Folk say…”. I was at a meeting yesterday of people hoping to shift the study of mathematical practices on from there.
It is not actually clear what the relevance of the precise definition of understanding is to the phenomenon of computerized mathematics. Can we not be a bit selfish and, instead of asking whether computers will understand mathematics, focus on the less philosophically fraught question of whether computers will help us understand mathematics in new ways by producing explanations that instill novel insights?
The conjectures that (1) they will and (2) all this computerized reasoning™ stuff will be required to do that seem like relatively concrete empirical claims (and hard ones to dispute, at least to me). (One can remove the answer of "they already have" by demanding the "explanations" occur in natural language and not graphs and datasets, I think.)
But I guess I can see a partial counterargument to the above selfishness! If one meets, e.g., a new graduate student, both "I don't care at all if you understand these new ideas, I just care if you can explain them to me" and "I don't care at all if you can explain these new ideas to me, I just care if you understand them yourself" would be inappropriate attitudes to take. So maybe both questions are worth studying in tandem.
I'm going to let this stand, because I agree with both the argument and the counterargument, with only the comment that, as far as I know, no corporation is remotely interested in the problem of developing systems that can explain mathematics in the style of a successful colloquium talk — with the ability to answer unexpected questions.
But why must we understand AI research through the lens of what corporations are or aren't doing? It seems that as the frontier of technical possibility advances, if corporations abandon a particular direction, it's frequently possible for hobbyists to pick it up and achieve similar or better things only slightly later (as happened with chess AI, for example).
I don't think it's possible to achieve the successful colloquium talk thing right now (I don't think we can really even convincingly mimic an unsuccessful colloquium talk which no one in the audience understands yet, but that might happen pretty soon) but when it becomes possible it might be possible for mathematicians to do it with the resources we have access to.
Thank you Michael, wonderfully illuminating. Hillary Putnam abandoned the computational theory of the mind for me good reasons. Why reduce intelligence to the how and abandon the why, to goal achievement rather than goal imagination, to be providing answers rather than discovering questions?
People speak disparagingly about blowing one’s own trumpet. But who else can be relied upon to blow it? So here is my effort to explain how uncritically accepting mathematical folklore about proofs can lead of computationalism about mind: https://link.springer.com/article/10.1007/s11229-022-03812-w#Abs1
Thank you for pointing this out. If I had known I would have quoted your article extensively but I will do so in the future. I agree with almost everything and certainly agree with the original title of the draft, which diligent readers can still find online.
My first slight disagreement is with the name "Standard View"; I prefer "Central Dogma" because (a) it is catchier and (b) like the Central Dogma of Molecular Biology, this one is fruitful but also unnecessarily restrictive.
My other disagreement has to do with sampling bias. Practically no mathematicians have expressed opinions on the relation between informal and formal proofs. I interpret this to mean that most mathematicians have no settled opinion on the matter, and that the few who do speak up are unrepresentative. But overall I am grateful for your explication of the issues, which is much clearer than mine could have been.
Thanks for these kind words. Two points well taken. The second especially—this discussion (in philosophy) is still of the sort that begins “Here’s what The Folk say…”. I was at a meeting yesterday of people hoping to shift the study of mathematical practices on from there.
It is not actually clear what the relevance of the precise definition of understanding is to the phenomenon of computerized mathematics. Can we not be a bit selfish and, instead of asking whether computers will understand mathematics, focus on the less philosophically fraught question of whether computers will help us understand mathematics in new ways by producing explanations that instill novel insights?
The conjectures that (1) they will and (2) all this computerized reasoning™ stuff will be required to do that seem like relatively concrete empirical claims (and hard ones to dispute, at least to me). (One can remove the answer of "they already have" by demanding the "explanations" occur in natural language and not graphs and datasets, I think.)
But I guess I can see a partial counterargument to the above selfishness! If one meets, e.g., a new graduate student, both "I don't care at all if you understand these new ideas, I just care if you can explain them to me" and "I don't care at all if you can explain these new ideas to me, I just care if you understand them yourself" would be inappropriate attitudes to take. So maybe both questions are worth studying in tandem.
I'm going to let this stand, because I agree with both the argument and the counterargument, with only the comment that, as far as I know, no corporation is remotely interested in the problem of developing systems that can explain mathematics in the style of a successful colloquium talk — with the ability to answer unexpected questions.
Thanks!
But why must we understand AI research through the lens of what corporations are or aren't doing? It seems that as the frontier of technical possibility advances, if corporations abandon a particular direction, it's frequently possible for hobbyists to pick it up and achieve similar or better things only slightly later (as happened with chess AI, for example).
I don't think it's possible to achieve the successful colloquium talk thing right now (I don't think we can really even convincingly mimic an unsuccessful colloquium talk which no one in the audience understands yet, but that might happen pretty soon) but when it becomes possible it might be possible for mathematicians to do it with the resources we have access to.
Thank you Michael, wonderfully illuminating. Hillary Putnam abandoned the computational theory of the mind for me good reasons. Why reduce intelligence to the how and abandon the why, to goal achievement rather than goal imagination, to be providing answers rather than discovering questions?
Corrected: Thank you for catching that!