feat: Add Shafarevich's Theorem on solvable Galois groups problem

[bixbyr]

feat: Add Shafarevich's Theorem on solvable Galois groups problem. This states that every finite solvable group can be realized as the Galois group of a number field K / Q.

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

[kim-em]

🤖 Claude says:

Three things before merge:

• Drop the import LeanEval.NumberTheory.Shafarevich line from LeanEval.lean. That file aggregates only 18 of the 214 problem modules and isn't needed for a new problem. It also makes this PR conflict with your feat: Add Kronecker-Weber Theorem problem #476 and feat: Add Unconditional Odlyzko Bound problem #477, which add a line in the same place.
• Use ∃ (K : Type) rather than Type*. With Type* the statement has to hold in every universe at once, so a solver has to ULift for no reason; the convention here is Type (see MartinetTotallyRealTowers.lean).
• The notes field does real work in this repo: what Mathlib already has, why the statement is phrased this way, how the problem differs from its neighbours. Compare abel_ruffini.toml. Worth a paragraph — and worth saying that Shafarevich's original argument had a gap at 2 that was repaired later, since source points at the 1954 paper.