diff --git a/formal/CoreFormalism/ChentsovFinite.lean b/formal/CoreFormalism/ChentsovFinite.lean
index 1b4b295a..6c8b7275 100644
--- a/formal/CoreFormalism/ChentsovFinite.lean
+++ b/formal/CoreFormalism/ChentsovFinite.lean
@@ -710,7 +710,7 @@ section ChentsovTheorem
 
 /-- Chentsov's theorem: IsChentsovInvariant + IsPermutationInvariant → scalar multiple of Fisher metric -/
 axiom chentsov_theorem_axiom (n : ℕ) (hn : n ≥ 3) (g : RiemannianMetric n)
-    (h_inv : IsChentsovInvariant g sorry)
+    (h_inv : IsChentsovInvariant g)
     (h_perm : IsPermutationInvariant g)
     (h_smooth : True) :
     ∃ (c : ℝ), c > 0 ∧ ∀ (p : openSimplex n) (X Y : Fin n → ℝ),
@@ -718,7 +718,7 @@ axiom chentsov_theorem_axiom (n : ℕ) (hn : n ≥ 3) (g : RiemannianMetric n)
       g.toFun p X Y = c * fisherMetric p X Y
 
 theorem chentsov_theorem (n : ℕ) (hn : n ≥ 3) (g : RiemannianMetric n)
-    (h_inv : IsChentsovInvariant g sorry)
+    (h_inv : IsChentsovInvariant g)
     (h_perm : IsPermutationInvariant g)
     (h_smooth : True) :
     ∃ (c : ℝ), c > 0 ∧ ∀ (p : openSimplex n) (X Y : Fin n → ℝ),