feat: Add Kronecker-Weber Theorem problem

[bixbyr]

feat: Add the Kronecker - Weber theorem. This states that every finite abelian extension of Q is contained in a cyclotomic field.

Co-authored-by: Gemini 3.1 Pro gemini@google.com

[kim-em]

I'm dubious this is a hard enough problem for LeanEval.

[alreadydone]

Apparently there's a 16-page proof of the local version: https://arxiv.org/abs/2206.05801 (h/t Jason Rute on Zulip)
It's an intended application of the local class field theory project
Kevin commented on the sources
Apparently @xroblot is currently working on it

[xroblot]

Apparently there's a 16-page proof of the local version: https://arxiv.org/abs/2206.05801 (h/t Jason Rute on Zulip) It's an intended application of the local class field theory project Kevin commented on the sources Apparently @xroblot is currently working on it

Indeed, I have an almost complete proof of Kronecker-Weber here. Missing parts are results coming from some PRs still in the queue and results about quadratic fields for the case p = 2. The proof relies on a paper of Lemmermeyer that proves Kronecker-Weber via Stickelberger theorem. (PS. The code has been mostly written by me and Claude was only used to help manage the project.)

[kim-em]

I think this problem is just too easy for LeanEval at the moment: we need to push towards harder problems. It's great that people are working on formalizing this, but their aim should be towards LeanPool + TauCeti + Mathlib + Palomar, etc, not LeanEval.

[bixbyr]

That makes sense. Crazy world where this actually counts as easy considering it needs global class field theory :)

I was thinking about the N groups paper from Thompson, sort of a sequel to the odd order theorem and another horribly huge finite group theory brawl. If we needs definitions which are not in math lib to state the theorem are they best in the same file as the problem statement?

Edit: if we do propose that problem, it uses Feit-Thompson as one of its assumptions. Since that is a separate challenge problem, should it take the odd order theorem as a hypothesis to avoid coupling the two problems?