Siegel's Lemma

Stream: mathlib4

[Fabrizio Barroero]

Hi everyone!
During the Lean workshop which took place last January in Roma Tor Vergata, me and some colleagues (@Amos Turchet and @Laura Capuano ), encouraged by @Riccardo Brasca and @Filippo A. E. Nuccio , started a project aiming to prove Siegel's lemma. The first sorry-free proof goes back to the end of last February. During the LFTCM 2024 event I showed some parts of the proof to Riccardo, Filippo and @Floris van Doorn and got some very useful tips that improved the proof quite a lot. Thanks guys! I think it is now time to try to add this to Mathlib. For that I need GitHub permission, my GitHub username is fbarroero.
Actually, the original long-term plan was to prove some Diophantine Approximation result (e.g. Thue's Theorem or maybe even Roth's Theorem). This is a much more ambitious project which we might start working on during the summer.

[Floris van Doorn]

invite sent

[Fabrizio Barroero]

Floris van Doorn said:

invite sent

Thanks!

[Michael Stoll]

It would be great to have Roth's Theorem!

[Fabrizio Barroero]

Michael Stoll said:

It would be great to have Roth's Theorem!

It would surely be great! We will see how far we get...

[Yaël Dillies]

Funnily enough, mathlib acquired Roth's theorem yesterday (the other Roth's theorem)

[Fabrizio Barroero]

Cool!

[Filippo A. E. Nuccio]

Fabrizio Barroero said:

Hi everyone!
During the Lean workshop which took place last January in Roma Tor Vergata, me and some colleagues (Amos Turchet and Laura Capuano ), encouraged by Riccardo Brasca and Filippo A. E. Nuccio , started a project aiming to prove Siegel's lemma. The first sorry-free proof goes back to the end of last February. During the LFTCM 2024 event I showed some parts of the proof to Riccardo, Filippo and Floris van Doorn and got some very useful tips that improved the proof quite a lot. Thanks guys! I think it is now time to try to add this to Mathlib. For that I need GitHub permission, my GitHub username is fbarroero.
Actually, the original long-term plan was to prove some Diophantine Approximation result (e.g. Thue's Theorem or maybe even Roth's Theorem). This is a much more ambitious project which we might start working on during the summer.

Congratulations! Do not hesitate to tell us the PR numbers as soon as you open them.

[Fabrizio Barroero]

Thanks! At the moment I have a problem. I am sure you guys can help me figure it out. I have created a file SiegelsLemma.lean in the NumberTheory folder with the first part of the proof. I need a lemma called mulVec_def which unfolds the definition of mulVec and I added it to the file Mathlib.Data.Matrix.Basic. I imported this in my SiegelsLemma.lean and run lake build Mathlib.Data.Matrix.Basic. Still, when I call the lemma I get unknown identifier 'mulVec_def'.

[Richard Osborn]

This error happens when you do lake build Mathlib.NumberTheory.SiegelsLemma?

[Kevin Buzzard]

Is it a namespace issue? What happens if you hit ctrl-space after mulVec_def?

[Filippo A. E. Nuccio]

Are you sure that mulVec is not inside a namespace that you need to open?

[Fabrizio Barroero]

Richard Osborn said:

This error happens when you do lake build Mathlib.NumberTheory.SiegelsLemma?

No, when the file is open, lean gives me that error

[Ruben Van de Velde]

I think the question is - if you try the lake command, does it also happen?

[Ruben Van de Velde]

But yes, check the namespace first

[Fabrizio Barroero]

It's inside a namespace Matrix, which is opened. In any case I get the same error with Matrix.mulVec_def.

If I run lake build Mathlib.NumberTheory.SiegelsLemmaI get:
⚠ [1683/1683] Built Mathlib.NumberTheory.SiegelsLemma
warning: ././././Mathlib/NumberTheory/SiegelsLemma.lean:103:22: unused variable i_1
note: this linter can be disabled with set_option linter.unusedVariables false
Build completed successfully.

[Filippo A. E. Nuccio]

It would be easier to help you if you can push this to a PR (that you can mark help wanted and/or WIP). Since at any rate you are planning to PR these things, it is perhaps the right moment to open it :smile:

[Fabrizio Barroero]

Done! It's #13470

[Filippo A. E. Nuccio]

OK, I'm having a look.

[Fabrizio Barroero]

Thanks Filippo!

[Filippo A. E. Nuccio]

No problem! I have started the review, will finish tomorrow :night:

[Richard Osborn]

btw, I believe the reason vscode gave you that error unknown identifier 'mulVec_def' is because it doesn't always see that an import has changed, and the file needs to be rebuilt. Clicking Restart File at the bottom of the infoview will fix this (or you can just build the file via the command line)

[Filippo A. E. Nuccio]

Yes, @Richard Osborn is right and if you restart the file everything works nicely. I have also started the review to you PR, please feel free to ask questions whenever some of my comments were unclear.

[Fabrizio Barroero]

Thanks but I restarted the file... it's still not working...

[Fabrizio Barroero]

Thanks for the help, Filippo. It's very useful

[Filippo A. E. Nuccio]

Let's advance little by little:

1. Is Mathlib.Data.Matrix.Basic compiling?
2. Can you close everything (including VSCode), do a lake exe cache get and then lake build?

[Riccardo Brasca]

You can try lake exe cache get! to be sure to download everything

[Riccardo Brasca]

(note the !)

[Fabrizio Barroero]

Thanks for the help. Unfortunately it still does not work. I have tried on 3 computers and get the same result

[Ruben Van de Velde]

So the code builds in our continuous integration but not on any of the three computers you tried? That sounds very surprising

[Fabrizio Barroero]

I must be doing something wrong... Also, since today, every time Mathlib is updated, even if I run lake exe cache get, it builds the imports and it takes forever. I apologise but I am really a Github beginner.

[Richard Osborn]

Have you tried lake exe cache get!?

[Fabrizio Barroero]

I did

[Richard Osborn]

Ok, when you say "every time Mathlib is updated", what commands/actions are you doing to update mathlib?

[Fabrizio Barroero]

I just press Commit in the source control panel of VS code

[Richard Osborn]

So until you push your changes to github and let CI build your code, the cache won't make your local builds any faster. If you modify a file in mathlib, all of the files that import it will have to be rebuilt (or if you are building a single file, all the files "between" the modified file and the file you are building will be rebuilt).

[Fabrizio Barroero]

I think I understand. Thanks!

[Fabrizio Barroero]

I just created the second PR #13487