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

LeanEval/NumberTheory/ShafarevichSolvableGalois.lean

@@ -0,0 +1,16 @@
+import Mathlib
+import EvalTools.Markers
+
+namespace LeanEval
+namespace NumberTheory
+
+/-- **Shafarevich's theorem on solvable Galois groups**. Every finite solvable
+group is realizable as a Galois group over `ℚ`. -/
+@[eval_problem]
+theorem shafarevich_solvable_galois (G : Type*) [Group G] [Finite G] [IsSolvable G] :
+    ∃ (K : Type) (_ : Field K) (_ : Algebra ℚ K) (_ : FiniteDimensional ℚ K) (_ : IsGalois ℚ K),
+      Nonempty (G ≃* (K ≃ₐ[ℚ] K)) := by
+  sorry
+
+end NumberTheory
+end LeanEval

manifests/problems/shafarevich_solvable_galois.toml

@@ -0,0 +1,9 @@
+id = "shafarevich_solvable_galois"
+title = "Shafarevich's theorem on solvable Galois groups"
+test = false
+module = "LeanEval.NumberTheory.ShafarevichSolvableGalois"
+holes = ["shafarevich_solvable_galois"]
+submitter = "Ryan Smith"
+notes = "Every finite solvable group is realizable as a Galois group over ℚ: the solvable case of the inverse Galois problem. Mathlib has IsSolvable and the Galois correspondence, but nothing about realizability — no embedding problems, no Scholz–Reichardt construction, no inverse-Galois API at all — so a solver builds the extensions from scratch. Distinct from the two other Shafarevich problems in the catalog: shafarevich_relation_rank_bound (the cohomological relation-rank inequality for the maximal unramified pro-p extension) and golod_shafarevich_inequality. Shafarevich's original 1954 proof contained an error at the prime 2, which he later corrected; the source field cites both the correction and a modern complete proof."
+source = "I. R. Shafarevich, 'Construction of fields of algebraic numbers with given solvable Galois group', Izv. Akad. Nauk SSSR Ser. Mat. 18 (1954), no. 6, 525–578, https://www.mathnet.ru/eng/im3517. The prime-2 correction appears in Shafarevich's Collected Mathematical Papers, Springer (1989). For a complete corrected proof, see A. Schmidt and K. Wingberg, 'Šafarevič's theorem on solvable groups as Galois groups' (1998), https://arxiv.org/abs/math/9809211."
+informal_solution = "Reduce the realization problem to split finite embedding problems with nilpotent kernels. For each p-primary kernel, construct controlled Scholz solutions and solve successive central embedding problems. When an obstruction appears, Shafarevich's shrinking procedure modifies earlier stages so that the obstruction vanishes; the corrected argument handles the prime 2. Iterating along a solvable series yields a finite Galois extension K/ℚ with Galois group G."