I stumbled on your blog and then followed to this substack. Thank you for your very thoughtful article. I must admit that (like many fellow mathematicians) that I don't have much patience for philosophy and history of mathematics, but I do share your reservation about formalization of mathematics, on a narrower ground.
In my view, there is a long history of computer scientists and tech evangelists to oversell the value of automation. Inevitably, some comparison to basic tools like printing press or steam engine is made. However, computer automation has only changed the way we work, often not for the better. Even in the programmers' own domain, a new programming language is invented every month promising to raise programmers' productivity drastically. Needless to say none achieves that goal since new ones keep appearing. I think it's possible that the formalizers end up in a similar conundrum as the programmers, that a large amount of time is spent on satisfying the compiler instead of thinking about mathematics. If referring to someone else's theorem works similarly to importing a library in programming, I don't really envy a mathematician who is required to do that for their proof to be accepted.
In my view, the recent advances in machine learning has not changed the situation significantly. The "AI" succeeds in very narrow domain (like Go and chess), but only produces something that appears correct in the domain of language and arts. The AI optimists are counting on the mysterious singularity to validate their hypes. Now, it's entirely possible that the singularity will come in the near future, but I do doubt the current technology is a net benefit.
Thank you for your comment. Most of the colleagues with whom I speak agree with you but prefer not to say so in public. Peter Woit may have an explanation: in his recent report on next week's Fields Medal Symposium in Toronto,
"I’ve tried asking some of my colleagues what they think of all this activity, most common response so far is 'why aren’t they proving theorems instead of spending their time talking about this?'"
I have a good deal of sympathy with this question!
Good essay. However it seems to me that the discussion on power relations and critical thinking though being apt fall into an ironic contrast between what you write on the topic and say the example given on note 3.
Maybe its just me being cynical, but it leaves a certain distaste in my mouth nonetheless
Thank you for your comment and for the link to your essay. I'm not sure where our agreement is "violent"; I am much less keen than you on Frege, but that remains to be developed. Thank you for quoting me. I have some serious complaints about the way I was quoted in that Quanta article, outlined at https://mathematicswithoutapologies.wordpress.com/2020/09/01/the-inevitable-questions-about-automated-theorem-proving/; my continuing frustration with Quanta was one of the factors that led me to start Silicon Reckoner.
It's generous of you to say that I've triggered a discussion, but I haven't seen much evidence that this is the case. I hope more people who disagree with the hype, or propaganda, will speak up. I particularly appreciate section 6 of your essay, but when you write about "meaning" and that "There is no audience besides the audience of mathematicians," you have to bear in mind that much of the ethos of the mechanization project is already post-human and its most energetic protagonists are probably past being convinced.
I for one am in violent agreement with your take, and your caution in general. You have not failed to "explore the reasons for the absence of any sustained discussion of these issues". You were just first, and you have triggered such discussion yourself. You are way ahead of the hype curve on formalization, grappling with issues that are probably not going to surface in the mainstream mind until years from now. So I think the muted response is to be expected. I however aspire to be as ahead of the curve as you are. I am studying homotopy type theory and formalization of mathematics, and have used Lean enough to prove, for example, that the set of real-valued smooth functions on a manifold form an algebra. As part of a masters I'm doing at CMU I wrote an essay that quotes you and mirrors some of your ideas. You can check it out at http://greg.langmead.info/writing/frege/. My day job is in the area of machine learning, and I work for a tech giant. But I am revolted by the Szegedy Take on math as being literally empty, and am in alignment with your view of math as a human activity by definition. My essay tries to set up a dividing line, and to put Frege and most of the Lean community on our side of the line, even though they flirt with disaster. I look forward to future posts. (By the way, I did my PhD in math at Columbia with John Morgan, finishing in 2001. My masters work with homotopy type theory is a sort of part-time re-entry into the field that I love.)
I stumbled on your blog and then followed to this substack. Thank you for your very thoughtful article. I must admit that (like many fellow mathematicians) that I don't have much patience for philosophy and history of mathematics, but I do share your reservation about formalization of mathematics, on a narrower ground.
In my view, there is a long history of computer scientists and tech evangelists to oversell the value of automation. Inevitably, some comparison to basic tools like printing press or steam engine is made. However, computer automation has only changed the way we work, often not for the better. Even in the programmers' own domain, a new programming language is invented every month promising to raise programmers' productivity drastically. Needless to say none achieves that goal since new ones keep appearing. I think it's possible that the formalizers end up in a similar conundrum as the programmers, that a large amount of time is spent on satisfying the compiler instead of thinking about mathematics. If referring to someone else's theorem works similarly to importing a library in programming, I don't really envy a mathematician who is required to do that for their proof to be accepted.
In my view, the recent advances in machine learning has not changed the situation significantly. The "AI" succeeds in very narrow domain (like Go and chess), but only produces something that appears correct in the domain of language and arts. The AI optimists are counting on the mysterious singularity to validate their hypes. Now, it's entirely possible that the singularity will come in the near future, but I do doubt the current technology is a net benefit.
Thank you for your comment. Most of the colleagues with whom I speak agree with you but prefer not to say so in public. Peter Woit may have an explanation: in his recent report on next week's Fields Medal Symposium in Toronto,
https://www.math.columbia.edu/~woit/wordpress/?p=13087
he writes:
"I’ve tried asking some of my colleagues what they think of all this activity, most common response so far is 'why aren’t they proving theorems instead of spending their time talking about this?'"
I have a good deal of sympathy with this question!
Good essay. However it seems to me that the discussion on power relations and critical thinking though being apt fall into an ironic contrast between what you write on the topic and say the example given on note 3.
Maybe its just me being cynical, but it leaves a certain distaste in my mouth nonetheless
I'm not sure I understand what you mean by "ironic contrast." Could you be more specific?
Thank you for your comment and for the link to your essay. I'm not sure where our agreement is "violent"; I am much less keen than you on Frege, but that remains to be developed. Thank you for quoting me. I have some serious complaints about the way I was quoted in that Quanta article, outlined at https://mathematicswithoutapologies.wordpress.com/2020/09/01/the-inevitable-questions-about-automated-theorem-proving/; my continuing frustration with Quanta was one of the factors that led me to start Silicon Reckoner.
It's generous of you to say that I've triggered a discussion, but I haven't seen much evidence that this is the case. I hope more people who disagree with the hype, or propaganda, will speak up. I particularly appreciate section 6 of your essay, but when you write about "meaning" and that "There is no audience besides the audience of mathematicians," you have to bear in mind that much of the ethos of the mechanization project is already post-human and its most energetic protagonists are probably past being convinced.
I for one am in violent agreement with your take, and your caution in general. You have not failed to "explore the reasons for the absence of any sustained discussion of these issues". You were just first, and you have triggered such discussion yourself. You are way ahead of the hype curve on formalization, grappling with issues that are probably not going to surface in the mainstream mind until years from now. So I think the muted response is to be expected. I however aspire to be as ahead of the curve as you are. I am studying homotopy type theory and formalization of mathematics, and have used Lean enough to prove, for example, that the set of real-valued smooth functions on a manifold form an algebra. As part of a masters I'm doing at CMU I wrote an essay that quotes you and mirrors some of your ideas. You can check it out at http://greg.langmead.info/writing/frege/. My day job is in the area of machine learning, and I work for a tech giant. But I am revolted by the Szegedy Take on math as being literally empty, and am in alignment with your view of math as a human activity by definition. My essay tries to set up a dividing line, and to put Frege and most of the Lean community on our side of the line, even though they flirt with disaster. I look forward to future posts. (By the way, I did my PhD in math at Columbia with John Morgan, finishing in 2001. My masters work with homotopy type theory is a sort of part-time re-entry into the field that I love.)