Most likely place for an error?

Stream: FLT

[Mr Proof]

Hello. Just wondered, from your experience formalising the proof so far. What percent chance do you think that Wiles' proof is correct. And if there were to be a potential error in the proof which part of the proof is it most likely to be in? Probably a part of the proof which has to prove lots of individual cases I bet and then one case gets through the net.

[Kevin Buzzard]

99.99% and nowhere, is my personal opinion on this.

[Mr Proof]

In that case I will bet you $1 at odds 5000:1 that there is an error. If you complete the proof and there is no error you get $1. Can't say fairer than that.

[Ruben Van de Velde]

We're not formalising Wiles's proof, so how would we know?

[Mr Proof]

Hmm... in the sense that if you replace every part of a car it's not the same car?

[Ruben Van de Velde]

I think that was a ship

[Johan Commelin]

If you replace every part of a ship, it might become a car? :see_no_evil:

[Ruben Van de Velde]

Maybe if you're James Bond?

[Kevin Buzzard]

Mr Proof said:

Hmm... in the sense that if you replace every part of a car it's not the same car?

No. We're formalising a different proof to Wiles' proof.

[Patrick Massot]

A much more fundamental issue is such a bet would be meaningless without defining the word “error”.

[Nikolay Ulyanov]

But the error has already been found (and repaired) like in 1993 or something!
https://www.reddit.com/r/math/comments/18lf8ji/who_were_the_referees_who_discovered_the_error_in/
https://mathoverflow.net/questions/488143/wiless-original-proof-for-fermats-last-theorem

[Kevin Buzzard]

An error in the 1993 proof was discovered by one of the referees, but the 1994 Wiles/Taylor--Wiles proof is also fine.

[Ruben Van de Velde]

Anyway, shouldn't you be holidaying (or writing blueprints)? :)

[Kevin Buzzard]

I should be holidaying (or preparing a class field theory workshop). Normal FLT service will be resumed in about 10 days.

[Mr Proof]

@Patrick Massot I was thinking in the sense of finding one of the lemmas on which the proof rests was not true. There could be another case in which a lemma is not proved to be false but was found to not be not provable by the techniques outlined in the literature. Since it can't be proved to be false, we'd have to add a time constraint to the proof as a whole - shall we say 5 years? :thinking:

[Patrick Massot]

This is still too naive. A lemma being not true is also not well define. More precisely the obvious definition is irrelevant.

[Michael Rothgang]

For instance, would you count the error in Roby's work discovered by Antoine Chambert-Loir and Maria Inés de Frutos Fernandez in your definition? A lemma was definitely false, but the overall result (a background theorem for the FLT proof) was definitely true, and has a new proof now.

[Michael Rothgang]

(Though, I understand, the new proof was be more involved than this post may make it seem.)

[Mr Proof]

@Michael Rothgang Exactly. That's why there would have to be a time limit. Since small lemmas could be false or not fully proven by the methods laid out in papers but be simply patched which we should give a certain amount of lee way.

However, if there was a lemma essential to the poof that was not provable by the methods stated in the literature and not able to be patched within the 5 years I think we can safely say, that the proof is in error. (Which doesn't mean FLT is false, just unproven so far). This is in the same sense as the first error was found in Wile's original proof.

@Patrick Massot Yes, let's be precise here. A lemma essential to the proof whose definition is formalised in lean can indeed be proved within lean to be false. Perhaps you are thinking of a lemma in a more colloquial sense?

[Michael Rothgang]

I'm still somewhat confused about your notion of error. Is the above lemma "essential to the proof" --- assuming for the sake of discussion that it's a background theorem for FLT (in particular, not parts of Wiles and Taylor's work), but every known proof crucially uses it? Must the error be in work of Wiles and Taylor?

[Michael Rothgang]

So you are saying "minor errors are fine", where minor includes everything that can be patched within five year. I see.

[David Michael Roberts]

How about things like claims that are made without proof, because they are seen to be obvious? Are they holes?

[Riccardo Brasca]

I don't want to enter into the discussion about Wiles' proof, but I recommend "What is mathematical rigor?" by John Burgess and Silvia De Toffoli as in interesting reading about... well, what is mathematical rigor.

[David Michael Roberts]

Did Gaitsgory et al "really" finish proving their big geometric Langlands theorem when they didn't prove some technical claims in their background material which have taken others a decade to prove, and only just this month released the proof of the last one?

[Mr Proof]

@David Michael Roberts Yes, I think they would definitely count as holes. Since things that seem obvious sometimes turn out either not to be so, or actually not true at all, especially if the proof to patch them turns out to be long.

I think the one that springs to mind is “All smooth structures on R^4 are diffeomorphic to the standard one.” Seems pretty obvious... until it was disproved in the 1980's.

@David Michael Roberts In my opinion no. What they did was laid the framework and it was only proved when the final pieces were in place. The last person to put the piece in the jigsaw is the person who solved the jigsaw even if someone else did 99% of it. That's my opinion. Just because the last 1% is "easy" doesn't make any difference. But still I would give the Fields medal to the one who did the 99% :blush:. But if there was a prize for solving the proof then it goes to the person who did the 1% on the finish line.

[Oliver Nash]

I’m reluctant to join this thread but I might just say that the claim about fake R4 doesn’t fit with my memory. I am not aware of any source claiming the non-existence of a fake R^4, even though the proof of their existence was a major surprise.

[Mr Proof]

Why would you claim the non-existence of something you had no idea existed in the first place? :thinking:
People also didn't claim the non-existence of the Azure-thighed tree frog :frog: until it was discovered in 2023.

OK, I'll adjust my dates and say, before 1956, the idea seemed obvious. But it's not that important.

[Mario Carneiro]

Why would you claim the non-existence of something you had no idea existed in the first place? :thinking:

Isn't that the main reason you would claim its nonexistence? It's pretty natural to conjecture a partial classification you have at the moment is complete

[Mario Carneiro]

e.g. with the kepler conjecture: "I have this packing here and it looks pretty good, I tried a few things and couldn't find a better one, so maybe it's the best?"

[Alex Meiburg]

I just noticed this thread (sorry for necro) and thought it was entertaining. As a sort of repetition of the above:papers are often full of "errors" where a lemma or claim isn't true as written, but just because it omits some "obvious" condition that no one would typically care about.

A very common one I encounter in my work is, in the context of linear algebra, that some lemma only holds when a vector space (esp. a Hilbert space) has nonzero dimension. Or, maybe the lemma holds, but the proof says something like "take any nonzero vector v..." which you guaranteed to have -- but then the zero-dimensional case is trivial. Is this an error? For someone translating into Lean, maybe. For someone refereeing a paper or editing a textbook, absolutely not.

As another quibble, what if a paper starts by stating that they're presenting partial progress on a well-known, named open problem in commutative ring theory, they start with some motivating examples from reals and from integer polynomials, but then they use "ring" throughout instead of ever specifying "commutative ring" (and indeed many of their theorems rely on this fact). It would be fair to say that such a paper would be _improved_ by adding a sentence such as, "We assume all rings are commutative throughout the paper." near the top of the paper, but I certainly wouldn't say the paper was full of _errors_.

Anyway, I'm curious: let's say, very generously, that these imprecisions in natural language would fall under an umbrella of "errors", where the most literal and minimal-context translation of the English to Lean could render it incorrect.

What is the "largest error" you would expect to encounter in formalizing FLT? Or, what's the largest you've found so far? I'm sure there's been at least one case of an author being slightly loose with their language (without being 'wrong').

[Ruben Van de Velde]

The biggest error is that the last few hundred years of mathematicians have been writing prose rather than lean, clearly :)

[Johan Commelin]

Yeah, I still think it's really crazy that Fermat used a margin comment to state his theorem conjecture, instead of a git commit message!

[Ruben Van de Velde]

To be fair, his metatheorem that the proof didn't fit in the margin seems to be true

[Kevin Buzzard]

Alex Meiburg said:

What is the "largest error" you would expect to encounter in formalizing FLT? Or, what's the largest you've found so far?

I don't expect to find any serious errors, although I was surprised about the error discovered in the original foundational paper on divided powers (which was fixed elsewhere in the literature in the sense that someone else gave a new proof which wasn't wrong, but they didn't notice the original proof was wrong).

[Mr Proof]

Can I ask another question:
Once the FLT has been formalised. Using all the tools and lemmas built up for this task. Are there any other well known proofs that can then be easily formalised using these tools and lemmas? Or are there even some proofs tangential to FLT that people are proving along the way using the tools built up for the FLT project.

Thanks.

[Kevin Buzzard]

There are plenty of other proofs that can then be formalised, that's the point, although it will not be "easy" to formalise any of them and it would be hard to class any of them as "well known". We will be proving stronger results than what was originally proved in the Wiles/Taylor--Wiles papers but it is not possible to explain what we're strengthening to a non-expert, the strengthenings are statements in the Langlands program rather than claims of an elementary Diophantine nature. Remember, Wiles did not prove Fermat's Last Theorem; he proved the semistable Shimura-Taniyama conjecture. The fact that FLT followed as a consequence was an earlier theorem of Ribet.

[Ryan Smith]

I suppose a natural generalization would be the full modularity theorem. Not sure I'd call that a small or easy next step.

Have there been any significant simplifications since the original paper from Breuil-Conrad-Diamond-Taylor? I've been out of the loop.

[Kevin Buzzard]

Yes sure, Serre's conjecture has been proved by Khare and Wintenberger so you don't have to get your hands dirty at 3 any more

[Ryan Smith]

I do know about that part. This is just an opinion question, but would you say that Khare-Winterberger is a small or easy next step? Maybe I'm not remembering how many additional dependencies BCDT has compared to FLT, but Khare-Winterberger needs a bunch of stuff which isn't in the FLT roadmap I thought?

[Kevin Buzzard]

Actually we're doing a bunch of K-W stuff on the route

[Alex Meiburg]

For whatever it's worth, over at https://github.com/Timeroot/Lean-QuantumInfo we've been formalizing an important paper from quantum information (the generalized quantum stein's lemma) and we recently found an error -- albeit a small one. For anyone curious:

• There's a "gap" between two quantities R1 and R2, you know that R1 <= R2, but you want to show that they're actually equal. R2 is defined as an infimum over some structure σ, so this is really a problem of finding a σ that makes it tight.
• They prove that there's a rather complicated procedure to take σ and produce a new σ', with a gap that is at most 1 - ε times as big. (The parameter ε depends on some other variables in the context of the problem, but not on σ.)
• So, they say, this means you can keep shrinking the gap arbitrarily small, so the gap must be zero. So - and I quote - "you start with any arbitrary σ, and this procedure [succeeds]".

This doesn't quite suffice, because R1 and R2 are _extended_ reals, and for generic choices of initial σ, the starting gap is infinite. This problem was found only during formalization. I initially had in fact written let σ := Exists.choose [...], and then it was only a couple weeks later that I got stuck ruling out infinite cases that this was caught.

In the context of the paper, it's very obvious (and only ~4 lines of Lean) to see why there's a valid finite starting case. It's small enough that I wouldn't even count it as an error (and merely a "didn't feel the need to write down explicitly" issue), if it wasn't for the particular claim that an arbitrary start works.

This is the scale of "error" that I would be curious about!