Consider the four color theorem. We have a proof by computer of this theorem, but it is far too complex for any human to verify. Would you agree that the fact that a computer built and programmed in a certain way claims to have proven the theorem is empirical evidence for the truth of the theorem?
No. The computer output is a strong justification for behaving as if all maps are four-colorable.
But if the “proof” cannot be understood, then the truth of the theorem is simply beyond human comprehension. We could petition the evolution fairy for a better brain. Then again, dogs don’t seem to mind that they can’t comprehend that the derivative of e^x is e^x.
No. The computer output is a strong justification for behaving as if all maps are four-colorable.
Would you feel differently if the proof were verified by a general AI? If not, how is this not just carbon chauvinism?
Also, if you want another example, consider the classification of finite simple groups. Here the combined proofs run into the 1000s of pages, and it is likely that no single human being has checked the entire thing. Is your analysis for that case different from that of the four color theorem?
Can the proof be understand by a motivated, human-intelligence Cartesian skeptic who is protected from errors of carelessness? Because a Cartesian skeptic will never derive true physics statements, no matter how much effort is applied, since the skeptic is cut off from empirical data by definition.
And I think that is an interesting distinction between math and physics.
I certainly admit that there are physical processes that could cause me to believe a false mathematical statement was true. But that is properly understood as a fact about me, and does not mean that math has any empirical content.
Can the proof be understand by a motivated, human-intelligence Cartesian skeptic who is protected from errors of carelessness?
To the same extent the proof of the four color theorem can be. It will just take orders of magnitude more time than any human has. So do you consider it to be proven in the same sense? Do you need to wait until such a person exists and does it? If so, why is that different?
No. The computer output is a strong justification for behaving as if all maps are four-colorable.
But if the “proof” cannot be understood, then the truth of the theorem is simply beyond human comprehension. We could petition the evolution fairy for a better brain. Then again, dogs don’t seem to mind that they can’t comprehend that the derivative of e^x is e^x.
Would you feel differently if the proof were verified by a general AI? If not, how is this not just carbon chauvinism?
Also, if you want another example, consider the classification of finite simple groups. Here the combined proofs run into the 1000s of pages, and it is likely that no single human being has checked the entire thing. Is your analysis for that case different from that of the four color theorem?
Can the proof be understand by a motivated, human-intelligence Cartesian skeptic who is protected from errors of carelessness? Because a Cartesian skeptic will never derive true physics statements, no matter how much effort is applied, since the skeptic is cut off from empirical data by definition.
And I think that is an interesting distinction between math and physics.
I certainly admit that there are physical processes that could cause me to believe a false mathematical statement was true. But that is properly understood as a fact about me, and does not mean that math has any empirical content.
To the same extent the proof of the four color theorem can be. It will just take orders of magnitude more time than any human has. So do you consider it to be proven in the same sense? Do you need to wait until such a person exists and does it? If so, why is that different?