Fermat's Last Theorem

Stream: new members

[R Dong]

I am doing this proof in NNG. Am I missing something obvious or do I have to do a triple induction on a, b, and c? I also can't use any of the inequality theorems.

Also, the repeat tactic in NNG doesn't seem to support picking one of multiple tactics, unlike the standard one. Is that the case?

[Julian Berman]

I don't follow the title of your question. Are you actually asking about Fermat's Last Theorem?

[Riccardo Brasca]

If you are doing level 10 of power world note the sentence "This level looks superficially like other levels we have seen, but the shortest solution known to humans would translate into many millions of lines of Lean code. The author of this game, Kevin Buzzard, is working on translating the proof by Wiles and Taylor into Lean, although this task will take many years."

[R Dong]

Yeah it's level 10. I hope it's not going to actually take me millions of lines... unless it's meant to be an unbeatable level?

[Yaël Dillies]

Let's say that if you beat it, then someone (ie Kevin Buzzard) is out of a job for the next five years

[Alex Mobius]

I wish to see the day when proof assistants will crack that kind of thing like it's nothing.

[R Dong]

I mean, I solved the base case... and then feel like the rest is really complicated.

Maybe it should be made more obvious that that level is not required.

[Alex Mobius]

Only took us all 400 years, so don't beat yourself down :).

[Riccardo Brasca]

Wait, the base case is flt for exponent 3, isn't it?

[R Dong]

I mean the case when a, b, c, are all zero

[Riccardo Brasca]

Ah ok :sweat_smile:

[Ruben Van de Velde]

Kevin is hoping for another George Dantzig and the next five years on the beach :beach:

[Kevin Buzzard]

Yes, unfortunately this level is impossible. In fact in a draft future version of NNG this level will be moved into a whole world of impossible levels, such as the Goldbach conjecture, the Twin Prime conjecture and so on. I just have no time to work on NNG right now.

[Andrew Yang]

Wait, it's impossible? What should I work on for the next four years...

[Kevin Buzzard]

I mean the proof is too large to fit in the NNG box!

[Mario Carneiro]

especially since you can't make definitions in the NNG box, it would be an interesting challenge to see whether it can be done

[Mario Carneiro]

I suspect that the proof would be too large to elaborate as a single declaration

[Vera Huang]

I wonder if this level 10 for Fermat's Last Theorem haven't been solved in NNG, how can we get into the Advanced multiplication World? :face_with_monocle:

[Kevin Buzzard]

Power world is not a prerequisite for advanced multiplication world, right?

[Vera Huang]

Ohh,,yes. I figure out that when I review the previous theorem and close it before the web refresh, the game will show that I haven't proved the theorem yet. :joy:

[Vera Huang]

sorry for bother :melting_face: