5 ms·

The Fermat's Last Theorem Project

75 points by happa 2y ago

levn11 2y ago
https://www.techrxiv.org/users/717330/articles/702287-on-fermat-s-last-theorem https://www.techrxiv.org/users/717330/articles/702287-on-fer...
- voldacar 2y ago
  Why post this? This appears to be the writings of a crank.
  - levn11 2y ago
    which part
    - n4r9 2y ago
      On p.4 you argue that for integers a, b, c and n: (a + b − c)^n = (c − a)(c − b)g_1(n) => a + b − c = [(c − a)(c − b)g_1(n)]^(1/n) => g_1(n) | a + b - c This doesn't follow as it stands. For example, if a=b=3 and c=n=2, then g_1(n)=16 whereas a + b - c = 4.
    - voldacar 2y ago
      The part in which FLT is derived from the binomial theorem, lol.
      - hughesjj 2y ago
        Nah not derived, set equal to from the outset with essentially no explanatory test throughout but with enough effort to insert some arbitrary graphs and label them with 'hey neato look at the vibes'
        voldacar 2y ago
        My favorite part is "The derivative resembles the rhythm of a heartbeat."
- n4r9 2y ago
  This would definitely benefit from a bit more explanatory text as I'm struggling to understand what you've shown. The crux seems to be that if a^n+b^n=c^n then (c-a)(c-b) divides (a+b-c)^n. I haven't been through all the details of this, but I also don't see how that implies FLT.
  - hughesjj 2y ago
    If I'm not mistaken Fermat's last theroem isn't even featured in the proof. Like nowhere did I see a^n+b^n=c^n referenced in the proof,save for the end of page 1 and 3, but it's never featured in an equality. Just 'this implies this trust me bro'.
    - n4r9 2y ago
      I've actually had another quick look and I now have a vague idea of the outline. It's an attempted proof by contradiction, where a solution to FLT is applied to the binomial theorem and some arguments about integrality are made to form a contradiction. My issue at the moment is with a line at the bottom of p.4, which effectively says that if k^n = xy for integers k, n, x, y, then k must be a multiple of y. Unless I'm missing something this is clearly false, for example 2^4 = 4 x 4.
rndnumthy 2y ago
What I really like is that this project will not blindly formalize the proof from the 90's. Instead they take a SOTA approach, streamlining and optimizing many parts of the proof. So it will result in a useful artifact for modern number theorists.
- Pet_Ant 2y ago
  SOTA?
  - lightspot21 2y ago
    SOTA = state of the art
rndnumthy 2y ago
PDF slides from the talk where the project was launched: https://math.mit.edu/~drew/vantage/BuzzardSlides.pdf https://math.mit.edu/~drew/vantage/BuzzardSlides.pdf
mehulashah 2y ago
I wonder if after all that work, we might automatically reduce the proof and discover a simpler one that could have been included in the “margin”.
- ultrablack 2y ago
  I was just about to post my proof, but it didnt fit on Twitter :)
- kevinbuzzard 2y ago
  I highly doubt that the proof will get small enough to fit into a margin, but history shows that it's not at all unreasonable to expect simplifications/generalisations of the argument to come out of a formalisation (for example this happened with the Liquid Tensor Experiment, where dependence on stable homotopy groups of sphere was completely removed from the argument). I think it is unreasonable to expect that at the end of an FLT formalisation there will be no mention of elliptic curves, modular forms, Galois representations etc (the standard tools used by Wiles to prove the result in the 90s and which have themselves been simplified and generalised by mathematicians such as Taylor and Kisin since then). And you'll need quite a big margin to get all that stuff in.
- downboots 2y ago
  perhaps it was a veiled suggestion to use infinity in the proof (which would not fit in any margin) (?) https://en.wikipedia.org/wiki/Proof_by_infinite_descent https://en.wikipedia.org/wiki/Proof_by_infinite_descent
practal 2y ago
Very smart to open up the project from the start to make collaboration possible. I have ambivalent feelings about this project. On one hand, I think this is great, it approaches things in the right way, and I think the project has a big chance of being very successful. On the other hand, the more successful mathematics in Lean becomes, the more entrenched a type-theoretic outlook on formalised mathematics will become. I think that is highly problematic as it makes the expression of theorems and theories more involved and complicated than it needs to be. This is not a stopping block, and people like Buzzard can just power through this. Also, that's just my opinion. I am trying to go with Practal a different path and prove this opinion to be true, but that will take time.
- cjfd 2y ago
  I think the type-theoretic outlook on formalized mathematics is actually great, much nicer than set theory anyway. Set theory is a bit like an untyped programming language. You get to ask 'interesting' questions like whether the trivial group is equal to the number 5 which makes sense because both of them are actually a set. What I am dismayed about is giving yet another area of computing to Microsoft. We all know that Microsoft ensures great care of the long term quality of software, right? Like when you click 'delete' on an email in outlook and have to wait 20 seconds for it to actually disappear. Why not use coq instead?
  - msfanboy-aahum 2y ago
    The main dev of Lean no longer works at MS. So currently there are basically no ties to MS. Lean is developed by the Lean FRO, which aims at being selfsustainable in ~4 yrs from now.
  - kevinbuzzard 2y ago
    Lean is free and open source and nothing to do with MS. Check out https://lean-lang.org/ https://lean-lang.org/ and https://github.com/leanprover/lean4 https://github.com/leanprover/lean4 -- no mention of MS or MSR (where de Moura was where he developed Lean 3 and started on Lean 4). I have no doubt that a similar project could be done in Coq. The fact that we're using Lean is a random historical coincidence. If we'd used Coq then you could ask "why not Lean".
pylua 2y ago
I think this is awesome. I do wonder if projects like this will are the first step for humans to completely hand over proving to machines.
- criddell 2y ago
  At first I was going to react to you using "completely" because I thought the obvious thing was that the machines would remain a tool and maybe become collaborators. Then I started to think about it and now I have the same question. When will a machine spit out a proof that we just can't understand? Just like how a dog will never understand the fundamental theorem of calculus, there are almost certainly ideas and concepts that we can't understand but the machines might.
  - JoeAltmaier 2y ago
    Already happened? The four-color map theorem was a computer program exhaustively going through some solution-space until it found one. Thousands of lines of logic spit out on paper. Probably impossible for any human to comprehend.
    - pylua 2y ago
      That had been proven previously ? I guess so has flt, but it will eventually solve an unsolved problem ?
      - kevinbuzzard 2y ago
        Right now, machines proving stuff which is interesting to lots of human mathematicians but unprovable by them is science fiction. People seem to have very different opinions on the following two questions: 1) Whether it will still be science fiction by 2030; 2) Whether ITPs like Lean will be useful when working on this goal, or whether it will just be LLMs all the way. But rather than asking questions like "will some system belch out a million line incomprehensible proof of the Riemann Hypothesis" one could ask the following much easier question. Computers are very helpful to mathematicians who do calculations right now, but are way way less helpful to mathematicians who prove theorems (there are many pure mathematicians in my department who have absolutely no use for computers in their research other than the obvious email/search/etc applications). Can we make tools which will help these mathematicians (who might be trying to prove theorems about uncountable and noncomputable objects) to do their day job? Again one can ask two questions: 1) Will this still be science fiction in 2030; 2) Will ITPs be involved? And again I don't know the answers, but this work is an attempt by the Lean community to help ITPs understand precise statements of what's going on in modern number theory, in case that helps with (1).
throwaway81523 2y ago
Why has Lean taken over the formalization world? Previously some big proofs were done in Coq, HOL, etc.

75 points by happa 2y ago

https://www.techrxiv.org/users/717330/articles/702287-on-fermat-s-last-theorem https://www.techrxiv.org/users/717330/articles/702287-on-fer...

voldacar 2y ago
Why post this? This appears to be the writings of a crank.
- levn11 2y ago
  which part
  - n4r9 2y ago
    On p.4 you argue that for integers a, b, c and n: (a + b − c)^n = (c − a)(c − b)g_1(n) => a + b − c = [(c − a)(c − b)g_1(n)]^(1/n) => g_1(n) | a + b - c This doesn't follow as it stands. For example, if a=b=3 and c=n=2, then g_1(n)=16 whereas a + b - c = 4.
  - voldacar 2y ago
    The part in which FLT is derived from the binomial theorem, lol.
    - hughesjj 2y ago
      Nah not derived, set equal to from the outset with essentially no explanatory test throughout but with enough effort to insert some arbitrary graphs and label them with 'hey neato look at the vibes'
      - voldacar 2y ago
        My favorite part is "The derivative resembles the rhythm of a heartbeat."
n4r9 2y ago
This would definitely benefit from a bit more explanatory text as I'm struggling to understand what you've shown. The crux seems to be that if a^n+b^n=c^n then (c-a)(c-b) divides (a+b-c)^n. I haven't been through all the details of this, but I also don't see how that implies FLT.
- hughesjj 2y ago
  If I'm not mistaken Fermat's last theroem isn't even featured in the proof. Like nowhere did I see a^n+b^n=c^n referenced in the proof,save for the end of page 1 and 3, but it's never featured in an equality. Just 'this implies this trust me bro'.
  - n4r9 2y ago
    I've actually had another quick look and I now have a vague idea of the outline. It's an attempted proof by contradiction, where a solution to FLT is applied to the binomial theorem and some arguments about integrality are made to form a contradiction. My issue at the moment is with a line at the bottom of p.4, which effectively says that if k^n = xy for integers k, n, x, y, then k must be a multiple of y. Unless I'm missing something this is clearly false, for example 2^4 = 4 x 4.

rndnumthy 2y ago

What I really like is that this project will not blindly formalize the proof from the 90's. Instead they take a SOTA approach, streamlining and optimizing many parts of the proof. So it will result in a useful artifact for modern number theorists.

Pet_Ant 2y ago
SOTA?
- lightspot21 2y ago
  SOTA = state of the art

rndnumthy 2y ago

PDF slides from the talk where the project was launched: https://math.mit.edu/~drew/vantage/BuzzardSlides.pdf https://math.mit.edu/~drew/vantage/BuzzardSlides.pdf

mehulashah 2y ago

I wonder if after all that work, we might automatically reduce the proof and discover a simpler one that could have been included in the “margin”.

ultrablack 2y ago
I was just about to post my proof, but it didnt fit on Twitter :)
kevinbuzzard 2y ago
I highly doubt that the proof will get small enough to fit into a margin, but history shows that it's not at all unreasonable to expect simplifications/generalisations of the argument to come out of a formalisation (for example this happened with the Liquid Tensor Experiment, where dependence on stable homotopy groups of sphere was completely removed from the argument). I think it is unreasonable to expect that at the end of an FLT formalisation there will be no mention of elliptic curves, modular forms, Galois representations etc (the standard tools used by Wiles to prove the result in the 90s and which have themselves been simplified and generalised by mathematicians such as Taylor and Kisin since then). And you'll need quite a big margin to get all that stuff in.
downboots 2y ago
perhaps it was a veiled suggestion to use infinity in the proof (which would not fit in any margin) (?) https://en.wikipedia.org/wiki/Proof_by_infinite_descent https://en.wikipedia.org/wiki/Proof_by_infinite_descent

practal 2y ago

Very smart to open up the project from the start to make collaboration possible. I have ambivalent feelings about this project. On one hand, I think this is great, it approaches things in the right way, and I think the project has a big chance of being very successful. On the other hand, the more successful mathematics in Lean becomes, the more entrenched a type-theoretic outlook on formalised mathematics will become. I think that is highly problematic as it makes the expression of theorems and theories more involved and complicated than it needs to be. This is not a stopping block, and people like Buzzard can just power through this. Also, that's just my opinion. I am trying to go with Practal a different path and prove this opinion to be true, but that will take time.

cjfd 2y ago
I think the type-theoretic outlook on formalized mathematics is actually great, much nicer than set theory anyway. Set theory is a bit like an untyped programming language. You get to ask 'interesting' questions like whether the trivial group is equal to the number 5 which makes sense because both of them are actually a set. What I am dismayed about is giving yet another area of computing to Microsoft. We all know that Microsoft ensures great care of the long term quality of software, right? Like when you click 'delete' on an email in outlook and have to wait 20 seconds for it to actually disappear. Why not use coq instead?
- msfanboy-aahum 2y ago
  The main dev of Lean no longer works at MS. So currently there are basically no ties to MS. Lean is developed by the Lean FRO, which aims at being selfsustainable in ~4 yrs from now.
- kevinbuzzard 2y ago
  Lean is free and open source and nothing to do with MS. Check out https://lean-lang.org/ https://lean-lang.org/ and https://github.com/leanprover/lean4 https://github.com/leanprover/lean4 -- no mention of MS or MSR (where de Moura was where he developed Lean 3 and started on Lean 4). I have no doubt that a similar project could be done in Coq. The fact that we're using Lean is a random historical coincidence. If we'd used Coq then you could ask "why not Lean".

pylua 2y ago

I think this is awesome. I do wonder if projects like this will are the first step for humans to completely hand over proving to machines.

criddell 2y ago
At first I was going to react to you using "completely" because I thought the obvious thing was that the machines would remain a tool and maybe become collaborators. Then I started to think about it and now I have the same question. When will a machine spit out a proof that we just can't understand? Just like how a dog will never understand the fundamental theorem of calculus, there are almost certainly ideas and concepts that we can't understand but the machines might.
- JoeAltmaier 2y ago
  Already happened? The four-color map theorem was a computer program exhaustively going through some solution-space until it found one. Thousands of lines of logic spit out on paper. Probably impossible for any human to comprehend.
  - pylua 2y ago
    That had been proven previously ? I guess so has flt, but it will eventually solve an unsolved problem ?
    - kevinbuzzard 2y ago
      Right now, machines proving stuff which is interesting to lots of human mathematicians but unprovable by them is science fiction. People seem to have very different opinions on the following two questions: 1) Whether it will still be science fiction by 2030; 2) Whether ITPs like Lean will be useful when working on this goal, or whether it will just be LLMs all the way. But rather than asking questions like "will some system belch out a million line incomprehensible proof of the Riemann Hypothesis" one could ask the following much easier question. Computers are very helpful to mathematicians who do calculations right now, but are way way less helpful to mathematicians who prove theorems (there are many pure mathematicians in my department who have absolutely no use for computers in their research other than the obvious email/search/etc applications). Can we make tools which will help these mathematicians (who might be trying to prove theorems about uncountable and noncomputable objects) to do their day job? Again one can ask two questions: 1) Will this still be science fiction in 2030; 2) Will ITPs be involved? And again I don't know the answers, but this work is an attempt by the Lean community to help ITPs understand precise statements of what's going on in modern number theory, in case that helps with (1).

throwaway81523 2y ago

Why has Lean taken over the formalization world? Previously some big proofs were done in Coq, HOL, etc.