7 ms·

"The proof is not the modern proof which I have been formalizing myself following ideas of Khare, Taylor etc, but the Darmon–Diamond–Taylor exposition from 1995

by glimshe 12d ago

"The proof is not the modern proof which I have been formalizing myself following ideas of Khare, Taylor etc, but the Darmon–Diamond–Taylor exposition from 1995 of the Wiles–Taylor–Wiles argument, via the Langlands–Tunnell theorem and Ribet’s level-lowering theorem. Anthropic’s repository develops Fontaine theory (to study flat deformations of Galois representations) and develops enough of Mazur’s work on the Eisenstein ideal to conclude that no Frey curve can have a point of order p>=17. This means that their FLT proof only works for p>=17, however FLT was already formalized for odd regular primes by Best-Birkbeck-Brasca-Rodriguez, and the smallest irregular prime is 37, so it’s all good." My question to any mathematician reading this: does the above make ANY sense to you? I ask that because I can read most technical material related to computer engineering, programming, hardware specifications etc. Even if I don't fully understand all details, I can follow them pretty well. So I wonder if professional mathematicians can look at the above and still make sense of it like experienced software engineers do for computer stuff.

jovas 12d ago
Yes, I'm a mathematician. But not an expert on this. While I don't know the specifics, and someone more "in-the-field" than me would recognize all the "named" theorems etc I am aware that there have been minor issues that have come up with the formalization specifically, and that previous proofs for lower values of n were always needed. Though it used to be n=5 and lower needed to be checked.
CogDisco 12d ago
Yep. While I'm not focussed on these areas, I know enough from scoping out a "learn about the proof of FLT" course that it's covering all the usual suspects and says the right-enough words. Patching their weaker results with someone else's seem like a good strategy (and I could find the result on arXiv so it isn't obviously hallucinated). This is very different to believing the proof, which would require at least a pass understanding the general approach, seeing that it all actually fits together, then going deeper. At some point you transition to relying on the Lean all hanging together, but as mathematicians we all draw that line somewhere. But yeah, makes sense. Same thing if you saw news on someone's new database technique to improve performance. If they say the right words, don't say the wrong words, and if you cared enough you'd do spot checks proportional to the claim. If pressed you'd examine the source code, and run independent checks. But if smells roughly right, that's a good first approximation.
zmgsabst 12d ago
I did an undergrad in math with a little research in number theory and recognized parts — eg, I myself worked through the proof for odd regular primes and that 37 is irregular, breaking the general case. Wiles-Taylor-Wiles was the original proof by Andrew Wiles, and its corrections. Galois representations is about vectors over Galois extensions, which are essentially adding roots to regular numbers (rationals, integers, etc). That ties into the Langlands program, which is a big area in number theory (that I don’t know much about). Together with flat deformations and Frey curve, I think they’re talking about a topic in algebraic geometry as applied to number theory. I also recognize the name Eisenstein from my time as an undergrad, though two decades out and not working in the field I’ve forgotten what his work on ideals implied here. Ideals are a well-known topic though, a sort of structure inside a ring (set with + and *) that is closed under operations — like evens in the integers are the 2Z ideal. So I’d describe it as “sensible with an undergrad background”.
- atombender 12d ago
  About the Langlands program, Nunberphile has an excellent episode with Edward Frenkel explaining what it's about: https://youtu.be/4dyytPboqvE https://youtu.be/4dyytPboqvE.
  - auntienomen 12d ago
    Frenkel does a nice job explaining the Langlands program in general. But Buzzard's complaint about Langlands, I believe, refers specifically to the proof of a version of the Geometric Langlands Conjecture by Gaitsgory et al. The proo f is of order thousand pages of mathematical text and builds off of thousands of pages of higher-categorical algebraic geometry by Lurie & others. It's a ripe target for formalization because it's terrifically complicated, not well understood or thoroughly digested yet, and relatively important. A formal proof would be reassuring to mathematicians, whereas Fermat's Last Theorem is relatively unique in that so many mathematicians have examined the proof that it's not very likely to be wrong.
LanceH 12d ago
It's something you would have to be keeping up with as a mathematician, really. Vaguely. It's describing connections between a number of other mathematics results than can be connected to prove FLT. I assume all the work described is being done to make the proof more presentable, smaller, basically "prettier". It sounds like they established a minimum and maximum bounds for n in x^n + y^n = z^n, where one proof works for n greater than or equal to 17, and another proof for n < 37 (when prime). I believe the case (remembering back 40 years here) n is even is very easy, and n is composite and odd slightly less so. Neither really being in the ballpark of what they describe here.
UltraSane 12d ago
advanced math like this takes 10 years to learn all the tower of things it is based on.
- hackandthink 12d ago
  if you are a fast learner
jibal 12d ago
I'm not a mathematician and I don't see the problem, at all.
skipants 12d ago
Funnily enough, this is more readable to me than most Clayde jargon.
mathisfun123 12d ago
This question gets asked every single time a serious mathematical result gets posted.
contubernio 11d ago
As a mathematician not expert kn these things, yes it scans as reasonable, and yes it has me and most of my colleagues reconsidering what we do for a living.
- YeGoblynQueenne 11d ago
  Well, if I were a mathematician, what I'd be noodling about with right now is a way to model the number of failed attempts that AI companies must be making for every success they report. I guess you don't have to be a mathematician to do that sort of calculation, but I'm just proposing it as a way to lift mathematicians' spirits a bit. Also pay attention to the fact that every time a new model is released there's a slew of new results and then they dry out for a while, which suggests a "throw stuff at the wall and keep what sticks" approach that's incompatible with a kind of system that can just magickally solve all maths right now. I'm saying that because I get the feeling that mathematicians don't have a good model for the true capabilities of those systems and that can lead to an overreaction, like "woe is me, all of mathematics will be solved and my entire discipline will be rendered obsolete". Coming from an AI background I don't think that's right. I think because mathematicians are not AI researchers they simply don't have a very clear idea of what's going on with those systems. And tbf even many AI researchers (the ones who don't enjoy the benefits of a long tradition that goes back to the 1950's and basically only joined the field in the last 10 years or so) don't understand those systems very well either. Bottom line: don't panic. Or, not yet :0)
  - contubernio 10d ago
    Nobody is in panic, but we are using these systems and seeing what are their capabilities and it's clear that their use has a big impact on the practice of mathematical research, probably far more impact than it has in other areas. Part of mathematics involves classifying structures - think of describing combinatorial objects - and this is a sort of game with which a well directed AI tool can be very effective. Part of mathematics involves being able to bring to bear on a problem a diversity of techniques, and AI is also very helpful in this regard. The point is that people who spend their time classifying nilpotent Lie groups that admit structure X are out of work if they don't change their perspective. Maybe such problems were never really that interesting, although it was useful to have a group of people acting as human computers to work them out - but well used AI yields for such problems more complete and more reliable results - and so allows researchers to spend their time on other more interesting things. The problem for your run of the mill professional mathematician is that more interesting things are harder ...

by glimshe 12d ago

jovas 12d ago

Yes, I'm a mathematician. But not an expert on this. While I don't know the specifics, and someone more "in-the-field" than me would recognize all the "named" theorems etc I am aware that there have been minor issues that have come up with the formalization specifically, and that previous proofs for lower values of n were always needed. Though it used to be n=5 and lower needed to be checked.

CogDisco 12d ago

Yep. While I'm not focussed on these areas, I know enough from scoping out a "learn about the proof of FLT" course that it's covering all the usual suspects and says the right-enough words. Patching their weaker results with someone else's seem like a good strategy (and I could find the result on arXiv so it isn't obviously hallucinated). This is very different to believing the proof, which would require at least a pass understanding the general approach, seeing that it all actually fits together, then going deeper. At some point you transition to relying on the Lean all hanging together, but as mathematicians we all draw that line somewhere. But yeah, makes sense. Same thing if you saw news on someone's new database technique to improve performance. If they say the right words, don't say the wrong words, and if you cared enough you'd do spot checks proportional to the claim. If pressed you'd examine the source code, and run independent checks. But if smells roughly right, that's a good first approximation.

zmgsabst 12d ago

I did an undergrad in math with a little research in number theory and recognized parts — eg, I myself worked through the proof for odd regular primes and that 37 is irregular, breaking the general case. Wiles-Taylor-Wiles was the original proof by Andrew Wiles, and its corrections. Galois representations is about vectors over Galois extensions, which are essentially adding roots to regular numbers (rationals, integers, etc). That ties into the Langlands program, which is a big area in number theory (that I don’t know much about). Together with flat deformations and Frey curve, I think they’re talking about a topic in algebraic geometry as applied to number theory. I also recognize the name Eisenstein from my time as an undergrad, though two decades out and not working in the field I’ve forgotten what his work on ideals implied here. Ideals are a well-known topic though, a sort of structure inside a ring (set with + and *) that is closed under operations — like evens in the integers are the 2Z ideal. So I’d describe it as “sensible with an undergrad background”.

atombender 12d ago
About the Langlands program, Nunberphile has an excellent episode with Edward Frenkel explaining what it's about: https://youtu.be/4dyytPboqvE https://youtu.be/4dyytPboqvE.
- auntienomen 12d ago
  Frenkel does a nice job explaining the Langlands program in general. But Buzzard's complaint about Langlands, I believe, refers specifically to the proof of a version of the Geometric Langlands Conjecture by Gaitsgory et al. The proo f is of order thousand pages of mathematical text and builds off of thousands of pages of higher-categorical algebraic geometry by Lurie & others. It's a ripe target for formalization because it's terrifically complicated, not well understood or thoroughly digested yet, and relatively important. A formal proof would be reassuring to mathematicians, whereas Fermat's Last Theorem is relatively unique in that so many mathematicians have examined the proof that it's not very likely to be wrong.

LanceH 12d ago

It's something you would have to be keeping up with as a mathematician, really. Vaguely. It's describing connections between a number of other mathematics results than can be connected to prove FLT. I assume all the work described is being done to make the proof more presentable, smaller, basically "prettier". It sounds like they established a minimum and maximum bounds for n in x^n + y^n = z^n, where one proof works for n greater than or equal to 17, and another proof for n < 37 (when prime). I believe the case (remembering back 40 years here) n is even is very easy, and n is composite and odd slightly less so. Neither really being in the ballpark of what they describe here.

UltraSane 12d ago

advanced math like this takes 10 years to learn all the tower of things it is based on.

hackandthink 12d ago
if you are a fast learner

jibal 12d ago

I'm not a mathematician and I don't see the problem, at all.

skipants 12d ago

Funnily enough, this is more readable to me than most Clayde jargon.

mathisfun123 12d ago

This question gets asked every single time a serious mathematical result gets posted.

contubernio 11d ago

As a mathematician not expert kn these things, yes it scans as reasonable, and yes it has me and most of my colleagues reconsidering what we do for a living.

YeGoblynQueenne 11d ago
Well, if I were a mathematician, what I'd be noodling about with right now is a way to model the number of failed attempts that AI companies must be making for every success they report. I guess you don't have to be a mathematician to do that sort of calculation, but I'm just proposing it as a way to lift mathematicians' spirits a bit. Also pay attention to the fact that every time a new model is released there's a slew of new results and then they dry out for a while, which suggests a "throw stuff at the wall and keep what sticks" approach that's incompatible with a kind of system that can just magickally solve all maths right now. I'm saying that because I get the feeling that mathematicians don't have a good model for the true capabilities of those systems and that can lead to an overreaction, like "woe is me, all of mathematics will be solved and my entire discipline will be rendered obsolete". Coming from an AI background I don't think that's right. I think because mathematicians are not AI researchers they simply don't have a very clear idea of what's going on with those systems. And tbf even many AI researchers (the ones who don't enjoy the benefits of a long tradition that goes back to the 1950's and basically only joined the field in the last 10 years or so) don't understand those systems very well either. Bottom line: don't panic. Or, not yet :0)
- contubernio 10d ago
  Nobody is in panic, but we are using these systems and seeing what are their capabilities and it's clear that their use has a big impact on the practice of mathematical research, probably far more impact than it has in other areas. Part of mathematics involves classifying structures - think of describing combinatorial objects - and this is a sort of game with which a well directed AI tool can be very effective. Part of mathematics involves being able to bring to bear on a problem a diversity of techniques, and AI is also very helpful in this regard. The point is that people who spend their time classifying nilpotent Lie groups that admit structure X are out of work if they don't change their perspective. Maybe such problems were never really that interesting, although it was useful to have a group of people acting as human computers to work them out - but well used AI yields for such problems more complete and more reliable results - and so allows researchers to spend their time on other more interesting things. The problem for your run of the mill professional mathematician is that more interesting things are harder ...