diff --git a/lean4/src/putnam_2013_a5.lean b/lean4/src/putnam_2013_a5.lean
index c430f9d..23b0125 100644
--- a/lean4/src/putnam_2013_a5.lean
+++ b/lean4/src/putnam_2013_a5.lean
@@ -8,14 +8,14 @@ For $m \geq 3$, a list of $\binom{m}{3}$ real numbers $a_{ijk}$ ($1 \leq i< j< k
 -/
 theorem putnam_2013_a5
 (m : ℕ)
-(area2 : (Fin 2 → ℝ) → (Fin 2 → ℝ) → (Fin 2 → ℝ) → ℝ)
-(area3 : (Fin 3 → ℝ) → (Fin 3 → ℝ) → (Fin 3 → ℝ) → ℝ)
+(area2 : EuclideanSpace ℝ (Fin 2) → EuclideanSpace ℝ (Fin 2) → EuclideanSpace ℝ (Fin 2) → ℝ)
+(area3 : EuclideanSpace ℝ (Fin 3) → EuclideanSpace ℝ (Fin 3) → EuclideanSpace ℝ (Fin 3) → ℝ)
 (areadef2 : (Fin m → Fin m → Fin m → ℝ) → Prop)
 (areadef3 : (Fin m → Fin m → Fin m → ℝ) → Prop)
 (mge3 : m ≥ 3)
 (harea2 : ∀ a b c, area2 a b c = (volume (convexHull ℝ {a, b, c})).toReal)
 (harea3 : ∀ a b c, area3 a b c = (μH[2] (convexHull ℝ {a, b, c})).toReal)
-(hareadef2 : ∀ a, areadef2 a ↔ ∀ A : Fin m → (Fin 2 → ℝ), (∑ i : Fin m, ∑ j : Fin m, ∑ k : Fin m, if (i < j ∧ j < k) then (a i j k * area2 (A i) (A j) (A k)) else 0) ≥ 0)
-(hareadef3 : ∀ a, areadef3 a ↔ ∀ A : Fin m → (Fin 3 → ℝ), (∑ i : Fin m, ∑ j : Fin m, ∑ k : Fin m, if (i < j ∧ j < k) then (a i j k * area3 (A i) (A j) (A k)) else 0) ≥ 0)
+(hareadef2 : ∀ a, areadef2 a ↔ ∀ A : Fin m → EuclideanSpace ℝ (Fin 2), (∑ i : Fin m, ∑ j : Fin m, ∑ k : Fin m, if (i < j ∧ j < k) then (a i j k * area2 (A i) (A j) (A k)) else 0) ≥ 0)
+(hareadef3 : ∀ a, areadef3 a ↔ ∀ A : Fin m → EuclideanSpace ℝ (Fin 3), (∑ i : Fin m, ∑ j : Fin m, ∑ k : Fin m, if (i < j ∧ j < k) then (a i j k * area3 (A i) (A j) (A k)) else 0) ≥ 0)
 : ∀ a, areadef2 a → areadef3 a :=
 sorry