Zulip Chat Archive

Stream: FLT-regular

Topic: Exponent 3

Riccardo Brasca (Oct 03 2022 at 09:13):

I've added @Ruben Van de Velde work for exponent equal to 3, so we can check it compiles with latest mathlib. In particular we have a sorry free proof of

lemma flt_three
  {a b c : ℤ}
  (ha : a ≠ 0)
  (hb : b ≠ 0)
  (hc : c ≠ 0) :
  a ^ 3 + b ^ 3 ≠ c ^ 3 :=

Riccardo Brasca (Oct 03 2022 at 09:23):

This is technically not needed for caseI, but still, it's nice to have it...

Ruben Van de Velde (Oct 03 2022 at 10:27):

Thanks!

Chris Birkbeck (Oct 03 2022 at 12:31):

Riccardo Brasca said:

This is technically not needed for caseI, but still, it's nice to have it...

Is that true? I think at some point Washington uses that p is not 3

Chris Birkbeck (Oct 03 2022 at 12:34):

Actually yes, the proof first does 3 by other methods and then $p \geq 5$ is done with all the lemmas we are working on.

Riccardo Brasca (Oct 03 2022 at 12:34):

I mean we don't need the full statement.

Chris Birkbeck (Oct 03 2022 at 12:34):

oh yeah ok I see what you mean

Riccardo Brasca (Oct 03 2022 at 12:34):

It doesn't matter, but CaseI for p=3 is easy (and already formalized I think).

Riccardo Brasca (Oct 03 2022 at 12:35):

The first really interesting one is p=7 according to Washington

Chris Birkbeck (Oct 03 2022 at 12:36):

Yep!

Chris Birkbeck (Oct 03 2022 at 12:37):

(not that we can prove its regular)

Riccardo Brasca (Oct 03 2022 at 09:13):

I've added @Ruben Van de Velde work for exponent equal to 3, so we can check it compiles with latest mathlib. In particular we have a sorry free proof of

lemma flt_three
  {a b c : ℤ}
  (ha : a ≠ 0)
  (hb : b ≠ 0)
  (hc : c ≠ 0) :
  a ^ 3 + b ^ 3 ≠ c ^ 3 :=

Riccardo Brasca (Oct 03 2022 at 09:23):

This is technically not needed for caseI, but still, it's nice to have it...

Ruben Van de Velde (Oct 03 2022 at 10:27):

Thanks!

Chris Birkbeck (Oct 03 2022 at 12:31):

Riccardo Brasca said:

This is technically not needed for caseI, but still, it's nice to have it...

Is that true? I think at some point Washington uses that p is not 3

Chris Birkbeck (Oct 03 2022 at 12:34):

Actually yes, the proof first does 3 by other methods and then $p \geq 5$ is done with all the lemmas we are working on.

Riccardo Brasca (Oct 03 2022 at 12:34):

I mean we don't need the full statement.

Chris Birkbeck (Oct 03 2022 at 12:34):

oh yeah ok I see what you mean

Riccardo Brasca (Oct 03 2022 at 12:34):

It doesn't matter, but CaseI for p=3 is easy (and already formalized I think).

Riccardo Brasca (Oct 03 2022 at 12:35):

The first really interesting one is p=7 according to Washington

Chris Birkbeck (Oct 03 2022 at 12:36):

Yep!

Chris Birkbeck (Oct 03 2022 at 12:37):

(not that we can prove its regular)

Last updated: Dec 20 2023 at 11:08 UTC