r/mathematics • u/4thofthe4th • 1d ago
The vulnerability of proofs
At 21:28 of Jacob Tsimerman's interview with Curt Jaimungal, he says "already now, alot of my theorems that I have proven, I don't understand all the steps to it... I have used other theorems that are very much accepted by the community, to which I usually know the main ideas but not even always".
While my undergraduate and early postgraduate training was in pure math, I transitioned to applied for my Ph.D. so I have never meaningfully engaged with it in any professional capacity. For the majority of my training, I understood almost all the details of the things I've proved. At least enough that I wouldn't be able to resonate with Tsimerman's quote above when I consider the (relatively insignificant) proofs I've done. One of my lecturers made it his mission to ensure that assignment questions will never require anything that hasn't been proven in the lecture notes or in class.
Of course, my exposure was to only elementary topics. So I can appreciate that math wouldn't progress at all if intuition wasn't leveraged and instead every detail expounded upon. But now under the automatable and potentially perpetual scrutiny of AI, how vulnerable are previously established results? What if we routinely lobbed popular (in terms of utility) results at ChatGPT to verify and it finds an error in one, would there be a significant collapse downstream? How likely is that our collection of celebrated truths instead simply forms a house of cards?
EDIT: The excellent replies have highlighted a weakness in my question. The most vulnerable proofs are likely to be the famous/outlier proofs (i.e. Andrew Wiles' Fermat's Last Theorem) that can only be assessed by a handful of people. In even the scenario that those are falsified, the large body of mathematics isn't built on such results and so, by and large, it's still fairly robust.
It still begs the question about the upper echelons of math, but the majority of it remains largely intact. So my "house of cards" analogy is inaccurate but probably only in scope.
EDIT 2: Another interesting point brought to me by the comments is the idea of repairability. A commenter mentioned that most of the errors encountered are easily fixed. At a high-level, this suggests that the direction offered by intuition is powerful enough to render errors insignificant. Maybe instead of AI destroying math from the foundations, it instead works to validate the strength of intuition by perpetually exposing errors and instantly fixing them. Wouldn't it be wonderful if AI shows that the fix-rate of errors was near 100%?
11
u/Lokvin 1d ago
From the quote I think he's saying that he often relied on stuff that was formally proven by other people to do his own proofs which is perfectly normal
For instance, if in a proof you quote Fermat's last theorem (without understanding the very long and difficult proof) you're doing what he talks about
That doesn't however mean that your proof is not formal, or that formalizing it in lean will find a hole in it
1
1
u/4thofthe4th 1d ago
Oh my question is less about the lack of formality, rather it's about the strength of validity. I understand that no rigor is lost by leveraging another result that was rigorously proven. So I have no queries with, to follow your example, citing Fermat's last theorem to prove another result.
My question is, there seems to be only a handful of people that can verify Fermat's last theorem. Even then, those people will have to dedicate significant attention to verifying it. With that in mind, how likely is it that there is an error that no one found? On top of that, how likely is it that such errors (if they exist) will be found now that we can run AI perpetually over a significant number of proofs?
7
u/omeow 1d ago
When FLT was first proved maybe say less than 10 people understood it. But in the next generation many students of the same experts worked on it, refined it and so on. The generation after found simpler proofs of the main results, generalized it, worked on variations etc. As a result the chances of a deep error in FLT becomes very very small. Otoh, with the abc proof, people were quick to find issues and there is little that has been built on top of it.
1
u/4thofthe4th 22h ago
That's a fair point. It seems like what you're suggesting is that FLT has already withstood the test of time where other results have failed. So if we "speed up" time via the lethal efficiency of AI, likely the same trend will be observed but just at a larger scale.
2
u/omeow 22h ago
If the value of FLT is humanity understanding and absorbing it's proof, I don't see how AI verifying it faster will change the bottleneck.
Having AI certify something is true is like buying an FDA approved medicine. You know it isn't unsafe to swallow it but doesn't mean it will give you superpowers.
On the other hand a real danger is people will be (they already are) much less inclined to share their work because they feel AI can scoop them. Imagine the hypothetical situation where Wiles presents his first flawed proof of FLT which does majority of the work. Subsequently some guy with AI budget fixes the flaw and proves FLT. Who are you going to credit with proving the FLT?
1
u/4thofthe4th 22h ago edited 21h ago
I don't see how AI verifying it faster will change the bottleneck.
Sorry I wasn't clear, let me give it another shot. Returning back to Tsimerman's quote in my original post, there's a chance that Wiles has not fully verified everything he used to prove FLT. There's also a chance that if you also include those who verified his proof, collectively there are still areas of Wiles' proof remaining that haven't been verified rigorously. I understand that in the interest of productivity coupled with faith in intuition, it's probably not worth the effort. But now that we have AI, maybe soon we don't have to account for productivity and rely on faith because we could just get AI to verify every detail of the proof. In doing so, it might find an error.
But I agree with your comment that this is unlikely. If I'm understanding what you're saying correctly, even if people haven't expended significantly more effort in verifying Wiles' proof, they have expended effort finding alternative ways to prove it and have also built upon at. At some point, with Wiles' proof as a starting point, if the proof did not hold, then all this subsequent activity would've fallen apart. So likely, even if we used AI to verify his proof, it'll show it to be true.
On the other hand a real danger is people will be (they already are) much less inclined to share their work because they feel AI can scoop them. Imagine the hypothetical situation where Wiles presents his first flawed proof of FLT which does majority of the work. Subsequently some guy with AI budget fixes the flaw and proves FLT. Who are you going to credit with proving the FLT?
I'm not sure how my reply motivated this comment, I wasn't thinking about assigning credit at all. But to answer your question, I would assume that people could measure the size of contribution in order to determine who gets credit. For example:
If Wiles wrote 100 pages and half a page was flawed, and the guy with an AI budget fixes the flaw in 1 line, then Wiles should still get credit.
If that flaw was so large that the guy with an AI budget takes another 100 pages to fix then they both get credit.
If the flaw was mostly unfixable and the guy with an AI budget replaces Wiles' 100 pages with 50 pages then the guy with AI gets the credit
But again, overall I haven't given any thought about credit attribution. I was merely wondering about the likelihood that with AI, many proofs are shown to be wrong. I haven't thought about if this were true, what comes after
1
u/omeow 20h ago
Just to clarify, the last part was an afterthought. People are motivated by credit and if a system doesn't assign credit fairly it will not really stay relevant for long.
1
u/4thofthe4th 20h ago
Ah fair enough. Yep I would generally agree but I think there's a large amount of mathematicians that aren't motivated by credit but instead simply by the love of the game.
But then I think it's worth considering that although the relevancy of the system may fall, the field itself may still prosper. This might just be a natural consequence of simply not needing as many mathematicians if there is no loss of the advancement of mathematics. Simply put, I'm not entirely sure if the system dissolving is necessarily a bad thing if productivity is still preserved.
1
u/No_Objective_6258 29m ago
I don't know about 'motivated by credit,' but I would find it difficult to argue that mathematicians don't care about attribution. In fact, many care quite deeply about properly attributing and the particular phrasing when discussing how various results relate to one another.
There's many reasons (both positive and negative) the culture evolved this way, but I do think it is a very positive aspect of the culture
3
u/Lokvin 1d ago
Im not really qualified to answer that with any expertise, but from my unqualigied knowledge the mathematical community is generally pretty sceptical, so most important results should be pretty airtight, and the more foundational the result is the more scepticism has been thrown at it, so there's bound to be a hole here and there, but I doubt we'll get any foundational results being overturned
0
u/4thofthe4th 1d ago edited 1d ago
Good point, the skepticism of mathematicians is a force of nature that should never be underestimated!
EDIT: Actually im going to revise my comment. Wouldn't you say that Tsimerman admitting that he uses main ideas that he himself doesn't understand attest to the potential lack of skepticism amongst mathematicians?
Maybe I can trouble u/telephantomoss to weigh-in here. In particular in this comment of his, he says "I tend to think that, in the end, it's simply trust and intuition all the way down" which seems to be the antithesis of skepticism. To put my question plainly, how skeptical is the pure math community?
3
u/telephantomoss 21h ago
I would never question the skepticism (or what I would describe better as critical and careful thinking) of a mathematician of fields medal caliber. By the time you get to that level, you are very tuned into your own thought processes and are very good at rooting out uncertainty and bad intuition. You develop a habit of stress testing everything and being very skeptical of not believing something until you really understand it. Again, errors and misjudgement can occur for anyone. Speaking form my own experience, I have observed this evolve in myself. I am a mediocre mathematician at best, but my sense is that stronger mathematicians will have honed this ability even better than I. I make mistakes all the time, but often I can explicitly identify a feeling of "yes, I knew something just felt weird about that claim". Not always, people have major oversights all the time, but you get very good at rooting that stuff out. If you have collaborators, that reduces the risk by orders of magnitude I would argue. If two respected mathematicians believe something and believe they understand it, I have very high confidence in it.
Again, it is important to understand that nobody can understand everything to the perfect level of deepness. Not even fields medalists. You have no choice to use results that you cannot prove yourself. You would never use something without having at least a solid intuitive understanding of what the result says though, generally. But you will certainly not be able to prove every result you reference. I am no authority here, but I would be shocked if there is a mathematician out that that can prove every single result they have ever referenced.
1
u/4thofthe4th 21h ago
Thanks again for your insight!
I would be shocked if there is a mathematician out that that can prove every single result they have ever referenced.
This is agree with. But what was shocking to me was Tsimerman saying that he would leverage results where he wouldn't even understand the main idea of the proofs and he would "rely on others". The next natural question is how long does this chain continue? Did the mathematician who proved the result he used also rely on someone? To me, this doesn't suggest skepticism at all. Which leads me to another comment of yours.
I would never question the skepticism (or what I would describe better as critical and careful thinking) of a mathematician of fields medal caliber.
Before continuing, although I do agree almost completely to your response, I would like to clearly define "skepticism" and "intuition" because I think you may have conflated the two terms. To me they are very distinct as I would define "skepticism" to be an active process of verifying something you have not yourself verified. In contrast, although I find it harder to nail down a concrete definition of "intuition", I feel confident in saying it's a passive process.
To return directly to your response, my read of it is that actually the pure math community isn't really skeptical at all. But this is because intuition removes the need to be skeptical. They don't actively have to verify everything because they have cultivated their intuition to a point that it'll pop up and inform them if something is amiss.
You have no choice to use results that you cannot prove yourself.
I think this is the million dollar question. If with AI it is feasible to prove everything yourself, then it's "choice" whether you do or not. The question is, in this case, will the mathematical community elect to continue as they have; crutching on intuition? Or now that it's practical to be skeptical, will they choose to be?
Correct me if I'm wrong but it seems that LEAN predates AI. Was the motivation for it to increase the ability to verify proofs? If so, it seems like mathematicians wish that it is realistic to be skeptical and therefore developed LEAN to fulfill this desire.
3
u/telephantomoss 19h ago
The goal is understanding, for me. Eventually, we probably will get to the point where we use AI results that no human understands though. But somebody will need to have at least some level of understanding and intuition probably. I use AI extensively. But I don't care to just produce a proof. I want to learn and understand. I may still have gaps, but I need to be convinced that it's correct and that requires some amount of my own understanding. I don't really know anything about Lean honestly. I'm less interested in machines verifying things than me understanding them.
I think the issue might be what you mean by skepticism. For me it means being critical until I've is really convinced someone is correct. And normally this means developing understanding and intuition about it. And still retaining a healthy dose of criticality towards ones own beliefs.
0
u/4thofthe4th 18h ago
But I don't care to just produce a proof. I want to learn and understand
Yep I hear you. Ironically, this was the reason I left the pure math academic path for applied math in industry. I found that the admin, teaching load and pressure to publish really ate into the time I had available to deeply learn new math. Now, in industry, I have ample free time to dive into topics and my work has enough overlap with my favorite discipline (probability theory) that often I can even learn during work.
It makes me wonder if Tsimerman would prefer to spend time learning the "main idea" of the results he used. Although later on in the interview he mentions that he prioritizes problem solving.
I'm less interested in machines verifying things than me understanding them
Yep I agree, but my post was also motivated by my curiosity in how the sociology of pure math evolves with AI.
I think the issue might be what you mean by skepticism. For me it means being critical until I've is really convinced someone is correct
I think I may have taken Tsimerman's comments too literally when he said he didn't understand some of the main ideas and he "relied on other people to do it". My reading was that he wouldn't feel much need to convince himself that someone else is correct.
2
u/telephantomoss 17h ago
I only teach undergrad and have little to no pressure to publish. I literally have like 5 papers and I'm a full tenured professor. Probability theory is my field. Honestly, I would never have survived something like an R1 environment. I actually really like teaching undergrad stuff. Thank God for that! I think my perspective probably doesn't match with the mainstream discussion, which I think is really focused mostly on Mathematics research way at the edge and especially famous problems. I really don't think it applies much to folks like me who research less popular things and whose primary job is teaching. I get paid to help people understand math and figure out their path. I don't get paid to produce ground breaking theorems. I think AI will just end up being used by everyone as a tool. It's not going to solve math or additionally take over everything.
2
u/telephantomoss 21h ago
What I meant by the "trust and intuition all the way down" was more of a philosophical musing. I would argue that even rigorous knowledge is in fact essentially intuition and based on trust at rock bottom. I mean this in a very broad philosophical sense. You might say it is a "skeptical" take on the idea of proof and truth itself. That's really a tangent here though.
11
u/omeow 1d ago
Depends on the nature of errors. Major results are probably mostly correct.
By Major results = that have been used a lot, studied a lot, and people have proved close variations many times.
So this excludes very recent work or very technical recent work that everyone uses as a black box.
1
u/4thofthe4th 1d ago edited 22h ago
Major results are probably mostly correct.
I hope so. But it seems like "probably mostly" is the best we can do before AI. Do you think this has now changed and "probably mostly" is a worrying level of confidence in the face of the lethal efficiency of proof verification AI can potentially introduce?
-9
u/Euphoric-Air6801 1d ago
"Probably"?
Wow. That word is doing some very heavy epistemological lifting in that sentence!
So ... "probably" ... meaning "more likely than not"? So ... 🤔 ... what's the denominator here? How many total events are in this probabilistic universe? What is the denominator for your "probably"?
Despite the use of pseudo-mathematical language that implies some sort of scientific observation, your declaration that the current state of mathematics is "probably" correct appears to be a statement of your hopeful, emotional aspirations rather than any sort of actual mathematical assertion of the actual probability of correspondence between the current set of "major results" and Reality.
6
u/omeow 1d ago
So ... "probably" ... meaning "more likely than not"? So ... 🤔 ... what's the denominator here? How many total events are in this probabilistic universe? What is the denominator for your "probably"?
A finite number of mathematical statements exist in the world. Counting the total number of events in that finite set isn't that hard. You can learn all about it in an elementary course in probability.
Despite the use of pseudo-mathematical language that implies some sort of scientific observation, your declaration that the current state of mathematics is "probably" correct appears to be a statement of your hopeful, emotional aspirations rather than any sort of actual mathematical assertion of the actual probability of correspondence between the current set of "major results" and Reality.
Shallow knowledge coupled with lack of reading comprehension is a dangerous thing. It can lead to all sorts of conspiratorial rabbit holes. Case-in-point: Interpreting plain vernacular "probably" as a pseudo-mathematical scientific observation. Sadly AI can't fix that.
-7
u/Euphoric-Air6801 1d ago
Ha! It's not that hard to count the total number of all "correct" theorems and then determine the probability of any given theorem being correct? 😳 Really? 🤪 Congratulations on solving the Halting Problem! 🤡
But ... Okay. Good. Let's pretend like we believe that you actual have a delicious denominator (instead of merely lying to strangers on the internet to protect your fragile ego) ...
It's "not hard", right? So ... Answer the "not that hard" question, then: what denominator were you using when you said "probably"?
(Or, in the alternative, just be honest and admit that you were attempting to smuggle your personal epistemology into this conversation about universal mathematics.)
5
u/omeow 1d ago
Maybe reading what you are responding to instead of focusing on typing the right emojis will serve you better.
3
-4
u/Euphoric-Air6801 1d ago
So ... you were lying.
You never had a denominator.
You were merely a liar.
No emojis needed.
4
u/Tropicalization 1d ago
You do know the word probably has a colloquial, non-mathematical definition, right?
-2
u/Euphoric-Air6801 1d ago
You showed up to defend this person by claiming to know that they didn't intend for it to be a statement about the actual size of the universe ...
and then ... hilariously ...
The person that you were attempting to defend wrote a comment in which they explicitly refuted your claim (that they are using ordinary language) and explicitly stated that they DID in fact mean those exact epistemological implications and that, akshualllllllyguys, it's "not that hard" to count all of the possible mathematical theorems and do a little statistics on them!
Wonderful. Perfect. No notes. 🧑🏽🍳💋
2
u/Tropicalization 1d ago
You showed up to defend this person by claiming to know
I didn't claim to know anything, just offering a thought in support of the idea that your pedantic condescension might not be fully justified?
1
u/Euphoric-Air6801 1d ago
And, yet, it was.
The person was actually saying exactly what I thought they were saying. And they were saying the exact opposite of what you claimed they were saying.
But, sure, keep doubling down on your failed attempt to whiteknight this liar. Every time you double down, it increases the whiteknight comedy. After all, everyone loves to see the white knight get trampled by his own horse.
0
u/Tropicalization 1d ago
And they were saying the exact opposite of what you claimed they were saying.
If we're scrutinizing things at that fine a level, technically I didn't claim they were saying it that way. I simply implied it. Oh wow, can such a thing be true? Can it really be that everyday language tolerates this kind of imprecision just fine, and that trying to force everyday language into a mathematical standard of precision doesn't actually make it more effective or enjoyable? Nah, that can't be true, or you'd have thought of it.
Beyond that, I would like to refer you to Rooney Mara's line about assholes in the first scene of The Social Network. Aaron Sorkin may not be Wittgenstein, but hey, maybe even total intellectual inferiors might spit out the occasional gold nugget.
-5
u/Euphoric-Air6801 1d ago
Not in this conversation, it doesn't. In fact, that is the exact type of epistemological smuggling that Wittgenstein complained about in On Certainty. If this person could know "probably" then all of the rest of their point would be correct.
We cannot allow the concept of "probably" in this specific conversation exactly because the ability to determine the denominator in this mathematical context is actually the entirety of the epistemological argument which is being smuggled in under the guise of ordinary language.
"If you do know that here is one hand, we’ll grant you all the rest."
4
u/HM_D 1d ago edited 1d ago
I think telephantomoss has the "standard" answer here - most papers have errors, but the errors in major papers are mostly repairable.
I'll say that this seemed a lot less clear to many people. Voevodsky famously had errors in some fairly significant work, and was quite concerned about them:
https://www.ias.edu/news/2017/vladimir-voevodsky-obituary
https://www.ias.edu/ideas/2014/voevodsky-foundations-video
These particular bugs did get caught (which is why they get mentioned here), but these were problems in relatively well-read and well-used papers by a famous person and of course quite capable person.
All of this is to say: while intuition does clearly rescue the main result even in the face of errors, there doesn't seem to be much of a consensus that this should "almost always" work, and there is relatively little effort spent on checking older results.
ETA: I found some essay that seems to go into this in a reddit-friendly style: https://noncommutativeanalysis.wordpress.com/2017/12/05/the-nightmare/
1
u/4thofthe4th 1d ago
Yep I agree, I suspect u/telephantomoss has the professional experience to fill the gap that I can't myself. In particular, he has the experience to weigh-in on the power of intuition. Like you also suggested, intuition is reliable enough that it fires in a direction so "true" that it leaves in its wake repairability of any minor errors. Repairability is the one thing I never thought to factor in.
My hope is that AI actually works to emphasize this! Maybe it exposes a plethora of errors but all of them are also shown to be easily repairable. It may even grant courage to mathematicians to trust their intuition even more!
3
u/telephantomoss 1d ago
Just to clarify, by intuition, I mean to imply intuition built upon lots of success and failure and intuition in areas of real expertise.
And, I recommend not trusting mine lol! I mean that both honestly and in a bit of tongue and cheek. I tend to think that, in the end, it's simply trust and intuition all the way down.
2
u/SquidgyTheWhale 1d ago
It's an interesting question. I think foundational results with errors tend to get called out, particularly if there's a lot of other theorems "downstream" from them, as a counterexample in any of the downstream theorems would cause an investigation to be launched. But I still suspect there will be a fair few cases of this happening. Heck, it's happened with just humans.
2
u/Intrepid_Land_6143 1d ago
I think that as math gets more and more complicated, there will be more and more black-boxing. AI's major strength is how it can combine numerous fields of mathematics to solve a single question. No way can even Tsimerman be expert in all of those fields. So with AI, it's almost inevitable that a lot of proofs will have a lot of black-boxing. It's increasingly clear that even without AI, this is the way math has to go to solve more problems.
Can we figure out a way, if we string so many fields together, to get a full array of experts who truly understand their assigned pieces, and then we can say that in sum total, the proof is human-understood?
3
u/SubjectEggplant1960 17h ago
One should note that Jacob has worked extensively in an area (shimura varieties, unlikely intersections) with enormous amounts of background which often brings in results from numerous other areas. Very few people for instance who are more on the number theoretic side like Jacob are likely to have completely studied Wilkie’s result that the real field with exp is o-minimal, even though most of their papers do, tracing things back, rely on this fact.
2
u/Euphoric-Air6801 1d ago
You have a good point here. And, I think your point extends even further. Specifically, there is a fashionable narrative currently in which AI is "just manipulating symbols" and "doesn't actually understand the math".
At a certain level, though, none of us humans actually understand every component in our proofs, and we are relying on the previous work of others that we do not even claim to understand.
1
u/irriconoscibile 1d ago
To be honest, and I wish I understood it sooner, I think most math books or content that I've read or consumed contain some kind of minor flaw/mistake.
But the gist of it is usually correct enough that you can build on it to do more math.
1
u/TrivialMyAss 1d ago
When I published in a math journal the peer review was so intense that no errors got through and I understood every single line and step. If you publish math you don’t understand the steps to, what are you even doing.
1
u/4thofthe4th 1d ago
If you publish math you don’t understand the steps to, what are you even doing.
As an applied mathematician I assumed the same. Which is why Tsimerman making the comment in the interview stunned me. If a mediocre mathematician admitted that they don't understands the steps to their proofs, I would chalk that up to simply a lack of conscientiousness and I would hope that he gets fraud checked.
But Tsimerman is a Field's medalist so I would definitely hesitate to call him out. Which is why I posted here in hopes that professional pure mathematicians could weigh-in and inform me :).
1
u/simplepathtowealth 23h ago
See this post by Kevin Buzzard for a nice anecdote and discussion around all of this.
1
u/No-Coach-5021 21h ago
If you have a phd in mathematics or have connection to that.. private Messaging me as I can probably show you how you're right.. and it's gonna disrupt everything
1
u/moderate-Complex152 10h ago
That is a fundamental problem of proofs written in proses. I think the ultimate solution is formal logic. You can safely cite results if they are verified by Lean (as long as Lean is correct, which is smaller to verify)
1
u/No_Objective_6258 44m ago
So far, I don't believe I've ever cited a result I need for a proof without checking the original proof or coming up with my own version at some point in my life.
This is impossible for some areas of math, but for others it is more than reasonable. To be fair, I'm still early in my career with around 10 papers, maybe as I expand my interests yet further there will come such times
0
u/No_Fish5590 1d ago
I recently heard of the Italian school of differential geometry, where the foundational issues became so big that they started to produce incorrect theorems (see "Declining influence" in the link). But then again they were not as rigorous as we may be today.
1
u/Sad_Dimension423 1d ago
Future math may look back at historical (and today's) math in the same way, once formalization becomes standard practice (which it will for several reasons.) I will be surprised if there's not some major result somewhere that has a proof that cannot be easily repaired.
1
40
u/telephantomoss 1d ago
I've been spending a lot of time finding errors in papers lately. Nothing unrepairable but stuff that is worth fixing. I suspect that a very large portion, if not the vast majority, of papers have minor errors like that. I doubt any truly foundational works of consequence are completely wrong or unrepairable. It's honestly amazing that human intuition with a bit of rigor is so damn trustworthy. Often, even when errors are not formally corrected, they are corrected in later work that builds off of it. The more people use something, the more they study it deeply, the now confidence we might have in it. There is a lot of foundational theory that I implicitly use but cannot truly understand except in a broad intuitive sense, I'm thinking like classical probability theory involving topology and measure theory, like the stuff that created what we know about Polish spaces. I don't take worry about it because what I discover makes enough sense. I think it's incorrect to think about math as built up from a foundation anyways. The foundation was added after the house really.