From 1419fac5871a47f9f5e2bc991f463a52426bf784 Mon Sep 17 00:00:00 2001
From: "A. M. Berns" <ansonberns@gmail.com>
Date: Mon, 18 May 2026 16:29:02 -0400
Subject: [PATCH] Add Morley categoricity

---
 LeanEval/ModelTheory/MorleyCategoricity.lean | 26 ++++++++++++++++++++
 manifests/problems.toml                      | 11 +++++++++
 2 files changed, 37 insertions(+)
 create mode 100644 LeanEval/ModelTheory/MorleyCategoricity.lean

diff --git a/LeanEval/ModelTheory/MorleyCategoricity.lean b/LeanEval/ModelTheory/MorleyCategoricity.lean
new file mode 100644
index 0000000..f831bd2
--- /dev/null
+++ b/LeanEval/ModelTheory/MorleyCategoricity.lean
@@ -0,0 +1,26 @@
+import Mathlib.ModelTheory.Satisfiability
+import EvalTools.Markers
+
+namespace LeanEval
+namespace ModelTheory
+
+open Cardinal
+
+/-!
+Morley's categoricity theorem.
+
+A complete theory in a countable language, all of whose models are infinite, that is
+categorical in some uncountable cardinal is categorical in every uncountable cardinal.  -/
+
+@[eval_problem]
+theorem morley_categoricity_theorem
+    (L : FirstOrder.Language.{0, 0}) (hL : L.card ≤ ℵ₀)
+    (T : L.Theory) (hT : T.IsComplete)
+    (hInf : ∀ M : FirstOrder.Language.Theory.ModelType.{0, 0, 0} T, Infinite M)
+    {κ : Cardinal.{0}} (hκ : ℵ₀ < κ) (hcat : κ.Categorical T)
+    {μ : Cardinal.{0}} (hμ : ℵ₀ < μ) :
+    μ.Categorical T := by
+  sorry
+
+end ModelTheory
+end LeanEval
diff --git a/manifests/problems.toml b/manifests/problems.toml
index b9e42d1..6b394ec 100644
--- a/manifests/problems.toml
+++ b/manifests/problems.toml
@@ -673,3 +673,14 @@ module = "LeanEval.Geometry.Uniformization"
 holes = ["uniformization"]
 submitter = "Junyan Xu"
 source = "John Hamal Hubbard, *Teichmüller theory and applications to geometry, topology, and dynamics. Vol. 1*, Chapter 1."
+
+[[problem]]
+id = "morley_categoricity_theorem"
+title = "Morley's categoricity theorem"
+test = false
+module = "LeanEval.ModelTheory.MorleyCategoricity"
+holes = ["morley_categoricity_theorem"]
+submitter = "A. M. Berns"
+notes = "A complete theory in a countable language with only infinite models that is categorical in some uncountable cardinal is categorical in every uncountable cardinal."
+source = "M. Ramsey, *Morley's Categoricity Theorem* (UChicago VIGRE REU 2010), Corollary 7.3. https://www.math.uchicago.edu/~may/VIGRE/VIGRE2010/REUPapers/RamseyN.pdf"
+informal_solution = "Show that categoricity in an uncountable cardinal forces the theory to be ω-stable, and then use Vaughtian pairs to prove that any two models of the same uncountable size are isomorphic and categoricity transfers to all uncountable cardinals."