Recently I had a conversation where I defended the rationality behind my being skeptical of the validity of the proofs and conclusions constructed in very abstracted, and not experimentally or formally verified math fields.
To my surprise, this provoked a very heated debate, where I was criticized for being overly confident in my assessments of fields I have very little contact with (I was expecting begrudging agreement). But there was very little rebuttal of my points! The rest of my conversation group had three arguments:
Results which much of a given field in math rests get significant attention.
Mathematicians would be highly renowned for falsifying an assumption many others were basing their work on.
You know very little about math as a field, so you should trust mathematicians when they tell you something is likely true.
These each seem flawed. My responses:
It is not always apparent on which results a given field in math rests, and many fields rely on many other fields for their conclusions, so I’m skeptical of the implicit claim that there are often very few results imported from other fields in a particular field, and that it is easy to enumerate those assumptions. Surely easier than in other fields, but still not absolutely easy. Its not like math papers come with an easy to read requirements.txt file. And even if they did, from programming we know its still not so easy.
Maybe this is true, maybe not. What is certain is attempting to falsify results won’t get you renown, so mathematicians need to choose between taking the boring & un-glamorous gamble of attempting to falsify someone’s results, or choose the far more engaging & glamorous option of proving a new theorem. I expect the super-majority choose to prove new theorems. It is easy to prove a theorem, it is far harder to find the one rotten proof in a pile of reasonable proofs (and even then you still need to go through the work of trying to correct it!).
I agree I know very little about math as an academic discipline, but this does not mean I should blindly trust mathematicians. Instead, I should invoke the lessons from Inadequate Equilibria, and ask whether math seems the type of field whose incentives sufficiently reward shorts in the market on math results compared to the difficulty & cost of such shorts. And I don’t think it does, as argued in 2[1].
The argument was unfortunately cut short, as we began arguing in circles. I don’t think my interlocutors ever understood the points I was making, though I also don’t think they tried very hard. They may have just been too shocked at my criticism of two sacred objects of nerd culture (academia, and math) to be able to hear my arguments. But I could have also been bad at explaining myself.
Unrelated to the validity of my argument, I always feel an internal pain whenever someone suggests deferring to authority, especially when I’m questioning the reliability of that authority to begin with. Perhaps, you argue, the mathematician has thought a lot about math. So if anyone knows the validity of a math proof, it is them. I respond: The theologian has thought far more about God than me. Yet I don’t defer to them about the existence of God. Why? Because there is no way to profitably short their belief while correcting it.
Long complicated proofs almost always have mistakes. So in that sense you are right. But its very rare for the mistakes to turn out to be important or hard to fix.
In my opinion the only really logical defense of Academic Mathematics as an epistemic process is that it does seem to generate reliable knowledge. You can read through this thread: https://mathoverflow.net/questions/35468/widely-accepted-mathematical-results-that-were-later-shown-to-be-wrong. There just don’t seem to be very many recent results that were widely accepted but proven wrong later. Certainly not many ‘important’ results. The situation was different in the 1800s but standard for rigor have risen.
Admittedly this isn’t the most convincing argument in the world. But it convinces me and I am fairly able to follow academic mathematics.
If you had a lot of very smart coders working on a centuries old operating system, and never once running it, every function of which takes 1 hour to 1 day to understand, each coder is put under a lot of pressure to write useful functions, not so much to show that others’ functions are flawed, and you pointed out that we don’t see many important functions being shown to be wrong, I wouldn’t even expect the code to compile, nevermind run even after all the syntax errors are fixed!
The lack of important results being shown to be wrong is evidence, and even more & interesting evidence is (I’ve heard) when important results are shown to be wrong, there’s often a simple fix. I’m still skeptical though, because it just seems like such an impossible task!
People metaphorically run parts of the code themselves all the time! Its quite common for people to work through proofs of major theorems themselves. As a grad student it is expected you will make an effort to understand the derivation of as much of the foundational results in your sub-field as you can. A large part of the rationale is pedagogical but it is also good practice. It is definitely considered moderately distasteful to cite results you dont understand and good mathematicians do try to minimize it. Its rare that an important theorem has a proof that is unusually hard to check out yourself.
Also a few people like Terrance Tao have personally gone through a LOT of results and written up explanations. Terry Tao doesn’t seem to report that he looks into X field and finds fatal errors.
As a grad student it is expected you will make an effort to understand the derivation of as much of the foundational results in your sub-field as you can […] It is definitely considered moderately distasteful to cite results you dont understand and good mathematicians do try to minimize it.
Yeah, that seems like a feature of math that violates assumption 2 argument 1. If people are actually constantly checking each others’ work, and never citing anything they don’t understand, that leaves me much more optimistic.
This seems like a rarity. I wonder how this culture developed.
One way that the analogy with code doesn’t carry over is that in math, you often can’t even being to use a theorem if you don’t know a lot of detail about what the objects in the theorem mean, and often knowing what they mean is pretty close to knowing why the theorem’s you’re building on are true. Being handed a theorem is less like being handed an API and more like being handed a sentence in a foreign language. I can’t begin to make use of the information content in the sentence until I learn what every symbol means and how the grammar works, and at that point I could have written the sentence myself.
skeptical of the validity of the proofs and conclusions constructed in very abstracted, and not experimentally or formally verified math fields.
Can you give a few examples? I can’t tell if you’re skeptical that proofs are correct, or whether you think the QED is wrong in meaninful ways, or just unclearly proven from minimal axioms. Or whether you’re skeptical that a proof is “valid” in saying something about the real world (which isn’t necessarily the province of math, but often gets claimed).
I don’t think your claim is meaningful, and I wouldn’t care to argue on either side. Sure, be skeptical of everything. But you need to specify what you have lower credence in than your conversational partner does.
I can’t give a few examples, only a criteria under which I don’t trust mathematical reasoning: When there are few experiments you can do to verify claims, and when the proofs aren’t formally verified. Then I’m skeptical that the stated assumptions of the field truly prove the claimed results, and I’m very confident not all the proofs provided are correct.
For example, despite being very abstracted, I wouldn’t doubt the claimed proofs of cryptographers.
OK, I also don’t doubt the cryptographers (especially after some real-world time in ensuring implementations can’t be attacked, which validates both the math and the implementation.
I was thrown off by your specification of “in math fields”, which made me wonder if you meant you thought a lot of formal proofs were wrong. I think some probably are, but it’s not my default assumption.
If instead you meant “practical fields that use math, but don’t formally prove their assertions”, then I’m totally with you. And I’d still recommend being specific in debates—the default position of scepticism may be reasonable, but any given evaluation will be based on actual reasons for THAT claim, not just your prior.
No, I meant that most of non-practical mathematics have incorrect conclusions. (I have since changed my mind, but for reasons in an above comment thread).
Still a bit confused without examples about what is a “conclusion” of “non-practical mathematics”, if not the QED of a proof. But if that’s what you mean, you could just say “erroneous proof” rather than “invalid conclusion”.
The reason I don’t say erroneous proof is because I want to distinguish between the claim that most proofs are wrong, and most conclusions are wrong. I thought most conclusions would be wrong, but thought much more confidently most proofs would be wrong, because mathematicians often have extra reasons & intuition to believe their conclusions are correct. The claim that most proofs are wrong is far weaker than the claim most conclusions are wrong.
Hmm. I’m not sure which is stronger. For all proofs I know, the conclusion is part of it such that if the conclusion is wrong, the proof is wrong. The reverse isn’t true—if the proof is right, the conclusion is right. Unless you mean “the proof doesn’t apply in cases being claimed”, but I’d hesitate to call that a conclusion of the proof.
Again, a few examples would clarify what you (used to) claim.
I’ll bow out here—thanks for the discussion. I’ll read futher comments, but probably won’t participate in the thread.
Either way, with the slow march of the Lean community, we can hope to see which of us are right in our lifetimes. Perhaps there will be another schism in math if the formal verifiers are unable to validate certain fields, leading to more rigorous “real mathematics” which are able to be verified in Lean, and less rigorous “mathematics” which insists their proofs, while hard to find a good formal representation for, are still valid, and the failure of the Lean community to integrate their field is more of an indictment of the Lean developers & the project of formally verified proofs than the relevant group of math fields.
Here’s an example of what I think you mean by “proofs and conclusions constructed in very abstracted, and not experimentally or formally verified math”:
Given two intersecting lines AB and CD intersecting at point P, the angle measure of two opposite angles APC and BPD are equal. The proof? Both sides are symmetrical so it makes sense for them to be equal.
On the other hand, Lean-style proofs (which I understand you to claim to be better) involve multiple steps, each of which is backed by a reasoning step, until one shows that LHS equals RHS, which here would involve showing that angle APC = BPD:
angle APC + angle CPB = 180 * (because of some theorem)
angle CPB + angle BPD = 180 * (same)
[...]
angle APC = angle BPD (substitution?)
There’s a sense in which I feel like this is a lot more complicated a topic than what you claim here. Sure, it seems like going Lean (which also means actually using Lean4 and not just doing things on paper) would lead to lot more reliable proof results, but I feel like the genesis of a proof may be highly creative, and this is likely to involve the first approach to figuring out a proof. And once one has a grasp of the rough direction with which they want to prove some conjecture, then they might decide to use intense rigor.
To me this seems to be intensely related to intelligence (as in, the AI alignment meaning-cluster of that word). Trying to force yourself to do things Lean4 style when you can use higher level abstractions and capabilities, feels to me like writing programs in assembly when you can write them in C instead.
On the other hand, it is the case that I would trust Lean4 style proofs more than humanly written elegance-backed proofs. Which is why my compromise here is that perhaps both have their utility.
They definitely both have their validity. They probably each also make some results more salient than other results. I’d guess in the future there’ll be easier Lean tools than we currently have, which make the practice feel less like writing in Assembly. Either because of clever theorem construction, or outside tools like LLMs (if they don’t become generally intelligent, they should be able to fill in the stupid stuff pretty competently).
Recently I had a conversation where I defended the rationality behind my being skeptical of the validity of the proofs and conclusions constructed in very abstracted, and not experimentally or formally verified math fields.
To my surprise, this provoked a very heated debate, where I was criticized for being overly confident in my assessments of fields I have very little contact with (I was expecting begrudging agreement). But there was very little rebuttal of my points! The rest of my conversation group had three arguments:
Results which much of a given field in math rests get significant attention.
Mathematicians would be highly renowned for falsifying an assumption many others were basing their work on.
You know very little about math as a field, so you should trust mathematicians when they tell you something is likely true.
These each seem flawed. My responses:
It is not always apparent on which results a given field in math rests, and many fields rely on many other fields for their conclusions, so I’m skeptical of the implicit claim that there are often very few results imported from other fields in a particular field, and that it is easy to enumerate those assumptions. Surely easier than in other fields, but still not absolutely easy. Its not like math papers come with an easy to read
requirements.txt
file. And even if they did, from programming we know its still not so easy.Maybe this is true, maybe not. What is certain is attempting to falsify results won’t get you renown, so mathematicians need to choose between taking the boring & un-glamorous gamble of attempting to falsify someone’s results, or choose the far more engaging & glamorous option of proving a new theorem. I expect the super-majority choose to prove new theorems. It is easy to prove a theorem, it is far harder to find the one rotten proof in a pile of reasonable proofs (and even then you still need to go through the work of trying to correct it!).
I agree I know very little about math as an academic discipline, but this does not mean I should blindly trust mathematicians. Instead, I should invoke the lessons from Inadequate Equilibria, and ask whether math seems the type of field whose incentives sufficiently reward shorts in the market on math results compared to the difficulty & cost of such shorts. And I don’t think it does, as argued in 2[1].
The argument was unfortunately cut short, as we began arguing in circles. I don’t think my interlocutors ever understood the points I was making, though I also don’t think they tried very hard. They may have just been too shocked at my criticism of two sacred objects of nerd culture (academia, and math) to be able to hear my arguments. But I could have also been bad at explaining myself.
Unrelated to the validity of my argument, I always feel an internal pain whenever someone suggests deferring to authority, especially when I’m questioning the reliability of that authority to begin with. Perhaps, you argue, the mathematician has thought a lot about math. So if anyone knows the validity of a math proof, it is them. I respond: The theologian has thought far more about God than me. Yet I don’t defer to them about the existence of God. Why? Because there is no way to profitably short their belief while correcting it.
Long complicated proofs almost always have mistakes. So in that sense you are right. But its very rare for the mistakes to turn out to be important or hard to fix.
In my opinion the only really logical defense of Academic Mathematics as an epistemic process is that it does seem to generate reliable knowledge. You can read through this thread: https://mathoverflow.net/questions/35468/widely-accepted-mathematical-results-that-were-later-shown-to-be-wrong. There just don’t seem to be very many recent results that were widely accepted but proven wrong later. Certainly not many ‘important’ results. The situation was different in the 1800s but standard for rigor have risen.
Admittedly this isn’t the most convincing argument in the world. But it convinces me and I am fairly able to follow academic mathematics.
If you had a lot of very smart coders working on a centuries old operating system, and never once running it, every function of which takes 1 hour to 1 day to understand, each coder is put under a lot of pressure to write useful functions, not so much to show that others’ functions are flawed, and you pointed out that we don’t see many important functions being shown to be wrong, I wouldn’t even expect the code to compile, nevermind run even after all the syntax errors are fixed!
The lack of important results being shown to be wrong is evidence, and even more & interesting evidence is (I’ve heard) when important results are shown to be wrong, there’s often a simple fix. I’m still skeptical though, because it just seems like such an impossible task!
People metaphorically run parts of the code themselves all the time! Its quite common for people to work through proofs of major theorems themselves. As a grad student it is expected you will make an effort to understand the derivation of as much of the foundational results in your sub-field as you can. A large part of the rationale is pedagogical but it is also good practice. It is definitely considered moderately distasteful to cite results you dont understand and good mathematicians do try to minimize it. Its rare that an important theorem has a proof that is unusually hard to check out yourself.
Also a few people like Terrance Tao have personally gone through a LOT of results and written up explanations. Terry Tao doesn’t seem to report that he looks into X field and finds fatal errors.
Yeah, that seems like a feature of math that violates
assumption 2argument 1. If people are actually constantly checking each others’ work, and never citing anything they don’t understand, that leaves me much more optimistic.This seems like a rarity. I wonder how this culture developed.
One way that the analogy with code doesn’t carry over is that in math, you often can’t even being to use a theorem if you don’t know a lot of detail about what the objects in the theorem mean, and often knowing what they mean is pretty close to knowing why the theorem’s you’re building on are true. Being handed a theorem is less like being handed an API and more like being handed a sentence in a foreign language. I can’t begin to make use of the information content in the sentence until I learn what every symbol means and how the grammar works, and at that point I could have written the sentence myself.
Can you give a few examples? I can’t tell if you’re skeptical that proofs are correct, or whether you think the QED is wrong in meaninful ways, or just unclearly proven from minimal axioms. Or whether you’re skeptical that a proof is “valid” in saying something about the real world (which isn’t necessarily the province of math, but often gets claimed).
I don’t think your claim is meaningful, and I wouldn’t care to argue on either side. Sure, be skeptical of everything. But you need to specify what you have lower credence in than your conversational partner does.
I can’t give a few examples, only a criteria under which I don’t trust mathematical reasoning: When there are few experiments you can do to verify claims, and when the proofs aren’t formally verified. Then I’m skeptical that the stated assumptions of the field truly prove the claimed results, and I’m very confident not all the proofs provided are correct.
For example, despite being very abstracted, I wouldn’t doubt the claimed proofs of cryptographers.
OK, I also don’t doubt the cryptographers (especially after some real-world time in ensuring implementations can’t be attacked, which validates both the math and the implementation.
I was thrown off by your specification of “in math fields”, which made me wonder if you meant you thought a lot of formal proofs were wrong. I think some probably are, but it’s not my default assumption.
If instead you meant “practical fields that use math, but don’t formally prove their assertions”, then I’m totally with you. And I’d still recommend being specific in debates—the default position of scepticism may be reasonable, but any given evaluation will be based on actual reasons for THAT claim, not just your prior.
No, I meant that most of non-practical mathematics have incorrect conclusions. (I have since changed my mind, but for reasons in an above comment thread).
Still a bit confused without examples about what is a “conclusion” of “non-practical mathematics”, if not the QED of a proof. But if that’s what you mean, you could just say “erroneous proof” rather than “invalid conclusion”.
Anyway, interesting discussion.
The reason I don’t say erroneous proof is because I want to distinguish between the claim that most proofs are wrong, and most conclusions are wrong. I thought most conclusions would be wrong, but thought much more confidently most proofs would be wrong, because mathematicians often have extra reasons & intuition to believe their conclusions are correct. The claim that most proofs are wrong is far weaker than the claim most conclusions are wrong.
Hmm. I’m not sure which is stronger. For all proofs I know, the conclusion is part of it such that if the conclusion is wrong, the proof is wrong. The reverse isn’t true—if the proof is right, the conclusion is right. Unless you mean “the proof doesn’t apply in cases being claimed”, but I’d hesitate to call that a conclusion of the proof.
Again, a few examples would clarify what you (used to) claim.
I’ll bow out here—thanks for the discussion. I’ll read futher comments, but probably won’t participate in the thread.
Either way, with the slow march of the Lean community, we can hope to see which of us are right in our lifetimes. Perhaps there will be another schism in math if the formal verifiers are unable to validate certain fields, leading to more rigorous “real mathematics” which are able to be verified in Lean, and less rigorous “mathematics” which insists their proofs, while hard to find a good formal representation for, are still valid, and the failure of the Lean community to integrate their field is more of an indictment of the Lean developers & the project of formally verified proofs than the relevant group of math fields.
Here’s an example of what I think you mean by “proofs and conclusions constructed in very abstracted, and not experimentally or formally verified math”:
Given two intersecting lines AB and CD intersecting at point P, the angle measure of two opposite angles APC and BPD are equal. The proof? Both sides are symmetrical so it makes sense for them to be equal.
On the other hand, Lean-style proofs (which I understand you to claim to be better) involve multiple steps, each of which is backed by a reasoning step, until one shows that LHS equals RHS, which here would involve showing that angle APC = BPD:
angle APC + angle CPB = 180 * (because of some theorem)
angle CPB + angle BPD = 180 * (same)
[...]
angle APC = angle BPD (substitution?)
There’s a sense in which I feel like this is a lot more complicated a topic than what you claim here. Sure, it seems like going Lean (which also means actually using Lean4 and not just doing things on paper) would lead to lot more reliable proof results, but I feel like the genesis of a proof may be highly creative, and this is likely to involve the first approach to figuring out a proof. And once one has a grasp of the rough direction with which they want to prove some conjecture, then they might decide to use intense rigor.
To me this seems to be intensely related to intelligence (as in, the AI alignment meaning-cluster of that word). Trying to force yourself to do things Lean4 style when you can use higher level abstractions and capabilities, feels to me like writing programs in assembly when you can write them in C instead.
On the other hand, it is the case that I would trust Lean4 style proofs more than humanly written elegance-backed proofs. Which is why my compromise here is that perhaps both have their utility.
They definitely both have their validity. They probably each also make some results more salient than other results. I’d guess in the future there’ll be easier Lean tools than we currently have, which make the practice feel less like writing in Assembly. Either because of clever theorem construction, or outside tools like LLMs (if they don’t become generally intelligent, they should be able to fill in the stupid stuff pretty competently).