Project idea: FLT3

Stream: LFTCM 2024

[Riccardo Brasca]

I would like to propose the proof of Fermat Last Theorem for exponent 3 as a project. A couple of comments:

• first of all we already have a formalized proof (see here, in the FltRegular/FltThree/ folder): that proof stays in ℤ and I would like to formalize the proof that uses ℤ[ζ₃].
• Almost all the number theoretic prerequisites are already in mathlib, so the work is totally doable.
• The final goal is not only to have a proof, but to have a mathlib-ready proof (indeed FLT3 is a special case that does not follow from the general case proved by Wiles).

For these reasons I think it's a very good project especially for students who like number theory (it is a good occasion to learn some beautiful math is you've never seen this proof).

I am going to do it anyway if nobody is interested, so I've prepared a repository here. As you can see I've already structured the proof I want to follow, there are "only" 37 sorry, but most of them are very easy (some of them will maybe need to be split, we will see).

Let me know if you want to participate!

[Riccardo Brasca]

If you've never played with Lean, sorry means "unproved results".

[Kevin Buzzard]

This is the first blue node in the FLT project by the way!

[Florestan]

Do you have a reference for the proof you are following ?

[Johan Commelin]

I think that the reference currently is:

• Buzzard, Kevin and Taylor, Richard. Private communication, 2023.

[Riccardo Brasca]

@Florestan if you mean the proof of FLT3 yes

[Riccardo Brasca]

It's here, page 43

[Riccardo Brasca]

It's in French but I guess this is not a problem

[Riccardo Brasca]

(english version, page 84 maybe paywalled)

[Florestan]

yes, thank you !

[Riccardo Brasca]

To get the repository (assuming Lean and git are installed), one can do

git clone https://github.com/riccardobrasca/flt3.git
lake exe cache get
lake build

the last step should take no more than a couple of minutes (and it should start compiling something like 2410/2412, not 1/2412).

[Riccardo Brasca]

note that copying/pasting the two files inside any other repository depending on mathlib will not work (because it uses a "future" version of mathlib)

[Riccardo Brasca]

To be precise I am following a slightly modified version of the proof, essentially I am not doing case 1 for the more general equation but only for the original one (since case 1 in ℤ is easy even in Lean, and it is already in mathlib, while case 1 for the general equation would be annoying).

In particular I am not proving that the more general equation has no solution, but only that it has no solution in case 2, but this is enough to have case 2 in ℤ and so FLT3. I guess nobody really cares about the more general equation.

[Notification Bot]

5 messages were moved from this topic to #LFTCM 2024 > Installation issues by Anatole Dedecker.

[davidlowryduda]

I think in Riccardo's steps above, you probably want to cd into the newly cloned repo. So I think one might do

git clone https://github.com/riccardobrasca/flt3.git
cd flt3
lake exe cache get
lake build

[Riccardo Brasca]

Yes, sorry, that's absolutely correct

[Riccardo Brasca]

If you are interested in FLT3 please show up here!

[Emilie Uthaiwat]

I would like to work on this project.

[Florent Schaffhauser]

I'm interested :+1:

[Pietro Monticone]

I'm interested.

[Lorenzo Luccioli]

I'm interested

[Riccardo Brasca]

Good! I propose to meet this afternoon after Amelia's talk somewhere (maybe in the library) to set up everything.

[Riccardo Brasca]

I really think we can finish this by Friday

[Sanyam Gupta]

I am interested too

[Florent Schaffhauser]

Riccardo Brasca said:

git clone https://github.com/riccardobrasca/flt3.git

How did you set up your repo in a way that it contains no or lakefile.lean or lean-toolchain file at the root of your directory?

[Riccardo Brasca]

The repo and what you have on you computer are two different things. lake exe cache get will download everything you need inside the project folder

[Omar Haddad]

Interested too :hand:

[Florent Schaffhauser]

Riccardo Brasca said:

The repo and what you have on you computer are two different things. lake exe cache get will download everything you need inside the project folder

Right, but I am asking because I did not even need to do that (the Lean 4 VS Code extension took care of it).

I am just surprised: what if you want to use a specific version of Lean, say 4.6.0, can you set this up somewhere in your repo? Usually, I would just edit the lean-toolchainfile and run lake update.

[Riccardo Brasca]

What you can start doing is to get the project and write here your github username

[Riccardo Brasca]

Flo (Florent Schaffhauser) said:

Riccardo Brasca said:

The repo and what you have on you computer are two different things. lake exe cache get will download everything you need inside the project folder

Right, but I am asking because I did not even need to do that (the Lean 4 VS Code extension took care of it).

I am just surprised: why if you want to use a specific version of Lean, say 4.6.0, can you set this up somewhere in your repo?

yes, you can do whatever you want. For example I specified in lakefile.lean that it uses mathlib from the branch RB/CIRM.

[Riccardo Brasca]

I am not completely familiar with all the various options, but you can specify absolutely whatever you want, and lake will do the right thing.

[Florent Schaffhauser]

Which lakefile.lean file? I don't see any :sweat_smile:

[Florent Schaffhauser]

Sorry, I'm talking about the FLT3 repo

[Florent Schaffhauser]

OK, Riccardo has just explained it to me: his repo does contain the files in question, and indeed they have been cloned to my machine: they just don't show up in VS Code due to some special settings in the .vscode/settings.json file. These can be modified by hand but maybe Riccardo will update the repo at some point?

[Florent Schaffhauser]

Either way, it works!

[davidlowryduda]

I'm also interested in working on this.

[Kevin Buzzard]

blue_node.png

It will fill in a blue node in the (currently still private) FLT repo so I would be very happy if this made it to mathlib :-)

[Riccardo Brasca]

May we claim we did 20% of the work when flt is done?

[Kevin Buzzard]

I guess some nodes are harder than others...

[Omar Haddad]

Riccardo Brasca said:

What you can start doing is to get the project and write here your github username

https://github.com/OmarHaddad

[Riccardo Brasca]

We can have a coffee together after Amelia's talk and look for a place to start working

[Riccardo Brasca]

https://github.com/riccardobrasca/flt3/

[Riccardo Brasca]

https://link.springer.com/book/10.1007/978-1-4471-2131-2

[Riccardo Brasca]

page 84

[Riccardo Brasca]

lemma dvd_of_mul_dvd_mul_left {R : Type*} [CancelMonoidWithZero R] (a b c : R) (hc : c ≠ 0)
    (H : c * a ∣ c * b) : a ∣ b := by
  rcases H with ⟨d, hd⟩
  exact ⟨d, by simpa [mul_assoc, hc] using hd⟩

[Riccardo Brasca]

lemma dvd_of_mul_dvd_mul_left {R : Type*} [CancelMonoidWithZero R] (a b c : R) (hc : c ≠ 0)
    (H : c * a ∣ c * b) : a ∣ b := by
  rcases H with ⟨d, hd⟩
  refine ⟨d, ?_⟩
  rw [mul_assoc, mul_eq_mul_left_iff] at hd
  rcases hd with (hd | hd)
  · rw [hd]
  · exfalso
    exact hc hd

[Pietro Monticone]

Opened a related PR #11677

[Pietro Monticone]

We've just rewritten the MWE and we've not been able to reproduce the #find_home! "bug" we thought we found yesterday with @Riccardo Brasca:

import Mathlib

lemma dvd_of_mul_dvd_mul_left_1 {R : Type*} [CancelMonoidWithZero R] (a b c : R) (hc : c ≠ 0)
    (H : c * a ∣ c * b) : a ∣ b := by
  rcases H with ⟨d, hd⟩
  refine ⟨d, ?_⟩
  rw [mul_assoc, mul_eq_mul_left_iff] at hd
  rcases hd with (hd | hd)
  · rw [hd]
  · exfalso
    exact hc hd

#find_home! dvd_of_mul_dvd_mul_left_1

lemma dvd_of_mul_dvd_mul_left_2 {R : Type*} [CancelMonoidWithZero R] (a b c : R) (hc : c ≠ 0)
    (H : c * a ∣ c * b) : a ∣ b := by
  rcases H with ⟨d, hd⟩
  exact ⟨d, by simpa [mul_assoc, hc] using hd⟩

#find_home! dvd_of_mul_dvd_mul_left_2

They both return the following output:

[Mathlib.Algebra.GroupWithZero.Divisibility,
 Mathlib.Algebra.Order.Ring.Pow,
 Mathlib.Data.Set.Pointwise.ListOfFn,
 Mathlib.Algebra.Order.Nonneg.Field,
 Mathlib.Algebra.Divisibility.Prod,
 Mathlib.Algebra.GroupWithZero.Power,
 Mathlib.Data.Nat.MaxPowDiv,
 Mathlib.Data.Int.Cast.Lemmas,
 Mathlib.Algebra.Group.NatPowAssoc,
 Mathlib.Algebra.Ring.Fin,
 Mathlib.Algebra.Order.Invertible,
 Mathlib.Tactic.NormNum.Basic,
 Mathlib.Algebra.EuclideanDomain.Instances,
 Mathlib.Data.Rat.Defs]

[Riccardo Brasca]

Maybe something was wrong with my computer, let's just ignore it.

[Riccardo Brasca]

The file is getting really slow. I've created the branch faster with a small modification that should make things a little faster, but with the cost of having to write a lot of hζ. Can you see if it looks faster on your computer?

[Riccardo Brasca]

Anyway I am going to sleep, see you tomorrow!

[Pietro Monticone]

Sure, I’ll do it tomorrow morning.

[Kevin Buzzard]

I'd be happy to look at any slow code if you want to post it here

[Riccardo Brasca]

@Kevin Buzzard it is the file flt3.lean in https://github.com/riccardobrasca/flt3 (I just gave you push rights if you want to experiment). It can be the usual problems with rings of integers, or the fact that η and λ are both notation. In the branch faster I replaced CyclotomicField 3 ℚ K (a specific model) with a generic cyclotomic extension, and as usual this helps a bit.

At any rate feel free to play with the code, but don't worry if you don't have time. Thanks!

[Kevin Buzzard]

Is there a specific declaration which is slow?

[Arend Mellendijk]

I don't have much experience diagnosing performance issues, but I'm seeing a lot of this in the slow bits.

[Meta.synthInstance] [0.246859s] ✅ HAdd ↥(𝓞 K) ↥(𝓞 K) ↥(𝓞 K) ▼
  [] [0.102071s] ❌ apply @Subalgebra.seminormedCommRing to SeminormedCommRing ↥(𝓞 K) ▶
  [] [0.110639s] ❌ apply @Subalgebra.normedCommRing to NormedCommRing ↥(𝓞 K) ▶

[Arend Mellendijk]

Also this line takes over five seconds to run on my machine. Looks like it's generating an 8000-line pretty-printer.

[Florent Schaffhauser]

@Riccardo Brasca is saying: a_cube_b_cube_same_congr is one of the first slow declarations

[Pietro Monticone]

Reminder for the other team: we are working on "odd" sorries.

We have proved:

• https://github.com/riccardobrasca/flt3/blob/f0b8a7e5ddd1454ff14723cc52f79667a1158a3c/FLT3/FLT3.lean#L418
• https://github.com/riccardobrasca/flt3/blob/f0b8a7e5ddd1454ff14723cc52f79667a1158a3c/FLT3/FLT3.lean#L447
• https://github.com/riccardobrasca/flt3/blob/f0b8a7e5ddd1454ff14723cc52f79667a1158a3c/FLT3/FLT3.lean#L477
• https://github.com/riccardobrasca/flt3/blob/f0b8a7e5ddd1454ff14723cc52f79667a1158a3c/FLT3/FLT3.lean#L511

[Riccardo Brasca]

Arend Mellendijk said:

Also this line takes over five seconds to run on my machine. Looks like it's generating an 8000-line pretty-printer.

Maybe I can try to make it a def

[Kevin Buzzard]

I added some dirty hacks to speed things up (I golfed a proof and I increased the priority of some instances; this is just a workaround to make your lives a bit easier) (and I pushed)

[Kevin Buzzard]

yeah something is seriously messed up with that notation!

/-- Let `K` be `CyclotomicField 3 ℚ` and let `η : 𝓞 K` be the root of unity given by
`IsCyclotomicExtension.zeta`. We also set `λ = η - 1` -/
def hζ := IsCyclotomicExtension.zeta_spec 3 ℚ K
local notation3 "η" => hζ.toInteger

count_heartbeats in -- Used 124986 heartbeats, which is less than the current maximum of 200000.
local notation3 "λ" => η - 1

[davidlowryduda]

I note for my group later that there is IsCoprime.isUnit_of_dvd', which we wanted earlier.

[Kevin Buzzard]

Arend Mellendijk said:

Also this line takes over five seconds to run on my machine. Looks like it's generating an 8000-line pretty-printer.

How can you see these 8000 lines? I can just see that it's taking 125K heartbeats. (I've minimised and asked in #mathlib4 )

[Pietro Monticone]

Opened #11691 undoing #11677 since we have found out that the lemmas

https://github.com/leanprover-community/mathlib4/blob/044f1333d4e273d0d45e7fdeaf07266d7e043c32/Mathlib/Algebra/GroupWithZero/Divisibility.lean#L171-L179

already exist in the same file with different names mul_dvd_mul_iff_left and mul_dvd_mul_iff_right:

https://github.com/leanprover-community/mathlib4/blob/0f2ac6785f4ecb39c798a30eee01dafa63c828d7/Mathlib/Algebra/GroupWithZero/Divisibility.lean#L46-L58

[Pietro Monticone]

Of course we have updated everything accordingly in the FLT3 repository.

[davidlowryduda]

Ok, I added a bit to our proof. I'm lean-stuck on a simple (I think) result:

If we know that $\lambda$ is prime, $p$ is prime, and $\lambda$ is not an associate of $p$ , then how can we convince lean that $p$ doesn't divide $\lambda$ ?

[davidlowryduda]

I expect this to be very straightforward.

[Riccardo Brasca]

docs#Prime.dvd_prime_iff_associated

[Pietro Monticone]

Opened #11695 generalising mul_dvd_mul_left to Monoid since it was only implemented for CommMonoid.

[Florent Schaffhauser]

Next step

Team Pietro can do this:

lemma lambda_not_dvd_x : ¬ λ ∣ S.x := by
  sorry

lemma lambda_not_dvd_y : ¬ λ ∣ S.y := by
  sorry

lemma lambda_not_dvd_z : ¬ λ ∣ S.z := by
  sorry

lemma lambda_not_dvd_w : ¬ λ ∣ S.w := by
  sorry

And the other team can do:

lemma coprime_x_y : IsCoprime S.x S.y := by
  sorry

lemma coprime_x_z : IsCoprime S.x S.z := by
  sorry

lemma coprime_y_z : IsCoprime S.y S.z := by
  sorry

lemma x_mul_y_mul_z : S.x * S.y * S.z = S.u * S.w ^ 3 := by
  sorry

Everybody agrees?

[Florent Schaffhauser]

PS: We did leave "Lemma 4" open, but we'll get back to it later :sweat_smile:

[Pietro Monticone]

Yes, we’re working on the first one.

[Florent Schaffhauser]

We just pushed coprime_x_y

[Pietro Monticone]

We proved lambda_not_dvd_w. We are working on lambda_not_dvd_x now.

[Florent Schaffhauser]

We just pushed coprime_x_z

[Florent Schaffhauser]

As well as coprime_y_z

[Pietro Monticone]

We just finished too.

[Florent Schaffhauser]

Just pushed x_mul_y_mul_z

[Johan Commelin]

You guys are on a roll!

[Pietro Monticone]

We finally proved lambda_pow_dvd_a_add_b!

[Harald Helfgott]

Sorry for being ignorant - where is the repository?
I'd like to catch up.

[Harald Helfgott]

Will I get an up-to-date version of everything if I type
"git clone https://github.com/riccardobrasca/flt3.git
lake exe cache get
lake build"?

[Pietro Monticone]

Harald Helfgott said:

Will I get an up-to-date version of everything if I type
"git clone https://github.com/riccardobrasca/flt3.git
lake exe cache get
lake build"?

Hi, we are proving the “ideals_coprime” lemma.

I’ll write here when we finish and you can follow the procedure you wrote to get the latest version.

[Harald Helfgott]

OK
What will people be working on next?

[Pietro Monticone]

Just finished the proof of “ideals_coprime” lemma. We are going to push it in a few minutes.

[Pietro Monticone]

Harald Helfgott said:

OK
What will people be working on next?

Then we are going to solve as many sorries as can.

If you want to contribute you can start from the last sorry in the file “FLT3.lean”.

[Pietro Monticone]

We’ve just pushed the proof for the “ideals_coprime” lemma.

[Florent Schaffhauser]

Together with @davidlowryduda, @Omar Haddad and Alexis, we were planning to work on this next:

lemma X_ne_zero : S.X ≠ 0 := by
  sorry

lemma lambda_not_dvd_X : ¬ λ ∣ S.X := by
  sorry

lemma lambda_not_dvd_Y : ¬ λ ∣ S.Y := by
  sorry

lemma lambda_not_dvd_Z : ¬ λ ∣ S.Z := by
  sorry

lemma coprime_Y_Z : IsCoprime S.Y S.Z := by
  sorry

[Harald Helfgott]

So, wait: we are in the case where lambda does not divide X Y Z? Why is it then non-trivial to show that lambda does not divide any of X, Y or Z?

[Harald Helfgott]

Is ideals_coprime the statement that a minimal solution must have X, Y, Z coprime?

[Harald Helfgott]

I'm a bit confused by what is meant by 'minimal' here. In the main case of the proof, it is clear - exactly one of the three variables (say, z) is divisible by lambda, and we order solutions by v_\lambda(z).

[Harald Helfgott]

Not sure where the statement and proof of Lemma 2.7 are?

[Harald Helfgott]

We obviously need that.

[Pietro Monticone]

UPDATE: We have just proved and pushed the “span_x_mul_span_y_mul_span_z”.

[Harald Helfgott]

I am somehow not getting that new version (with span_x_mul_span_y_mul_span_z - what does that mean?)

Forgive me for asking, but what does span_x_mul_span_y_mul_span_z mean? What does a Span mean here?

[davidlowryduda]

Harald Helfgott said:

Not sure where the statement and proof of Lemma 2.7 are?

We don't prove Lemma 2.7. Instead, we are actually proving flt3 only in the second case in the reference, which is the case when $3 \mid abc$. I think I heard that the other case (which is what Lemma 2.7 handles easily) is already in mathlib, but I'm not sure.

[davidlowryduda]

Harald Helfgott said:

I am somehow not getting that new version (with span_x_mul_span_y_mul_span_z - what does that mean?)

Forgive me for asking, but what does span_x_mul_span_y_mul_span_z mean? What does a Span mean here?

You can ask lean to define things for you. For example, hovering over span I get the message that span(u) is the ideal generated by the element u.

[Harald Helfgott]

But we will need Lemma 2.7 even in the second case in the reference.

[Harald Helfgott]

In the last paragraph of the proof (I'm going by the English-language version - the one published by Springer), "We finish by pointing out that..." follows from Lemma 2.7.

[davidlowryduda]

Looking at the document, I see that the implication from this last paragraph is in by_kummer, which is sorryd. Perhaps Kummer's lemma is also in mathlib? I don't know.

[Riccardo Brasca]

davidlowryduda said:

Looking at the document, I see that the implication from this last paragraph is in by_kummer, which is sorryd. Perhaps Kummer's lemma is also in mathlib? I don't know.

It is in cyclo, for p=3

[davidlowryduda]

Oh, nevermind --- it's in cyclo, and is called eq_one_or_neg_one_of_unit_of_congruent

[davidlowryduda]

(As Riccardo also just noted)

[Riccardo Brasca]

I spent the last two years proving kummer's lemma in general (with 5 collaborators), but it is not going to be in mathlib soon :sweat_smile:

[Harald Helfgott]

I don't mean the "therefore" (that follows from what we have just "finished by pointing out" by Kummer) - I mean what we "finish by pointing out"; to point that out, we need Lemma 2.7, no?

[Harald Helfgott]

It follows from the last displayed equation by Lemma 2.7

[davidlowryduda]

The "we finish" is the proof in cyclo, and the "therefore..." is the stubbed proof by_kummer

[davidlowryduda]

Suppose I have hx: p | x and hy: p | y. I want to show that x and y are not coprime. How do I put these hypotheses together into some definition and tell lean that?

[Harald Helfgott]

Sorry if I am being extremely obtuse, but it seems to me that eq_one_or_neg_one_of_unit_of_congruent (in cyclo) is the special case of Kummer that we need for the 'therefore...' step

[Harald Helfgott]

whereas ±1 ± u^4 ≡ 0 mod λ^2 follows from the displayed equation by (element not divisible by lambda)^3 = ±1 mod λ^2, which is a weaker ve

[Harald Helfgott]

a weaker version of Lemma 2.7

[Harald Helfgott]

Have we proved at least that weaker version? It's not obvious how to prove it without proving Lemma 2.7 in the process.

[Chris Birkbeck]

davidlowryduda said:

Suppose I have hx: p | x and hy: p | y. I want to show that x and y are not coprime. How do I put these hypotheses together into some definition and tell lean that?

I'm sure there is something better, but you could try IsCoprime.isUnit_of_dvd'?

[Harald Helfgott]

For that matter, we need the full power (such as it is) of Lemma 2.7 to get ±1 ± 1 ≡ u z^3 mod λ^4, two lines after (3.4) (it is an immediate consequence of (3.4) and Lemma 2.7).

[Harald Helfgott]

So we do need Lemma 2.7. Is it elsewhere in cyclo?

[Riccardo Brasca]

We can discuss this tomorrow, but mathematically we are here: we have a b c : 𝓞 K (here K is a 3-rd cyclotomic extension of ℚ) such that a^3+b^3=u*c^3, where u : (𝓞 K)ˣ and ¬ λ ∣ a, ¬ λ ∣ b and λ ∣ c, where λ = η - 1 and η is a fixed 3-rd root of unity (we know all the properties of λ, for example it is a prime). We also may (and do) assume that λ ^ 2 ∣ a + b.

[Riccardo Brasca]

we know that:

• λ ∣ (a + η * b)
• λ ∣ (a + η ^ 2 * b)
• ¬ λ ^ 2 ∣ (a + η * b)
• ¬ λ ^ 2 ∣ (a + η ^ 2 * b)

[Riccardo Brasca]

so we write (here t is the multiplicity of λ in c, that we know it is at least 2):

• a + b = λ^(3*t-2) * x
• a + η * b = λ * y
• a + η ^ 2 * b = λ * z

[Riccardo Brasca]

we know that x, y and z are pairwise coprime, and that

x * y * z = u * w^3 (1)

where c = λ ^ t * w

[Riccardo Brasca]

this is all done in Lean

[Riccardo Brasca]

Now, we move from (1) to the corresponding equality for ideals

[Riccardo Brasca]

so we have that the product of three pairwise coprime ideals is a cube in a PID, so each generator is a cube up to a unit, and this is the next math step

[Riccardo Brasca]

this is where we write x = u₁ * X^3, and similarly for y and z

[Riccardo Brasca]

Kummer's lemma enters into the story because playing with X, Y, Z and u₁, u₂, u₃, we can prove that

Y ^ 3 +u₄ * Z ^ 3 = u₅ * (λ ^ (t - 1) * X) ^ 3

where u₄ and u₅ are explicit.

[Riccardo Brasca]

Now, this looks like the original equation (the one we want to do the descent on), but there is an extraneous u₄. Looking modulo λ^2 and using kummer's lemma, we get u₄ = ±1 (since cubes not 0 modulo λ^2 are ±1 mod λ^2, and nothing is 0 mod λ^2 in this equation), so we have

Y ^ 3 +(u₄ * Z) ^ 3 = u₅ * (λ ^ (t - 1) * X) ^ 3

[Riccardo Brasca]

this essentially finishes the proof

[Harald Helfgott]

Right, thanks. I don't want to sound like a broken record, but I'm still wondering why we are not proving Lemma 2.7: we are using it implicitly in the above to ensure that λ ^ 2 ∣ a + b (otherwise I don't see how you are justifying that).

[Riccardo Brasca]

we have it

[Harald Helfgott]

We have Lemma 2.7?

[Riccardo Brasca]

it's called lambda_sq_dvd_or_dvd_or_dvd

[Riccardo Brasca]

no, sorry

[Riccardo Brasca]

it is a_cube_b_cube_same_congr

[Riccardo Brasca]

sorry again

[Riccardo Brasca]

lemma lambda_pow_four_dvd_cube_sub_one_or_add_one_of_lambda_not_dvd {x : 𝓞 K} (h : ¬ λ ∣ x) :
    λ ^ 4 ∣ x ^ 3 - 1 ∨ λ ^ 4 ∣ x ^ 3 + 1 := by

[Harald Helfgott]

Ah well then!
That clears matters

[Riccardo Brasca]

this is in cyclo, and it is used to prove that we may assume λ ^ 2 ∣ a + b (this condition holding or not is the difference between what I call Solution' (without the condition) and Solution)

[Riccardo Brasca]

we know that given a Solution' we may construct a Solution with the same c, so in practice we can work with a Solution

[Harald Helfgott]

OK, I'm a happy camper. Will try to fall asleep now.

[Riccardo Brasca]

same here. good night!

[Harald Helfgott]

There's not much left to do, is there?

[Riccardo Brasca]

I feel we are almost done, but maybe the devil is in the details

[Kevin Buzzard]

The devil will be getting it into mathlib :-)

[davidlowryduda]

Perhaps I went down a bit of a hole, but say I have the following status

S: Solution
p: ↥(𝓞 K)
hp: Prime p
p_dvd_Y: p ∣ Y S
p_dvd_Z: p ∣ Z S
auxY: p ∣ y S
auxZ: p ∣ z S
gcd_isUnit: IsUnit (gcd (y S) (z S))
⊢ ¬IsRelPrime (y S) (z S)

This is obviously mathematically true: auxY and auxZ immediately give a common prime factor p. But I don't know how to use lean's definition of IsRelPrime to conclude.

[Riccardo Brasca]

You should probably look in the API for IsRelPrime, but yesterday I had the impression we can avoid this notion. We can have a look together after the talk.

[davidlowryduda]

I just added the three lambda_not_dvd_* proofs.

[davidlowryduda]

Listening to these details on structures is very interesting. But it also makes me appreciate the work @Riccardo Brasca did in setting up the structures (and the whole outline) for this project before this workshop.

[davidlowryduda]

Thanks!

[Riccardo Brasca]

Solution' is indeed a structure, and Solution extends Solution'. We never need to use ext but it can be added.

[Riccardo Brasca]

I introduced those just to avoid having an infoview with like 37 variables a, b, c, u, x, ... and 62 assumptions

[davidlowryduda]

In the alternate world where we made our own outline and setup as we went along, I think we wouldn't have realized that Solution' and Solution would be so good at managing complexity and information hiding. I'm reminded of the experience of first learning a programming language with custom datatypes --- judicious types makes the whole process much easier to reason about.

[Pietro Monticone]

We're going to start proving these lemmas:

lemma x_eq_unit_mul_cube : ∃ (u₁ : (𝓞 K)ˣ) (X : 𝓞 K), S.x = u₁ * X ^ 3 := by
  sorry

lemma y_eq_unit_mul_cube : ∃ (u₂ : (𝓞 K)ˣ) (Y : 𝓞 K), S.y = u₂ * Y ^ 3 := by
  sorry

lemma z_eq_unit_mul_cube : ∃ (u₃ : (𝓞 K)ˣ) (Z : 𝓞 K), S.z = u₃ * Z ^ 3 := by
  sorry

[Florent Schaffhauser]

We just pushed X_ne_zero and coprime_Y_Z (so we’re done with the list from last night).

[davidlowryduda]

We're going to start proving

lemma u₄'_isUnit : IsUnit S.u₄' := by
  sorry

lemma u₅'_isUnit : IsUnit S.u₅' := by
  sorry

[Pietro Monticone]

We have added the following (still sorried) necessary lemmas:

lemma span_x_cube : ∃ I : Ideal (𝓞 K), span {S.x} = I^3 := by sorry

lemma span_y_cube : ∃ I : Ideal (𝓞 K), span {S.y} = I^3 := by sorry

lemma span_z_cube : ∃ I : Ideal (𝓞 K), span {S.z} = I^3 := by sorry

[Florent Schaffhauser]

We just pushed u₅'_isUnit

[Pietro Monticone]

Fixed bugs in new lemmas. We’re almost there!

[Florent Schaffhauser]

Excellent! Did you push to GitHub?

[Pietro Monticone]

Yes

[Riccardo Brasca]

I'm off to marseille, but I am sure you are doing an amazing job!

[Harald Helfgott]

Riccardo: Are you off to Marseille to have bouillabaisse?

[Riccardo Brasca]

I am seeing some friends, but no bouillabaisse paid by the conference only for me, don't worry :grinning:

[Harald Helfgott]

Money is not the issue, fish is the issue. Can some of us get together and pay extra for CIRM
bouillabaisse?

[Riccardo Brasca]

I have no idea, you can maybe ask

[Pietro Monticone]

Merged #11691

[Pietro Monticone]

We’ve just proved and pushed the following lemmas:

• x_unit_mul_cube;
• y_unit_mul_cube;
• z_unit_mul_cube.

[Pietro Monticone]

Now we tackle “formula_2”.

[Florent Schaffhauser]

Oh, ok! But I think that David had some remarks about the statement of that lemma.

[Florent Schaffhauser]

@Pietro Monticone Just so you know, there is also this:

lemma x_ne_y : S.x ≠ S.y := by sorry
lemma x_ne_z : S.x ≠ S.z := by sorry
lemma y_ne_z : S.y ≠ S.z := by sorry

[Pietro Monticone]

We know, we know. They are probably not needed. It was for the old proof of the latest lemmas we’ve proved and pushed.

We added comments to remind ourselves to discuss the removal of those lemmas we believe are not necessary.

[Florent Schaffhauser]

Ok, great! In any case, the first message was meant to avoid you spending a significant amount of time on Formula 2 if it ends up being the wrong statement.

[Pietro Monticone]

Ok, thank you!

[davidlowryduda]

I had noticed two things odd about formula2 before. But looking more, I see that one of them was because we had misdefined u_5 and u_5'. I just fixed that and pushed. (Interestingly, this didn't change the proof that u5 was a unit, as lean happily handled the missing inverse on its own).

[davidlowryduda]

That's the important one. The other observation is that in a vacuum, maybe I would have phrased formula1 differently. The way to transform formula2 into formula1 is to multiply formula2 by $\eta \lambda u_2$ (and then to parse the new notation for u4 and u5 correctly).

[davidlowryduda]

I guess this also indicates how to transform formula1 into formula2. Either is fine, as $\eta \lambda u_2$ is prime (and more importantly, obviously nonzero).

[davidlowryduda]

But multipying by $\eta$ is odd, as it suggests that we should have used a different combination of roots of unity to obtain formula1. This doesn't matter though.

[davidlowryduda]

There aren't so many sorry's left!

[Kevin Buzzard]

When you're done you can try proving that 5 is a regular prime, then you can do FLT5 :-)

[Chris Birkbeck]

I think we know that it's a PID in that case, so know its regular. FLT7 is next one we need.

[Pietro Monticone]

We’ve just proved an additional lemma we will use to prove “formula2” whatever is the u_4 unit.

[davidlowryduda]

I was thinking about the 6 remaining sorrys a bit. I think formula2, by_kummer, and final are all straightforward. But the three new lemmas saying that $x , y, z$ are pairwise unequal is rather finicky.

[Pietro Monticone]

Don’t worry about the three new lemmas. There almost certainly useless.

[davidlowryduda]

Yes, I was thinking about how to prove the one result we use them for, but without them.

[davidlowryduda]

It's true without those assumptions. But it is convenient to iterate over the finite set in that way.

[davidlowryduda]

I wonder if there is enough PID and unique factorization stuff in lean to make it easy.

[davidlowryduda]

Anyhow, that's a job for tomorrow me. Now I sleep.

[Pietro Monticone]

davidlowryduda said:

It's true without those assumptions. But it is convenient to iterate over the finite set in that way.

We have already worked around that with the following lemmas:

• x_unit_mul_cube;
• y_unit_mul_cube;
• z_unit_mul_cube.

[Pietro Monticone]

davidlowryduda said:

Anyhow, that's a job for tomorrow me. Now I sleep.

Sure. Se you tomorrow.

[davidlowryduda]

Oh, you pushed these away in the last 20 minutes or so! That's wonderful.

[davidlowryduda]

Outstanding

[Riccardo Brasca]

Pietro Monticone said:

We’ve just proved an additional lemma we will use to prove “formula2” whatever is the u_4 unit.

Yep, that is docs#IsCyclotomicExtension.Rat.five_pid

[Riccardo Brasca]

Sorry, I wanted to answer to Chris comment

[Riccardo Brasca]

Chris Birkbeck said:

I think we know that it's a PID in that case, so know its regular. FLT7 is next one we need.

This message

[Pietro Monticone]

We’ve just pushed a partial proof of “by_kummer”.

[davidlowryduda]

I pushed a proof of final.

[davidlowryduda]

Now just formula2 and by_kummer are left. I'm not sure how the ending of by_kummer is supposed to go mathematically though.

[Pietro Monticone]

We’re working on “formula2” and “by_kummer”.

[Pietro Monticone]

Locally fixed those ugly timeout errors (thanks @Floris van Doorn! )

[davidlowryduda]

I just pushed a longer partial formula2, with almost everything worked out except for exponent arithmetic

[Riccardo Brasca]

omega should take care of that

[davidlowryduda]

I had hoped that too, but it complains when I try. But last time I tried to reason with exponents you did give me some one line thing that solved my woes.

[Riccardo Brasca]

let me have a look

[Riccardo Brasca]

unless some of you wants to finish it :)

[Pietro Monticone]

I’m gonna try it

[Riccardo Brasca]

it is very similar (the exact same thing?) as what we did yesterday night

[Riccardo Brasca]

Anyway, stuff like

  rw [show λ * η * ↑(u₂ S) * Y S ^ 3
           +
           λ * η ^ 2 * ↑(u₃ S) * Z S ^ 3
           +
           ↑(u₁ S) * X S ^ 3 * λ ^ (3 * multiplicity S - 2)
           =
           ↑(u₁ S) * X S ^ 3 * λ ^ (3 * multiplicity S - 2)
           +
           ↑(u₂ S) * η * Y S ^ 3 * λ
           +
           ↑(u₃ S) * η ^ 2 * Z S ^ 3 * λ  by ring_nf]
  exact formula1 S

can be done via

  convert formula1 S using 1
  ring

[davidlowryduda]

haha, that seems like a pretty substantial improvement

[Pietro Monticone]

Solved the sorry by

have tmp : λ * (↑(u₁ S) * (λ ^ (multiplicity S - 1) * X S) ^ 3)
             =
             ↑(u₁ S) * X S ^ 3 * λ ^ (3 * multiplicity S - 2) := by
    rw [mul_comm, mul_assoc, mul_assoc]
    congr 1
    rw [mul_pow, mul_comm, ← mul_assoc, mul_comm _ (S.X ^ _)]
    congr 1
    rw [← pow_mul, ← pow_succ]
    congr 1
    have := two_le_multiplicity S
    omega

[Pietro Monticone]

Now we need to tackle by_kummer.

[Florent Schaffhauser]

We should get together after the talk!

[Riccardo Brasca]

There is nothing special in by_kumme, don't worry

[davidlowryduda]

Ah, it really was similar to what you did yesterday. I haven't used congr much.

[davidlowryduda]

Here, the third time you used it, it recognized that it was sufficient to work with just the exponents. This was the secret!

[davidlowryduda]

Very nice.

[Florent Schaffhauser]

I've removed the three commented sorry's from the file (the ones from yesterday), you can pull the changes from GitHub.

[Pietro Monticone]

Great. Thanks.

[Pietro Monticone]

Oh btw, we finished :check:

[Pietro Monticone]

@Lorenzo Luccioli and I have just finished writing a sketch for our tomorrow's presentation.

You can find it here https://github.com/riccardobrasca/flt3/blob/master/FLT3/README.md

[Florent Schaffhauser]

@Pietro Monticone and @Lorenzo Luccioli Just updated the md file. Please double check for typos and omissions on my part :pray: Thanks!

[Pietro Monticone]

I've just polished and pushed the final version of the talk. https://github.com/riccardobrasca/flt3/tree/master/FLT3

[Pietro Monticone]

I've talked with @Lorenzo Luccioli , @davidlowryduda and @Flo (Florent Schaffhauser) a few minutes ago and we agreed on the following plan:

1. I'll start the lightning talk going through Motivation and Overview projecting VS Code from my laptop and switching between FLT3.lean and the Markdown document.
2. Anybody can interrupt whenever needed
3. @Lorenzo Luccioli will present the Lean Showcase we prepared yesterday night

[Florent Schaffhauser]

Pietro Monticone said:

I've just polished and pushed the final version of the talk. https://github.com/riccardobrasca/flt3/tree/master/FLT3

@Pietro Monticone
Great, thanks! But I guess you did not pull before editing the file? Because the modifications I made this morning are no longer there (I had renamed the file to FinalPres.md).

[davidlowryduda]

Ah, good catch

[Pietro Monticone]

Oh sorry. I didn't noticed. I'll fix it.

[Florent Schaffhauser]

No worries :blush:

[Pietro Monticone]

Done https://github.com/riccardobrasca/flt3/tree/master/FLT3

[Florent Schaffhauser]

OK, I'll remove FinalPres.mdthen :+1:

[Florent Schaffhauser]

Done (plus some markdown cleanup).

[Pietro Monticone]

Pushed final version with direct links to slide comments so that @Lorenzo Luccioli can easily and quickly switch from the README.md file (in preview mode) to the relevant line in the FLT3.lean script. https://github.com/riccardobrasca/flt3/tree/master/FLT3

[Florent Schaffhauser]

Nice!

[Florent Schaffhauser]

Added reference to Theorem 2.6 p.84 in Hindry's book.

[Riccardo Brasca]

I've open #11767. You can have a look and comment/improve it. I can show you how to get it on your computer if you need it. I didn't pay too much attention to the names, so feel free to check them.

[Pietro Monticone]

I'll try to setup the blueprint for the FLT3 project in order to understand how it works and force myself to learn at least some of the underlying mathematics I don't know yet.

[Pietro Monticone]

Riccardo Brasca said:

I've open #11767. You can have a look and comment/improve it. I can show you how to get it on your computer if you need it. I didn't pay too much attention to the names, so feel free to check them.

What's the difference between:

/-!
Documentation comments...
-/

and

/--
Documentation comments...
-/

?

[Riccardo Brasca]

Probably something is displayed differently in the webpage, I don't know the details.

[Riccardo Brasca]

I copy/paste the same header since 3 years.

[Kevin Buzzard]

One of them shows up on the documentation web pages but is not attached to any declaration. The other is attached to a declaration so it also shows up when you hover over the declaration

[Kevin Buzzard]

eg any definition in mathlib will have a /-- before it and then wherever it appears in mathlib you can hover over it to find out what it is

[Riccardo Brasca]

I am updating mathlib, so we can use the "normal" version. This means that after the next git pull you have to do lake exe cache get.

Funny thing: yesterday the definition of monoid changed in mathlib (!) so a couple of proofs broke, but nothing serious.

[Pietro Monticone]

Kevin Buzzard said:

One of them shows up on the documentation web pages but is not attached to any declaration. The other is attached to a declaration so it also shows up when you hover over the declaration

I see. Thanks.

[Riccardo Brasca]

Anyway thanks everybody for all the work! I didn't see some of you yesterday afternoon and I didn't say goodbye in person, but it was really a pleasure to work with you.

And don't forget we want all of this in mathlib! :D

[Pietro Monticone]

Thank you for your amazing support and supervision! Learnt a lot.

[Florent Schaffhauser]

It was a great week indeed :blush:🧑🏼‍💻 Let’s do this again soon!

[Pietro Monticone]

I’ll add documentation to #11767 as soon as I can.

[Pietro Monticone]

Just opened #11791 to RB/flt3_reduction adding the first two tentative docstrings. If they're considered Mathlib-quality I'm going to document as many lemmas as I can this evening.

[Anatole Dedecker]

Just as a side note, PRs to another branch than master don't really fit in our workflow. Of course there's nothing wrong with using them, but the usual process is to ask "is it fine if I push [foo] on your branch" and if the answer is yes you can just do it directly.

[Pietro Monticone]

Ops, I didn’t know that. Sorry.

[Anatole Dedecker]

No reason to be!

[Pietro Monticone]

Closed #11791. I'll ask directly when necessary then.

[Pietro Monticone]

I have managed to get blueprint to work (https://github.com/pitmonticone/FLT3) after encountering the problems forewarned by @Floris van Doorn.

When I find the time, I will open a PR here https://github.com/PatrickMassot/leanblueprint to include the solution in the README so that others do not have to face the same issues.

[Pietro Monticone]

Done https://github.com/PatrickMassot/leanblueprint/pull/16

[Pietro Monticone]

I believe I’ve done everything correctly (https://github.com/pitmonticone/FLT3 ) but I don’t get why the GitHub page returns a 404 error (https://pitmonticone.github.io/FLT3).

Could it be due to the fact that I’ve not added anything in content.tex yet?

[Rémy Degenne]

It's because that's not the right address for the blueprint: https://pitmonticone.github.io/FLT3/blueprint/

[Rémy Degenne]

leanblueprint does not presume that's it's the only thing on you website and lets you have your own index page if you want

[Pietro Monticone]

Ops :man_facepalming:

Thank you very much!

[Rémy Degenne]

(and in your case there is no index.html at the root, so 404)

[Rémy Degenne]

And your doc is at https://pitmonticone.github.io/FLT3/docs/

[davidlowryduda]

I wrote about this a bit: https://davidlowryduda.com/flt3-at-lftcm2024/

[davidlowryduda]

This was fun! I suppose I should reexamine our code and start adjusting it for mathlib, including docs and conventions

[Riccardo Brasca]

@davidlowryduda thanks for writing this! Just a small comment: the fact that $\mathbb{Z}[\zeta_3]$ is a PID (or UFD, for ring of integers these notions are equivalent) is of course a key point, but to apply Minkowski's criterion one has first of all to know that $\mathbb{Z}[\zeta_3]$ is the ring of integers of $\mathbb{Q}(\zeta_3)$, something true but non obvious. And luckily this is already in mathlib!

[Riccardo Brasca]

I am PRing the prerequisites, (see #11767 and #11792, both marked awaiting author, but I will take care of the comments today). I agree that making η a unit will probably golf some of the proofs, especially those at the end (we need to find a way to convince automation to use η^2+η+1!).

[Pietro Monticone]

davidlowryduda said:

This was fun! I suppose I should reexamine our code and start adjusting it for mathlib, including docs and conventions

I’ll do it too + the blueprint as mentioned above. Here is the (now working) empty website: https://pitmonticone.github.io/FLT3.

[Pietro Monticone]

Writing the blueprint for FLT3, I realised that the lemma ideals_coprime (https://github.com/riccardobrasca/flt3/blob/23ef890df76a7383c3d8bc235abe7933df04336f/FLT3/FLT3.lean#L686C1-L709C16) is useless and can be removed without breaking anything.

I'm going to push the change to the original repository in a minute.

[Pietro Monticone]

Done :check:

[Pietro Monticone]

And the same is true for the lemma x_mul_y_mul_z https://github.com/riccardobrasca/flt3/blob/23ef890df76a7383c3d8bc235abe7933df04336f/FLT3/FLT3.lean#L670C1-L681C44 of course (since it's completely substituted by x_mul_y_mul_z_eq_u_w_pow_three). I'm going to remove that too.

[Pietro Monticone]

Done :check:

[Florent Schaffhauser]

Super nice @Pietro Monticone ! :tada:

[Pietro Monticone]

I've just finished documenting the Cyclo.lean file. https://github.com/pitmonticone/FLT3/blob/master/FLT3/Cyclo.lean

I'm going to push the the fully documented version to the original repository https://github.com/riccardobrasca/flt3/blob/master/FLT3/Cyclo.lean.

[Pietro Monticone]

The documentation of Cyclo.lean is going to be published in a few minutes here https://pitmonticone.github.io/FLT3/docs/FLT3/Cyclo.html.

[Pietro Monticone]

Done :check:

[Riccardo Brasca]

Thanks for doing this!

[Riccardo Brasca]

Just a comment: in my opinion the documentation should provide the bridge between the mathematical statement and the lean statement (of course it's not always clear what this means, since we have different mental images), and I have the impression your doc are a literal translation of the lean statement

[Riccardo Brasca]

For example, the difference between eta and zeta is mathematically irrelevant. And even if it should be mentioned once, I think that keeping repeating it just makes things more difficult to parse

[Riccardo Brasca]

But again, thanks for all the work, this is just a suggestion!

[Pietro Monticone]

Sure, I thought the blueprint should provide the bridge between the math and lean.

[Pietro Monticone]

I thought "Since we are documenting the Lean code..."

[Edgar Costa]

Also,

Let u be a unit in (𝓞 K)ˣ.`

shows up in various statements in the documentation, where the statement doesn't involve u.
Maybe along the lines of what @Riccardo Brasca , would be better to state all the variables up top.

[Pietro Monticone]

Edgar Costa said:

Also,

Let u be a unit in (𝓞 K)ˣ.`

shows up in various statements in the documentation, where the statement doesn't involve u.
Maybe along the lines of what Riccardo Brasca , would be better to state all the variables up top.

Ops, you're totally right. I'm going to fix that in a few minutes.

[Pietro Monticone]

Done :check:

[Pietro Monticone]

The dependency graph skeleton (without all the informal statements and proofs) should be finished in a few days https://pitmonticone.github.io/FLT3/blueprint/dep_graph_document.html

[Pietro Monticone]

Moved lambda_ne_zero from FLT3.lean to Cyclo.lean as we wrote in a comment and modified a few lemmas in FLT3.lean accordingly (lambda_ne_zero to (lambda_ne_zero hζ)) https://github.com/riccardobrasca/flt3/commits/master

[Pietro Monticone]

I've just verified that the lemma span_x_mul_span_y_mul_span_z is useless too. I'm going to remove it. https://github.com/pitmonticone/FLT3/blob/d37f6e39c4c6922ddbd3c8539bbab65d11628111/FLT3/FLT3.lean#L715-L724

[Pietro Monticone]

Same for lambda_sq_dvd_u_mul_cube.

[Pietro Monticone]

Update:

• Code documentation and refactoring completed :check: https://pitmonticone.github.io/FLT3/docs/
• Dependency graph completed :check: https://pitmonticone.github.io/FLT3/blueprint/dep_graph_document.html
• Blueprint: informalised statements completed :check: https://pitmonticone.github.io/FLT3/blueprint/index.html
• Blueprint: informalised proofs in progress https://pitmonticone.github.io/FLT3/blueprint/index.html

If anyone wants to review the work done so far, I would greatly appreciate it.

[Riccardo Brasca]

I am in Singapore for two weeks, so I don't have too much time, but it looks a great job!

[Pietro Monticone]

Update: 12 informalised proofs left. I should be able to conclude by the end of the week.

[Riccardo Brasca]

#11767 is now merged, so I am bumping mathlib and removing the corresponding results from the project.

[Pietro Monticone]

Simplified proof of associated_of_dvd_a_add_b_of_dvd_a_add_eta_sq_mul_b

[Pietro Monticone]

Simplified proof of final (thanks @Lorenzo Luccioli ).

[Pietro Monticone]

Update:

• Code documentation and refactoring completed :check: https://pitmonticone.github.io/FLT3/docs/
• Dependency graph completed :check: https://pitmonticone.github.io/FLT3/blueprint/dep_graph_document.html
• Blueprint: informalised statements completed :check: https://pitmonticone.github.io/FLT3/blueprint/index.html
• Blueprint: informalised proofs completed :check: https://pitmonticone.github.io/FLT3/blueprint/index.html

[Riccardo Brasca]

#11792 is merged. I've updated the repo and opened #12765.

[Riccardo Brasca]

Opened also #12767

[Riccardo Brasca]

Just to let you know that #14653 finishes the proof of flt3.

[Johan Commelin]

Great work!

[Riccardo Brasca]

This is now in mathlib! I think we can declare the project a success :partying_face: thanks to all for your contribution