## 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...

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

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...

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

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