Formalizing theorems using Lean4

Stream: maths

[Suryansh Shrivastava]

My project advisor and I are looking at lean as a possible field for my final UG project. We are looking to formalize one of these proofs:-
Stickelberger's Theorem
Gelford-Schneider Theorem.
Any ideas on how feasible it is to formalize these proofs in Lean4 in 4 months? I have a basic understanding of Lean4 as a programming language.

[Andrew Yang]

I think it would be better to use Lean 3 since mathlib is still on Lean 3.

[Suryansh Shrivastava]

Any ideas on when we could port Mathlib4

[Johan Commelin]

See #mathlib4. It's happening right now.

[Johan Commelin]

But it will take some time before it's finished.

[Riccardo Brasca]

Stickelberger’s Theorem about the discriminant? It would be very nice to have it in mathlib! But you need quite a lot of algebraic number theory, so I would suggest to use mathlib, so Lean 3.

[Junyan Xu]

There's the recent work formalizing Lindemann-Weierstrass which also concerns transcendence but doesn't imply Gelford-Schneider or vice versa (both are consequences of Baker's theorem though).

[Bharath]

Hi, thank you for the suggestion. What I had in mind was Stickelberger's theorem on the annihilation of class groups of cyclotomic fields.

I have no experience with Lean. So the two suggestions (Sticekelber's theorem in algebraic number theory versus Gelfond--Schneider in transcendental number theory) above are somewhat disjoint; I am hoping that at least one of them will be a suitable undergraduate thesis problem for Suryansh (who has a little bit of experience with Lean).

[Kevin Buzzard]

Both of those are impossible in lean 4 and both would be attemptable in lean 3 but whether the student finishes would depend on how hard they worked, they would both be substantial projects.

[Eric Rodriguez]

for reference, we're currently doing the 1st case of flt for regular primes over on #FLT regular , and a running joke is that computing the class group of the 3rd cyclotomic extension is beyond us

[Riccardo Brasca]

I have a proof that that one is a euclidean domain! But that's it

[Riccardo Brasca]

I mean, I almost have a proof, but the idea is that formalizing graduate mathematics is a lot of work

[Riccardo Brasca]

But any partial result in that direction would be a more than welcomed contribution to mathlib, so don't hesitate to try!

[Michael Stoll]

There is a recent paper by @Anne Baanen, @Alex J. Best, Nirvana Coppola and @Sander Dahmen on formalized class group computations in Lean, see arXiv:2209.15492.

[Riccardo Brasca]

Very nice paper!! @Anne Baanen @Alex J. Best @Sander Dahmen did you formalize that the norm of a principal ideal is (the ideal generated by) the norm of a generator?

[Alex J. Best]

Yes indeed, that's used quite heavily for showing primality of ideals. We made a couple of definitions of ideal norm and show they agree, so it should be usable for both definitions fairly easily

[Riccardo Brasca]

Waiting for the PRs!