diff --git a/LeanEval.lean b/LeanEval.lean
index a5ae96df..0a38af4e 100644
--- a/LeanEval.lean
+++ b/LeanEval.lean
@@ -16,3 +16,4 @@ import LeanEval.NumberTheory.SmallHouse
 import LeanEval.Topology.CerfGammaFour
 import LeanEval.Topology.HomotopyGroups
 import LeanEval.Topology.SmaleConjecture
+import LeanEval.NumberTheory.KroneckerWeber
diff --git a/LeanEval/NumberTheory/KroneckerWeber.lean b/LeanEval/NumberTheory/KroneckerWeber.lean
new file mode 100644
index 00000000..40d4235e
--- /dev/null
+++ b/LeanEval/NumberTheory/KroneckerWeber.lean
@@ -0,0 +1,16 @@
+import Mathlib
+import EvalTools.Markers
+
+namespace LeanEval
+namespace NumberTheory
+
+/-- **Kronecker-Weber Theorem**. Every finite abelian extension of `ℚ` is a subfield of a cyclotomic field. -/
+@[eval_problem]
+theorem kronecker_weber (K : Type*) [Field K] [Algebra ℚ K] [FiniteDimensional ℚ K]
+    [IsGalois ℚ K] (h_ab : ∀ σ τ : K ≃ₐ[ℚ] K, σ * τ = τ * σ) :
+    ∃ (n : ℕ) (L : Type*) (_ : Field L) (_ : Algebra ℚ L) (_ : IsCyclotomicExtension {n} ℚ L),
+      Nonempty (K →ₐ[ℚ] L) := by
+  sorry
+
+end NumberTheory
+end LeanEval
diff --git a/manifests/problems/kronecker_weber.toml b/manifests/problems/kronecker_weber.toml
new file mode 100644
index 00000000..ca2d220e
--- /dev/null
+++ b/manifests/problems/kronecker_weber.toml
@@ -0,0 +1,9 @@
+id = "kronecker_weber"
+title = "Kronecker-Weber Theorem"
+test = false
+module = "LeanEval.NumberTheory.KroneckerWeber"
+holes = ["kronecker_weber"]
+submitter = "Ryan Smith"
+notes = "Every finite abelian extension of \u211a is a subfield of a cyclotomic field."
+source = "Kronecker (1853), Weber (1886), Hilbert (1896). For a modern proof using ramification theory, see Washington, L. C. (1997). 'Introduction to Cyclotomic Fields' (Graduate Texts in Mathematics 83, Springer), Chapter 14. For a proof using local class field theory, see Neukirch, J. (1999). 'Algebraic Number Theory' (Grundlehren der mathematischen Wissenschaften 322, Springer), Chapter VI."
+informal_solution = "Usually proven by reducing to the local case via class field theory or explicitly studying ramification groups. One determines the ramification index at each prime and bounds the highest power of a prime dividing the discriminant, showing the field is contained in the compositum of local cyclotomic fields, which patches together to a global cyclotomic field."