Zulip Chat Archive

Stream: FLT-regular

Topic: lean4

Ruben Van de Velde (Jan 06 2023 at 18:43):

How far are we from porting? :)

Riccardo Brasca (Jan 06 2023 at 18:50):

We are surely far. Note that (this is my fault) the definition of cyclotomic polynomials uses the complex numbers.

Riccardo Brasca (Jan 06 2023 at 18:51):

In any case something I will try to do is to move all unneeded results (to prove case 1) in the unused folder

Riccardo Brasca (Jan 06 2023 at 18:54):

Riccardo Brasca said:

We are surely far. Note that (this is my fault) the definition of cyclotomic polynomials uses the complex numbers.

More precisely, we need the existence of a complex primitive root of unity of any order. And this probably uses a lot of properties of the exponential function...

Riccardo Brasca (Jan 06 2023 at 18:55):

And of course we need finiteness of the class group !

Yaël Dillies (Jan 06 2023 at 18:55):

Hmm... For the definition, why can you not use well-founded recursion?

Riccardo Brasca (Jan 06 2023 at 18:56):

Yaël Dillies said:

Hmm... For the definition, why can you not use well-founded recursion?

Yes. It was my first contribution to mathlib and I didn't chose the best definition, just the one I found on my head.

Riccardo Brasca (Jan 06 2023 at 18:57):

Now to be honest I am too lazy to refactor everything

Riccardo Brasca (Jan 11 2023 at 16:19):

Riccardo Brasca said:

In any case something I will try to do is to move all unneeded results (to prove case 1) in the unused folder

In 603b96ac8ae28c657f4c1847003c429e691bb835 I deleted a bunch of useless results that we wrote trying several approaches. If at some point someone doesn't find something they're sure was there at some point, they can have a look at this commit.

Eric Rodriguez (Jan 11 2023 at 16:21):

Is it worth just tagging that commit so we don't lose track of it? Or putting it on some branch?

Riccardo Brasca (Jan 11 2023 at 16:28):

This is why I wrote my message. In any case almost all the results I deleted were trivial, and at worst they were easy, so it shouldn't be a big deal.

My goal is to open maybe one last PR to mathlib, and be ready to port the project in a few months...

Yaël Dillies (Jan 11 2023 at 17:05):

Could that last PR be homogenization? :grinning_face_with_smiling_eyes: We need it for the combinatorial Nullstellensatz.

Riccardo Brasca (Jan 11 2023 at 17:17):

I think it's a very good idea

Riccardo Brasca (Jan 11 2023 at 17:18):

You need to convince @Alex J. Best

Ruben Van de Velde (Jan 06 2023 at 18:43):

How far are we from porting? :)

Riccardo Brasca (Jan 06 2023 at 18:50):

We are surely far. Note that (this is my fault) the definition of cyclotomic polynomials uses the complex numbers.

Riccardo Brasca (Jan 06 2023 at 18:51):

In any case something I will try to do is to move all unneeded results (to prove case 1) in the unused folder

Riccardo Brasca (Jan 06 2023 at 18:54):

Riccardo Brasca said:

We are surely far. Note that (this is my fault) the definition of cyclotomic polynomials uses the complex numbers.

More precisely, we need the existence of a complex primitive root of unity of any order. And this probably uses a lot of properties of the exponential function...

Riccardo Brasca (Jan 06 2023 at 18:55):

And of course we need finiteness of the class group !

Yaël Dillies (Jan 06 2023 at 18:55):

Hmm... For the definition, why can you not use well-founded recursion?

Riccardo Brasca (Jan 06 2023 at 18:56):

Yaël Dillies said:

Hmm... For the definition, why can you not use well-founded recursion?

Yes. It was my first contribution to mathlib and I didn't chose the best definition, just the one I found on my head.

Riccardo Brasca (Jan 06 2023 at 18:57):

Now to be honest I am too lazy to refactor everything

Riccardo Brasca (Jan 11 2023 at 16:19):

Riccardo Brasca said:

In any case something I will try to do is to move all unneeded results (to prove case 1) in the unused folder

In 603b96ac8ae28c657f4c1847003c429e691bb835 I deleted a bunch of useless results that we wrote trying several approaches. If at some point someone doesn't find something they're sure was there at some point, they can have a look at this commit.

Eric Rodriguez (Jan 11 2023 at 16:21):

Is it worth just tagging that commit so we don't lose track of it? Or putting it on some branch?

Riccardo Brasca (Jan 11 2023 at 16:28):

This is why I wrote my message. In any case almost all the results I deleted were trivial, and at worst they were easy, so it shouldn't be a big deal.

My goal is to open maybe one last PR to mathlib, and be ready to port the project in a few months...

Yaël Dillies (Jan 11 2023 at 17:05):

Could that last PR be homogenization? :grinning_face_with_smiling_eyes: We need it for the combinatorial Nullstellensatz.

Riccardo Brasca (Jan 11 2023 at 17:17):

I think it's a very good idea

Riccardo Brasca (Jan 11 2023 at 17:18):

You need to convince @Alex J. Best

Ruben Van de Velde (Mar 30 2023 at 12:07):

Fwiw, I ported n=3 at https://github.com/Ruben-VandeVelde/flt4

Eric Wieser (Mar 30 2023 at 12:29):

With mathport and not by hand, I hope!

Ruben Van de Velde (Mar 30 2023 at 12:33):

With mathport, though oneshot needed some hand holding - I'd hope we can improve the tooling before porting bigger projects

Riccardo Brasca (Mar 30 2023 at 13:10):

Nice!! I've played a little bit with oneshot, how do handle multiple files?

Ruben Van de Velde (Mar 30 2023 at 13:55):

You copy and paste them one after the other into a single file. (Or if there's a better way, I didn't find it.) This was most of the hand holding I referred to

Patrick Massot (Mar 30 2023 at 14:19):

Ruben, any documentation you could write on using mathport on non-mathlib projects would be very useful, and the same with precise issues reporting.

Eric Wieser (Mar 30 2023 at 14:23):

I would imagine that probably there's a straightforward way of configuring mathport to run on a standalone project, and that probably we could derive it by comparing the mathlib3port, lean3port, and oneshot configurations

Eric Wieser (Mar 30 2023 at 14:23):

I certainly don't think building a workflow that invokes one-shot repeatedly is a good approach!

Riccardo Brasca (Mar 30 2023 at 15:09):

Ruben Van de Velde said:

You copy and paste them one after the other into a single file. (Or if there's a better way, I didn't find it.) This was most of the hand holding I referred to

I did the same :rolling_on_the_floor_laughing:

Riccardo Brasca (Mar 30 2023 at 15:10):

I used it for a very small projet (only two files) and I did the align by hand, but it worked quite well.

Ruben Van de Velde (Mar 30 2023 at 15:53):

Patrick Massot said:

Ruben, any documentation you could write on using mathport on non-mathlib projects would be very useful, and the same with precise issues reporting.

I can't really say more than "concatenate the files and follow the instructions from https://github.com/leanprover-community/mathport/tree/master/Oneshot" at this point. I'm guessing there's a better way, but I don't know when I'd have time to find it

Riccardo Brasca (Mar 30 2023 at 15:54):

Since you just did it, can you confirm that the sentence "or just ./download_release to get the latest one automatically" is wrong? It seems there is no ./download_release script (./download-release.sh worked for me).

Riccardo Brasca (Mar 30 2023 at 15:55):

(Note the underscore and the dash)

Ruben Van de Velde (Mar 30 2023 at 16:02):

I'm afraid I can't - it turns out I'm pretty bad at following instructions and I went back and forth a few times across the instructions :)

Ruben Van de Velde (Mar 30 2023 at 16:03):

Does seem like I ran ./download-release.sh at some point, though

Ruben Van de Velde (Apr 04 2023 at 13:18):

Kevin fixed that, btw: https://github.com/leanprover-community/mathport/pull/233

Riccardo Brasca (Apr 04 2023 at 13:22):

Nice!

Last updated: Dec 20 2023 at 11:08 UTC