On a separate note. It is not at all clear to me that "Lean"-related research strikes the "decision-makers in the business of war/defense" as (necessarily and consequentially) more intriguing than that pertaining to, say, "Langlands program". Nor is it apparent to me personally that it is any less potentially lethal (when suitably applied) granted the multitude of its potential far-reaching applications.
'Substitute “mathematics” for “novels” or “music” in those sentences and they remain inherently meaningful.'
Notwithstanding the similarities, the pertinent difference is that the validity of the "mathematical proof/narrative" is susceptible to formal verification. Consequently, a descendant (however distant) of ChatGPT capable of generating "mathematical narratives" can be purged of "hallucinations" when combined with "formal verification" assistant (however lean).
Why not keep the focus on the problem of doing automated math? Time, money, and compute. Such a focus puts the problem on such difficulties as to how to find parameters that produce a sample range that might sufficiently test a proof.
This approach seems in line with what you propose as reasonable for ascertaining a proof. Indeed, the most likely case is that not every proof will be able to show convergence, nor should it need to. However, should Kevin Buzzard be able to demonstrate proof by convergence in every instance (or above a certain percentage of cases), his argument might win out. So, is there middle ground here?
Here is a survey of some issues related to automated math, most all of which you are most likely aware of: https://asemicnet.blogspot.com/2024/01/untotal-asemic-eze-2024.html One of the problems that comes to the fore here is the problem of representation itself, let alone of understanding.
But, alas, philosophy is hard to resist. From Luke Dunne on Locke, here is a means to have an understanding without necessarily having the capacity for reflection:
"As to the Using Descartes’ concept of the idea, but denying that such ideas are found innately, John Locke then develops a theory of knowledge which explains how all of our ideas are ultimately drawn from experience. By way of experience, we acquire simple ideas, which correlate with the simplest forms of perception. The process of understanding is then one of putting together these simple forms; combining simple ideas into complex ones, holding several simple ideas in mind at once (and therefore, presumably, bringing to mind resonances or contrasts among the ideas and qualities of said ideas), and drawing general propositions by abstraction from these particular ideas. The limits of understanding for Locke are therefore the limits of perception and our processing faculties, and the question of just where those limits fall would become the major preoccupation of philosophers now placed in the same British Empiricist tradition." https://www.thecollector.com/john-locke-human-understanding/
It has been suggested that Ada Lovelace's remark about music was intended to tease Babbage, who hated barrel organs and even tried to have them banned.
On a separate note. It is not at all clear to me that "Lean"-related research strikes the "decision-makers in the business of war/defense" as (necessarily and consequentially) more intriguing than that pertaining to, say, "Langlands program". Nor is it apparent to me personally that it is any less potentially lethal (when suitably applied) granted the multitude of its potential far-reaching applications.
'Substitute “mathematics” for “novels” or “music” in those sentences and they remain inherently meaningful.'
Notwithstanding the similarities, the pertinent difference is that the validity of the "mathematical proof/narrative" is susceptible to formal verification. Consequently, a descendant (however distant) of ChatGPT capable of generating "mathematical narratives" can be purged of "hallucinations" when combined with "formal verification" assistant (however lean).
Why not keep the focus on the problem of doing automated math? Time, money, and compute. Such a focus puts the problem on such difficulties as to how to find parameters that produce a sample range that might sufficiently test a proof.
This approach seems in line with what you propose as reasonable for ascertaining a proof. Indeed, the most likely case is that not every proof will be able to show convergence, nor should it need to. However, should Kevin Buzzard be able to demonstrate proof by convergence in every instance (or above a certain percentage of cases), his argument might win out. So, is there middle ground here?
Here is a survey of some issues related to automated math, most all of which you are most likely aware of: https://asemicnet.blogspot.com/2024/01/untotal-asemic-eze-2024.html One of the problems that comes to the fore here is the problem of representation itself, let alone of understanding.
But, alas, philosophy is hard to resist. From Luke Dunne on Locke, here is a means to have an understanding without necessarily having the capacity for reflection:
"As to the Using Descartes’ concept of the idea, but denying that such ideas are found innately, John Locke then develops a theory of knowledge which explains how all of our ideas are ultimately drawn from experience. By way of experience, we acquire simple ideas, which correlate with the simplest forms of perception. The process of understanding is then one of putting together these simple forms; combining simple ideas into complex ones, holding several simple ideas in mind at once (and therefore, presumably, bringing to mind resonances or contrasts among the ideas and qualities of said ideas), and drawing general propositions by abstraction from these particular ideas. The limits of understanding for Locke are therefore the limits of perception and our processing faculties, and the question of just where those limits fall would become the major preoccupation of philosophers now placed in the same British Empiricist tradition." https://www.thecollector.com/john-locke-human-understanding/
Keep up the great posts!
It has been suggested that Ada Lovelace's remark about music was intended to tease Babbage, who hated barrel organs and even tried to have them banned.