diff --git a/lean4/src/putnam_1962_a3.lean b/lean4/src/putnam_1962_a3.lean
index bd70d8e0..1238d2cf 100644
--- a/lean4/src/putnam_1962_a3.lean
+++ b/lean4/src/putnam_1962_a3.lean
@@ -4,13 +4,13 @@ open BigOperators
 open MeasureTheory
 
 theorem putnam_1962_a3
-(A B C A' B' C' P Q R : Fin 2 → ℝ)
+(A B C A' B' C' P Q R : EuclideanSpace ℝ (Fin 2))
 (k : ℝ)
 (hk : k > 0)
 (hABC : ¬Collinear ℝ {A, B, C})
-(hA' : A' ∈ segment ℝ B C ∧ Euclidean.dist C A' / Euclidean.dist A' B = k)
-(hB' : B' ∈ segment ℝ C A ∧ Euclidean.dist A B' / Euclidean.dist B' C = k)
-(hC' : C' ∈ segment ℝ A B ∧ Euclidean.dist B C' / Euclidean.dist C' A = k)
+(hA' : A' ∈ segment ℝ B C ∧ dist C A' / dist A' B = k)
+(hB' : B' ∈ segment ℝ C A ∧ dist A B' / dist B' C = k)
+(hC' : C' ∈ segment ℝ A B ∧ dist B C' / dist C' A = k)
 (hP : P ∈ segment ℝ B B' ∧ P ∈ segment ℝ C C')
 (hQ : Q ∈ segment ℝ C C' ∧ Q ∈ segment ℝ A A')
 (hR : R ∈ segment ℝ A A' ∧ R ∈ segment ℝ B B')
diff --git a/lean4/src/putnam_1963_a6.lean b/lean4/src/putnam_1963_a6.lean
index b2445510..473f0ef7 100644
--- a/lean4/src/putnam_1963_a6.lean
+++ b/lean4/src/putnam_1963_a6.lean
@@ -4,11 +4,11 @@ open BigOperators
 open Topology Filter
 
 theorem putnam_1963_a6
-(F1 F2 U V A B C D P Q : Fin 2 → ℝ)
+(F1 F2 U V A B C D P Q : EuclideanSpace ℝ (Fin 2))
 (r : ℝ)
-(E : Set (Fin 2 → ℝ) := {H : Fin 2 → ℝ | Euclidean.dist F1 H + Euclidean.dist F2 H = r})
-(M : Fin 2 → ℝ := midpoint ℝ U V)
-(hr : r > Euclidean.dist F1 F2)
+(E : Set (Fin 2 → ℝ) := {H : EuclideanSpace ℝ (Fin 2) | dist F1 H + dist F2 H = r})
+(M : EuclideanSpace ℝ (Fin 2) := midpoint ℝ U V)
+(hr : r > dist F1 F2)
 (hUV : U ∈ E ∧ V ∈ E ∧ U ≠ V)
 (hAB : A ∈ E ∧ B ∈ E ∧ A ≠ B)
 (hCD : C ∈ E ∧ D ∈ E ∧ C ≠ D)
diff --git a/lean4/src/putnam_1964_a1.lean b/lean4/src/putnam_1964_a1.lean
index b183015d..18098521 100644
--- a/lean4/src/putnam_1964_a1.lean
+++ b/lean4/src/putnam_1964_a1.lean
@@ -2,8 +2,8 @@ import Mathlib
 open BigOperators
 
 theorem putnam_1964_a1
-(A : Finset (Fin 2 → ℝ))
+(A : Finset (EuclideanSpace ℝ (Fin 2)))
 (hAcard : A.card = 6)
-(dists : Set ℝ := {d : ℝ | ∃ a b : Fin 2 → ℝ, a ∈ A ∧ b ∈ A ∧ a ≠ b ∧ d = Euclidean.dist a b})
+(dists : Set ℝ := {d : ℝ | ∃ a b : EuclideanSpace ℝ (Fin 2), a ∈ A ∧ b ∈ A ∧ a ≠ b ∧ d = dist a b})
 : (sSup dists / sInf dists ≥ Real.sqrt 3) :=
 sorry
diff --git a/lean4/src/putnam_1964_b6.lean b/lean4/src/putnam_1964_b6.lean
index 804dfceb..b57e9928 100644
--- a/lean4/src/putnam_1964_b6.lean
+++ b/lean4/src/putnam_1964_b6.lean
@@ -4,7 +4,7 @@ open BigOperators
 open Set Function Filter Topology
 
 theorem putnam_1964_b6
-(D : Set (Fin 2 → ℝ) := {v : Fin 2 → ℝ | Euclidean.dist 0 v ≤ 1})
-(cong : Set (Fin 2 → ℝ) → Set (Fin 2 → ℝ) → Prop := fun A B ↦ ∃ f : (Fin 2 → ℝ) → (Fin 2 → ℝ), B = f '' A ∧ ∀ v w : Fin 2 → ℝ, Euclidean.dist v w = Euclidean.dist (f v) (f w))
+(D : Set (EuclideanSpace ℝ (Fin 2)) := {v : EuclideanSpace ℝ (Fin 2) | dist 0 v ≤ 1})
+(cong : Set (EuclideanSpace ℝ (Fin 2)) → Set (EuclideanSpace ℝ (Fin 2)) → Prop := fun A B ↦ ∃ f : (EuclideanSpace ℝ (Fin 2)) → (EuclideanSpace ℝ (Fin 2)), B = f '' A ∧ ∀ v w : EuclideanSpace ℝ (Fin 2), dist v w = dist (f v) (f w))
 : (¬∃ A B : Set (Fin 2 → ℝ), cong A B ∧ A ∩ B = ∅ ∧ A ∪ B = D) :=
 sorry
diff --git a/lean4/src/putnam_1965_a1.lean b/lean4/src/putnam_1965_a1.lean
index 6ca5f0bc..a02595e3 100644
--- a/lean4/src/putnam_1965_a1.lean
+++ b/lean4/src/putnam_1965_a1.lean
@@ -3,7 +3,6 @@ open BigOperators
 
 open EuclideanGeometry
 
---TODO: (George) Double check for errors here on Lean migration to v4.9.0. Angles do not work with Fin 2 → ℝ, but dist does not work for EuclideanSpace ℝ (Fin 2).
 noncomputable abbrev putnam_1965_a1_solution : ℝ := sorry
 -- Real.pi / 15
 theorem putnam_1965_a1
@@ -11,7 +10,7 @@ theorem putnam_1965_a1
 (A B C X Y : EuclideanSpace ℝ (Fin 2))
 (hABC : ¬Collinear ℝ {A, B, C})
 (hangles : ∠ C A B < ∠ B C A ∧ ∠ B C A < π/2 ∧ π/2 < ∠ A B C)
-(hX : Collinear ℝ {X, B, C} ∧ ∠ X A B = (π - ∠ C A B)/2 ∧ (A 0 - X 0)^2 + (A 1 - X 1)^2 = (A 0 - B 0)^2 + (A 1 - B 1)^2)
-(hY : Collinear ℝ {Y, C, A} ∧ ∠ Y B C = (π - ∠ A B C)/2 ∧ (B 0 - Y 0)^2 + (B 1 - Y 1)^2 = (A 0 - B 0)^2 + (A 1 - B 1)^2)
+(hX : Collinear ℝ {X, B, C} ∧ ∠ X A B = (π - ∠ C A B)/2 ∧ dist A X = dist A B)
+(hY : Collinear ℝ {Y, C, A} ∧ ∠ Y B C = (π - ∠ A B C)/2 ∧ dist B Y = dist A B)
 : ∠ C A B = putnam_1965_a1_solution :=
 sorry
diff --git a/lean4/src/putnam_1965_b6.lean b/lean4/src/putnam_1965_b6.lean
index 3de3c3a7..c3a6e955 100644
--- a/lean4/src/putnam_1965_b6.lean
+++ b/lean4/src/putnam_1965_b6.lean
@@ -4,11 +4,11 @@ open BigOperators
 open EuclideanGeometry Topology Filter Complex SimpleGraph.Walk
 
 theorem putnam_1965_b6
-(A B C D : Fin 2 → ℝ)
-(S : Set (Fin 2 → ℝ) := {A, B, C, D})
+(A B C D : EuclideanSpace ℝ (Fin 2))
+(S : Set (EuclideanSpace ℝ (Fin 2)) := {A, B, C, D})
 (hdistinct : S.ncard = 4)
-(through : (ℝ × (Fin 2 → ℝ)) → (Fin 2 → ℝ) → Prop := fun (r, P) => fun Q => Euclidean.dist P Q = r)
-(hABCD : ∀ r s : ℝ, ∀ P Q : Fin 2 → ℝ, through (r, P) A ∧ through (r, P) B ∧ through (s, Q) C ∧ through (s, Q) D →
-∃ I : Fin 2 → ℝ, through (r, P) I ∧ through (s, Q) I)
-: Collinear ℝ S ∨ ∃ r : ℝ, ∃ P : Fin 2 → ℝ, ∀ Q ∈ S, through (r, P) Q :=
+(through : (ℝ × (EuclideanSpace ℝ (Fin 2))) → (EuclideanSpace ℝ (Fin 2)) → Prop := fun (r, P) => fun Q => dist P Q = r)
+(hABCD : ∀ r s : ℝ, ∀ P Q : EuclideanSpace ℝ (Fin 2), through (r, P) A ∧ through (r, P) B ∧ through (s, Q) C ∧ through (s, Q) D →
+∃ I : EuclideanSpace ℝ (Fin 2), through (r, P) I ∧ through (s, Q) I)
+: Collinear ℝ S ∨ ∃ r : ℝ, ∃ P : EuclideanSpace ℝ (Fin 2), ∀ Q ∈ S, through (r, P) Q :=
 sorry
diff --git a/lean4/src/putnam_1966_a2.lean b/lean4/src/putnam_1966_a2.lean
index 51ed2325..591a9249 100644
--- a/lean4/src/putnam_1966_a2.lean
+++ b/lean4/src/putnam_1966_a2.lean
@@ -3,16 +3,16 @@ open BigOperators
 
 theorem putnam_1966_a2
 (r : ℝ)
-(A B C : Fin 2 → ℝ)
+(A B C : EuclideanSpace ℝ (Fin 2))
 (hABC : ¬Collinear ℝ {A, B, C})
-(a : ℝ := Euclidean.dist B C)
-(b : ℝ := Euclidean.dist C A)
-(c : ℝ := Euclidean.dist A B)
-(p : ℝ := (Euclidean.dist B C + Euclidean.dist C A + Euclidean.dist A B)/2)
-(hr : ∃ I : Fin 2 → ℝ,
-(∃! P : Fin 2 → ℝ, Euclidean.dist I P = r ∧ Collinear ℝ {P, B, C}) ∧
-(∃! Q : EuclideanSpace ℝ (Fin 2), Euclidean.dist I Q = r ∧ Collinear ℝ {Q, C, A}) ∧
-(∃! R : EuclideanSpace ℝ (Fin 2), Euclidean.dist I R = r ∧ Collinear ℝ {R, A, B}) ∧
-(∀ Z : EuclideanSpace ℝ (Fin 2), Euclidean.dist I Z ≤ r → Z ∈ convexHull ℝ {A, B, C}))
+(a : ℝ := dist B C)
+(b : ℝ := dist C A)
+(c : ℝ := dist A B)
+(p : ℝ := (dist B C + dist C A + dist A B)/2)
+(hr : ∃ I : EuclideanSpace ℝ (Fin 2),
+(∃! P : EuclideanSpace ℝ (Fin 2), dist I P = r ∧ Collinear ℝ {P, B, C}) ∧
+(∃! Q : EuclideanSpace ℝ (Fin 2), dist I Q = r ∧ Collinear ℝ {Q, C, A}) ∧
+(∃! R : EuclideanSpace ℝ (Fin 2), dist I R = r ∧ Collinear ℝ {R, A, B}) ∧
+(∀ Z : EuclideanSpace ℝ (Fin 2), dist I Z ≤ r → Z ∈ convexHull ℝ {A, B, C}))
 : 1/(p - a)^2 + 1/(p - b)^2 + 1/(p - c)^2 ≥ 1/r^2 :=
 sorry
diff --git a/lean4/src/putnam_1966_b1.lean b/lean4/src/putnam_1966_b1.lean
index 18ff35d6..99b75543 100644
--- a/lean4/src/putnam_1966_b1.lean
+++ b/lean4/src/putnam_1966_b1.lean
@@ -6,9 +6,9 @@ open Topology Filter
 theorem putnam_1966_b1
 (n : ℕ)
 (hn : n ≥ 3)
-(L : ZMod n → (Fin 2 → ℝ))
+(L : ZMod n → (EuclideanSpace ℝ (Fin 2)))
 (hsq : ∀ i : ZMod n, L i 0 ∈ Set.Icc 0 1 ∧ L i 1 ∈ Set.Icc 0 1)
 (hnoncol : ∀ i j k : ZMod n, i ≠ j ∧ j ≠ k ∧ k ≠ i → ¬Collinear ℝ {L i, L j, L k})
 (hconvex : ∀ i : ZMod n, segment ℝ (L i) (L (i + 1)) ∩ interior (convexHull ℝ {L j | j : ZMod n}) = ∅)
-: ∑ i : Fin n, (Euclidean.dist (L i) (L (i + 1)))^2 ≤ 4 :=
+: ∑ i : Fin n, (dist (L i) (L (i + 1)))^2 ≤ 4 :=
 sorry
diff --git a/lean4/src/putnam_1967_a5.lean b/lean4/src/putnam_1967_a5.lean
index f3bfa916..8b82400d 100644
--- a/lean4/src/putnam_1967_a5.lean
+++ b/lean4/src/putnam_1967_a5.lean
@@ -4,7 +4,7 @@ open BigOperators
 open Nat Topology Filter
 
 theorem putnam_1967_a5
-(R : Set (Fin 2 → ℝ))
+(R : Set (EuclideanSpace ℝ (Fin 2)))
 (hR : Convex ℝ R ∧ (MeasureTheory.volume R).toReal > Real.pi / 4)
-: ∃ P ∈ R, ∃ Q ∈ R, Euclidean.dist P Q = 1 :=
+: ∃ P ∈ R, ∃ Q ∈ R, dist P Q = 1 :=
 sorry
diff --git a/lean4/src/putnam_1967_b1.lean b/lean4/src/putnam_1967_b1.lean
index 43e617cc..2b9032a4 100644
--- a/lean4/src/putnam_1967_b1.lean
+++ b/lean4/src/putnam_1967_b1.lean
@@ -5,14 +5,14 @@ open Nat Topology Filter
 
 theorem putnam_1967_b1
 (r : ℝ)
-(L : ZMod 6 → (Fin 2 → ℝ))
-(P : Fin 2 → ℝ := midpoint ℝ (L 1) (L 2))
-(Q : Fin 2 → ℝ := midpoint ℝ (L 3) (L 4))
-(R : Fin 2 → ℝ := midpoint ℝ (L 5) (L 0))
+(L : ZMod 6 → (EuclideanSpace ℝ (Fin 2)))
+(P : EuclideanSpace ℝ (Fin 2) := midpoint ℝ (L 1) (L 2))
+(Q : EuclideanSpace ℝ (Fin 2) := midpoint ℝ (L 3) (L 4))
+(R : EuclideanSpace ℝ (Fin 2) := midpoint ℝ (L 5) (L 0))
 (hr : r > 0)
-(hcyclic : ∃ (O : Fin 2 → ℝ), ∀ i : ZMod 6, Euclidean.dist O (L i) = r)
+(hcyclic : ∃ (O : EuclideanSpace ℝ (Fin 2)), ∀ i : ZMod 6, dist O (L i) = r)
 (horder : ∀ i j : ZMod 6, i + 1 = j ∨ i = j + 1 ∨ segment ℝ (L i) (L j) ∩ interior (convexHull ℝ {L k | k : ZMod 6}) ≠ ∅)
-(hlens : Euclidean.dist (L 0) (L 1) = r ∧ Euclidean.dist (L 2) (L 3) = r ∧ Euclidean.dist (L 4) (L 5) = r)
+(hlens : dist (L 0) (L 1) = r ∧ dist (L 2) (L 3) = r ∧ dist (L 4) (L 5) = r)
 (hdist : L 1 ≠ L 2 ∧ L 3 ≠ L 4 ∧ L 5 ≠ L 0)
-: Euclidean.dist P Q = Euclidean.dist R P ∧ Euclidean.dist Q R = Euclidean.dist P Q :=
+: dist P Q = dist R P ∧ dist Q R = dist P Q :=
 sorry
diff --git a/lean4/src/putnam_1968_a4.lean b/lean4/src/putnam_1968_a4.lean
index 24be30cc..35c37748 100644
--- a/lean4/src/putnam_1968_a4.lean
+++ b/lean4/src/putnam_1968_a4.lean
@@ -5,7 +5,7 @@ open Finset
 
 theorem putnam_1968_a4
 (n : ℕ)
-(S : Fin n → (Fin 3 → ℝ))
-(hS : ∀ i : Fin n, (S i 0)^2 + (S i 1)^2 + (S i 2)^2 = 1)
-: ∑ i : Fin n, ∑ j : Fin n, (if i < j then (Euclidean.dist (S i) (S j))^2 else (0 : ℝ)) ≤ n^2 :=
+(S : Fin n → (EuclideanSpace ℝ (Fin 3)))
+(hS : ∀ i : Fin n, dist 0 (S i) = 1)
+: ∑ i : Fin n, ∑ j : Fin n, (if i < j then (dist (S i) (S j))^2 else (0 : ℝ)) ≤ n^2 :=
 sorry
diff --git a/lean4/src/putnam_1970_b6.lean b/lean4/src/putnam_1970_b6.lean
index 5b923430..065d54ed 100644
--- a/lean4/src/putnam_1970_b6.lean
+++ b/lean4/src/putnam_1970_b6.lean
@@ -4,14 +4,14 @@ open BigOperators
 open Metric Set EuclideanGeometry Filter Topology
 
 theorem putnam_1970_b6
-(L : ZMod 4 → (Fin 2 → ℝ))
-(S : Set (Fin 2 → ℝ) := {L i | i : ZMod 4})
+(L : ZMod 4 → (EuclideanSpace ℝ (Fin 2)))
+(S : Set (EuclideanSpace ℝ (Fin 2)) := {L i | i : ZMod 4})
 (hSquad : S.ncard = 4 ∧ ∀ s ⊆ S, s.ncard = 3 → ¬ Collinear ℝ s)
-(hlens : Euclidean.dist (L 0) (L 1) > 0 ∧ Euclidean.dist (L 1) (L 2) > 0 ∧ Euclidean.dist (L 2) (L 3) > 0 ∧ Euclidean.dist (L 3) (L 0) > 0)
+(hlens : dist (L 0) (L 1) > 0 ∧ dist (L 1) (L 2) > 0 ∧ dist (L 2) (L 3) > 0 ∧ dist (L 3) (L 0) > 0)
 (horder : ∀ i : ZMod 4, segment ℝ (L i) (L (i + 1)) ∩ interior (convexHull ℝ S) = ∅)
-(hcircum : ∃ (O: Fin 2 → ℝ) (r : ℝ), O ∈ convexHull ℝ S ∧ r > 0 ∧ ∀ i : ZMod 4,
-∃! I : Fin 2 → ℝ, Collinear ℝ {I, L i, L (i + 1)} ∧ Euclidean.dist O I = r)
+(hcircum : ∃ (O: EuclideanSpace ℝ (Fin 2)) (r : ℝ), O ∈ convexHull ℝ S ∧ r > 0 ∧ ∀ i : ZMod 4,
+∃! I : EuclideanSpace ℝ (Fin 2), Collinear ℝ {I, L i, L (i + 1)} ∧ dist O I = r)
 (harea : (MeasureTheory.volume (convexHull ℝ S)).toReal =
-Real.sqrt (Euclidean.dist (L 0) (L 1) * Euclidean.dist (L 1) (L 2) * Euclidean.dist (L 2) (L 3) * Euclidean.dist (L 3) (L 0)))
+Real.sqrt (dist (L 0) (L 1) * dist (L 1) (L 2) * dist (L 2) (L 3) * dist (L 3) (L 0)))
 : Cospherical S :=
 sorry
diff --git a/lean4/src/putnam_1971_a3.lean b/lean4/src/putnam_1971_a3.lean
index 86f86051..68db8076 100644
--- a/lean4/src/putnam_1971_a3.lean
+++ b/lean4/src/putnam_1971_a3.lean
@@ -9,7 +9,7 @@ theorem putnam_1971_a3
 (habclattice : a.1 = round a.1 ∧ a.2 = round a.2 ∧ b.1 = round b.1 ∧ b.2 = round b.2 ∧ c.1 = round c.1 ∧ c.2 = round c.2)
 (habcneq : a ≠ b ∧ a ≠ c ∧ b ≠ c)
 (hR : R > 0)
-(oncircle : (ℝ × ℝ) → ℝ → (ℝ × ℝ) → Prop := fun C r p => Euclidean.dist p C = r)
+(oncircle : (ℝ × ℝ) → ℝ → (ℝ × ℝ) → Prop := fun C r p => Real.sqrt ((p.1 - C.1)^2 + (p.2 - C.2)^2) = r)
 (hcircle : ∃ C : ℝ × ℝ, oncircle C R a ∧ oncircle C R b ∧ oncircle C R c)
-: (Euclidean.dist a b) * (Euclidean.dist a c) * (Euclidean.dist b c) ≥ 2 * R :=
+: (Real.sqrt ((a.1 - b.1)^2 + (a.2 - b.2)^2)) * (Real.sqrt ((a.1 - c.1)^2 + (a.2 - c.2)^2)) * (Real.sqrt ((b.1 - c.1)^2 + (b.2 - c.2)^2)) ≥ 2 * R :=
 sorry
diff --git a/lean4/src/putnam_1972_b5.lean b/lean4/src/putnam_1972_b5.lean
index 9cb76d55..0f94adf5 100644
--- a/lean4/src/putnam_1972_b5.lean
+++ b/lean4/src/putnam_1972_b5.lean
@@ -7,6 +7,5 @@ theorem putnam_1972_b5
 (A B C D : EuclideanSpace ℝ (Fin 3))
 (hnonplanar : ¬Coplanar ℝ {A, B, C, D})
 (hangles : ∠ A B C = ∠ C D A ∧ ∠ B C D = ∠ D A B)
-(distance : (Fin 3 → ℝ) → (Fin 3 → ℝ) → ℝ := fun X Y => ∑ i, (X i - Y i)^2)
-: distance A B = distance C D ∧ distance B C = distance D A :=
+: dist A B = dist C D ∧ dist B C = dist D A :=
 sorry
diff --git a/lean4/src/putnam_1973_a1.lean b/lean4/src/putnam_1973_a1.lean
index cf95432e..b15e0902 100644
--- a/lean4/src/putnam_1973_a1.lean
+++ b/lean4/src/putnam_1973_a1.lean
@@ -4,12 +4,12 @@ open BigOperators
 open Nat Set MeasureTheory Topology Filter
 
 theorem putnam_1973_a1
-(A B C X Y Z : Fin 2 → ℝ)
+(A B C X Y Z : EuclideanSpace ℝ (Fin 2))
 (hnoncol : ¬Collinear ℝ {A, B, C})
 (hX : X ∈ segment ℝ B C)
 (hY : Y ∈ segment ℝ C A)
 (hZ : Z ∈ segment ℝ A B)
-: ((Euclidean.dist B X ≤ Euclidean.dist X C ∧ Euclidean.dist C Y ≤ Euclidean.dist Y A ∧ Euclidean.dist A Z ≤ Euclidean.dist Z B) →
+: ((dist B X ≤ dist X C ∧ dist C Y ≤ dist Y A ∧ dist A Z ≤ dist Z B) →
 volume (convexHull ℝ {X, Y, Z}) ≥ (1/4) * volume (convexHull ℝ {A, B, C})) ∧
 sInf {volume (convexHull ℝ {A, Z, Y}), volume (convexHull ℝ {B, X, Z}), volume (convexHull ℝ {C, Y, X})} ≤ volume (convexHull ℝ {X, Y, Z}) :=
 sorry
diff --git a/lean4/src/putnam_1974_b1.lean b/lean4/src/putnam_1974_b1.lean
index 387c2a6b..54809211 100644
--- a/lean4/src/putnam_1974_b1.lean
+++ b/lean4/src/putnam_1974_b1.lean
@@ -4,9 +4,9 @@ open BigOperators
 open Set Nat Polynomial
 
 abbrev putnam_1974_b1_solution : (Fin 5 → (ℝ × ℝ)) -> Prop := sorry
--- fun points => (∃ (B : ℝ) (ordering : Equiv.Perm (Fin 5)), ∀ i : Fin 5, Euclidean.dist (points (ordering i)) (points (ordering (i+1))) = B)
+-- fun points => (∃ (B : ℝ) (ordering : Equiv.Perm (Fin 5)), ∀ i : Fin 5, Real.sqrt (((points (ordering i)).1 - (points (ordering (i+1))).1)^2 + ((points (ordering i)).2 - (points (ordering (i+1))).2)^2) = B)
 theorem putnam_1974_b1
-(on_unit_circle : (Fin 5 → (ℝ × ℝ)) -> Prop := fun points => ∀ i : Fin 5, Euclidean.dist (points i) (0,0) = 1)
-(distance_fun : (Fin 5 → (ℝ × ℝ)) -> ℝ := fun points => ∑ idx : Fin 5 × Fin 5, if idx.1 < idx.2 then Euclidean.dist (points idx.1) (points idx.2) else 0)
+(on_unit_circle : (Fin 5 → (ℝ × ℝ)) -> Prop := fun points => ∀ i : Fin 5, Real.sqrt ((points i).1^2 + (points i).2^2) = 1)
+(distance_fun : (Fin 5 → (ℝ × ℝ)) -> ℝ := fun points => ∑ idx : Fin 5 × Fin 5, if idx.1 < idx.2 then Real.sqrt (((points idx.1).1 - (points idx.2).1)^2 + ((points idx.1).2 - (points idx.2).2)^2) else 0)
 : ∀ points : Fin 5 → (ℝ × ℝ), on_unit_circle points → (distance_fun points = sSup {R | ∃ pts, on_unit_circle pts ∧ R = distance_fun pts} ↔ putnam_1974_b1_solution points) :=
 sorry
diff --git a/lean4/src/putnam_1978_a6.lean b/lean4/src/putnam_1978_a6.lean
index 390c4070..dab80a08 100644
--- a/lean4/src/putnam_1978_a6.lean
+++ b/lean4/src/putnam_1978_a6.lean
@@ -4,8 +4,8 @@ open BigOperators
 open Set Real
 
 theorem putnam_1978_a6
-(S : Finset (Fin 2 → ℝ))
+(S : Finset (EuclideanSpace ℝ (Fin 2)))
 (n : ℕ := S.card)
 (npos : n > 0)
-: ({pair : Set (Fin 2 → ℝ) | ∃ P ∈ S, ∃ Q ∈ S, pair = {P, Q} ∧ Euclidean.dist P Q = 1}.ncard < 2 * (n : ℝ) ^ ((3 : ℝ) / 2)) :=
+: ({pair : Set (EuclideanSpace ℝ (Fin 2)) | ∃ P ∈ S, ∃ Q ∈ S, pair = {P, Q} ∧ dist P Q = 1}.ncard < 2 * (n : ℝ) ^ ((3 : ℝ) / 2)) :=
 sorry
diff --git a/lean4/src/putnam_1979_a4.lean b/lean4/src/putnam_1979_a4.lean
index ec89384c..32253313 100644
--- a/lean4/src/putnam_1979_a4.lean
+++ b/lean4/src/putnam_1979_a4.lean
@@ -11,6 +11,6 @@ theorem putnam_1979_a4
 (w : (Fin 2 → ℝ) × (Fin 2 → ℝ) → ℝ → (Fin 2 → ℝ) := fun (P, Q) => fun x : ℝ => fun i : Fin 2 => x * P i + (1 - x) * Q i)
 : (∀ R : Finset (Fin 2 → ℝ), ∀ B : Finset (Fin 2 → ℝ), A (R, B) → ∃ v : Finset ((Fin 2 → ℝ) × (Fin 2 → ℝ)),
 (∀ L ∈ v, ∀ M ∈ v, L ≠ M → ∀ x ∈ Icc 0 1, ∀ y ∈ Icc 0 1,
-Euclidean.dist (w (L.1, L.2) x) (w (M.1, M.2) y) ≠ 0) ∧
+Real.sqrt ((w (L.1, L.2) x 0 - w (M.1, M.2) y 0)^2 + (w (L.1, L.2) x 1 - w (M.1, M.2) y 1)^2) ≠ 0) ∧
 v.card = R.card ∧ ∀ L ∈ v, L.1 ∈ R ∧ L.2 ∈ B) ↔ putnam_1979_a4_solution :=
 sorry
diff --git a/lean4/src/putnam_1988_a4.lean b/lean4/src/putnam_1988_a4.lean
index 10cb012a..a2470935 100644
--- a/lean4/src/putnam_1988_a4.lean
+++ b/lean4/src/putnam_1988_a4.lean
@@ -6,6 +6,6 @@ open Set Filter Topology
 abbrev putnam_1988_a4_solution : Prop × Prop := sorry
 -- (True, False)
 theorem putnam_1988_a4
-(p : ℕ → Prop := fun n ↦ ∀ color : (Fin 2 → ℝ) → Fin n, ∃ p q : Fin 2 → ℝ, color p = color q ∧ Euclidean.dist p q = 1)
+(p : ℕ → Prop := fun n ↦ ∀ color : (EuclideanSpace ℝ (Fin 2)) → Fin n, ∃ p q : EuclideanSpace ℝ (Fin 2), color p = color q ∧ dist p q = 1)
 : (let (a, b) := putnam_1988_a4_solution; (p 3 ↔ a) ∧ (p 9 ↔ b)) :=
 sorry
diff --git a/lean4/src/putnam_1989_b1.lean b/lean4/src/putnam_1989_b1.lean
index 80f75f12..0721cd2b 100644
--- a/lean4/src/putnam_1989_b1.lean
+++ b/lean4/src/putnam_1989_b1.lean
@@ -6,10 +6,10 @@ open Nat
 abbrev putnam_1989_b1_solution : ℤ × ℤ × ℤ × ℤ := sorry
 -- (4, 2, -5, 3)
 theorem putnam_1989_b1
-(square : Set (Fin 2 → ℝ) := {p : Fin 2 → ℝ | ∀ i : Fin 2, p i ∈ Set.Icc 0 1})
-(edges : Set (Fin 2 → ℝ) := {p ∈ square | p 0 = 0 ∨ p 0 = 1 ∨ p 1 = 0 ∨ p 1 = 1})
-(center : Fin 2 → ℝ := (fun i : Fin 2 => 1 / 2))
-(Scloser : Set (Fin 2 → ℝ) := {p ∈ square | ∀ q ∈ edges, Euclidean.dist p center < Euclidean.dist p q})
+(square : Set (EuclideanSpace ℝ (Fin 2)) := {p : EuclideanSpace ℝ (Fin 2) | ∀ i : Fin 2, p i ∈ Set.Icc 0 1})
+(edges : Set (EuclideanSpace ℝ (Fin 2)) := {p ∈ square | p 0 = 0 ∨ p 0 = 1 ∨ p 1 = 0 ∨ p 1 = 1})
+(center : EuclideanSpace ℝ (Fin 2) := (fun i : Fin 2 => 1 / 2))
+(Scloser : Set (EuclideanSpace ℝ (Fin 2)) := {p ∈ square | ∀ q ∈ edges, dist p center < dist p q})
 : let (a, b, c, d) := putnam_1989_b1_solution; b > 0 ∧ d > 0 ∧ (¬∃ n : ℤ, n^2 = b) ∧
 (MeasureTheory.volume Scloser).toReal / (MeasureTheory.volume square).toReal = (a * Real.sqrt b + c) / d :=
 sorry
diff --git a/lean4/src/putnam_1990_a4.lean b/lean4/src/putnam_1990_a4.lean
index bb5b3ab0..3a8b0125 100644
--- a/lean4/src/putnam_1990_a4.lean
+++ b/lean4/src/putnam_1990_a4.lean
@@ -6,5 +6,5 @@ open Filter Topology Nat
 abbrev putnam_1990_a4_solution : ℕ := sorry
 -- 3
 theorem putnam_1990_a4
-: sInf {n : ℕ | ∃ S : Set (Fin 2 → ℝ), S.encard = n ∧ ∀ Q : Fin 2 → ℝ, ∃ P ∈ S, Irrational (Euclidean.dist P Q)} = putnam_1990_a4_solution :=
+: sInf {n : ℕ | ∃ S : Set (EuclideanSpace ℝ (Fin 2)), S.encard = n ∧ ∀ Q : EuclideanSpace ℝ (Fin 2), ∃ P ∈ S, Irrational (dist P Q)} = putnam_1990_a4_solution :=
 sorry
diff --git a/lean4/src/putnam_1991_a4.lean b/lean4/src/putnam_1991_a4.lean
index b8da805f..88852655 100644
--- a/lean4/src/putnam_1991_a4.lean
+++ b/lean4/src/putnam_1991_a4.lean
@@ -6,11 +6,11 @@ open Filter Topology
 abbrev putnam_1991_a4_solution : Prop := sorry
 -- True
 theorem putnam_1991_a4
-(climit : (ℕ → (Fin 2 → ℝ)) → Prop)
+(climit : (ℕ → (EuclideanSpace ℝ (Fin 2))) → Prop)
 (rareas : (ℕ → ℝ) → Prop)
-(crline : (ℕ → (Fin 2 → ℝ)) → (ℕ → ℝ) → Prop)
-(hclimit : ∀ c : ℕ → (Fin 2 → ℝ), climit c = ¬∃ (p : Fin 2 → ℝ), ∀ ε : ℝ, ε > 0 → ∃ i : ℕ, c i ∈ Metric.ball p ε)
+(crline : (ℕ → (EuclideanSpace ℝ (Fin 2))) → (ℕ → ℝ) → Prop)
+(hclimit : ∀ c : ℕ → (EuclideanSpace ℝ (Fin 2)), climit c = ¬∃ (p : EuclideanSpace ℝ (Fin 2)), ∀ ε : ℝ, ε > 0 → ∃ i : ℕ, c i ∈ Metric.ball p ε)
 (hrareas : ∀ r : ℕ → ℝ, rareas r = ∃ A : ℝ, Tendsto (fun n : ℕ => ∑ i : Fin n, Real.pi * (r i) ^ 2) atTop (𝓝 A))
-(hcrline : ∀ (c : ℕ → (Fin 2 → ℝ)) (r : ℕ → ℝ), crline c r = (∀ v w : Fin 2 → ℝ, w ≠ 0 → ∃ i : ℕ, {p : Fin 2 → ℝ | ∃ t : ℝ, p = v + t • w} ∩ Metric.closedBall (c i) (r i) ≠ ∅))
-: (∃ (c : ℕ → (Fin 2 → ℝ)) (r : ℕ → ℝ), (∀ i : ℕ, r i ≥ 0) ∧ climit c ∧ rareas r ∧ crline c r) ↔ putnam_1991_a4_solution :=
+(hcrline : ∀ (c : ℕ → (EuclideanSpace ℝ (Fin 2))) (r : ℕ → ℝ), crline c r = (∀ v w : EuclideanSpace ℝ (Fin 2), w ≠ 0 → ∃ i : ℕ, {p : EuclideanSpace ℝ (Fin 2) | ∃ t : ℝ, p = v + t • w} ∩ Metric.closedBall (c i) (r i) ≠ ∅))
+: (∃ (c : ℕ → (EuclideanSpace ℝ (Fin 2))) (r : ℕ → ℝ), (∀ i : ℕ, r i ≥ 0) ∧ climit c ∧ rareas r ∧ crline c r) ↔ putnam_1991_a4_solution :=
 sorry
diff --git a/lean4/src/putnam_1993_b5.lean b/lean4/src/putnam_1993_b5.lean
index 5b5418b9..f41cc6cc 100644
--- a/lean4/src/putnam_1993_b5.lean
+++ b/lean4/src/putnam_1993_b5.lean
@@ -2,7 +2,7 @@ import Mathlib
 open BigOperators
 
 theorem putnam_1993_b5
-(pdists : (Fin 4 → (Fin 2 → ℝ)) → Prop)
-(hpdists: ∀ p : Fin 4 → (Fin 2 → ℝ), pdists p = ∀ i j : Fin 4, i ≠ j → (Euclidean.dist (p i) (p j) = round (Euclidean.dist (p i) (p j)) ∧ Odd (round (Euclidean.dist (p i) (p j)))))
-: ¬∃ p : Fin 4 → (Fin 2 → ℝ), pdists p :=
+(pdists : (Fin 4 → (EuclideanSpace ℝ (Fin 2))) → Prop)
+(hpdists: ∀ p : Fin 4 → (EuclideanSpace ℝ (Fin 2)), pdists p = ∀ i j : Fin 4, i ≠ j → (dist (p i) (p j) = round (dist (p i) (p j)) ∧ Odd (round (dist (p i) (p j)))))
+: ¬∃ p : Fin 4 → (EuclideanSpace ℝ (Fin 2)), pdists p :=
 sorry
diff --git a/lean4/src/putnam_1994_a3.lean b/lean4/src/putnam_1994_a3.lean
index 9ff2538b..42511bd7 100644
--- a/lean4/src/putnam_1994_a3.lean
+++ b/lean4/src/putnam_1994_a3.lean
@@ -3,10 +3,9 @@ open BigOperators
 
 open Filter Topology
 
+-- Note: The formalization here differs slightly from the original problem statement, in that T is the entire triangle, not just the sides. We adopt the former interpretation because it is simpler to state and maintains the difficulty of the problem.
 theorem putnam_1994_a3
-(vec : ℝ → ℝ → (Fin 2 → ℝ))
-(T : Set (Fin 2 → ℝ) := convexHull ℝ {vec 0 0, vec 1 0, vec 0 1})
+(T : Set (EuclideanSpace ℝ (Fin 2)) := convexHull ℝ {![0,0], ![1,0], ![0,1]})
 (Tcolors : T → Fin 4)
-(hvec : ∀ x y : ℝ, (vec x y) 0 = x ∧ (vec x y) 1 = y)
-: ∃ p q : T, Tcolors p = Tcolors q ∧ Euclidean.dist p.1 q.1 ≥ 2 - Real.sqrt 2 :=
+: ∃ p q : T, Tcolors p = Tcolors q ∧ dist p.1 q.1 ≥ 2 - Real.sqrt 2 :=
 sorry
diff --git a/lean4/src/putnam_1996_a2.lean b/lean4/src/putnam_1996_a2.lean
index 35b048cb..a52d054e 100644
--- a/lean4/src/putnam_1996_a2.lean
+++ b/lean4/src/putnam_1996_a2.lean
@@ -1,12 +1,14 @@
 import Mathlib
 open BigOperators
 
-abbrev putnam_1996_a2_solution : (Fin 2 → ℝ) → (Fin 2 → ℝ) → Set (Fin 2 → ℝ) := sorry
--- (fun O1 O2 : Fin 2 → ℝ => {p : Fin 2 → ℝ | Euclidean.dist p (midpoint ℝ O1 O2) ≥ 1 ∧ Euclidean.dist p (midpoint ℝ O1 O2) ≤ 2})
+open Metric
+
+abbrev putnam_1996_a2_solution : (EuclideanSpace ℝ (Fin 2)) → (EuclideanSpace ℝ (Fin 2)) → Set (EuclideanSpace ℝ (Fin 2)) := sorry
+-- (fun O1 O2 : EuclideanSpace ℝ (Fin 2) => {p : EuclideanSpace ℝ (Fin 2) | dist p (midpoint ℝ O1 O2) ≥ 1 ∧ dist p (midpoint ℝ O1 O2) ≤ 2})
 theorem putnam_1996_a2
-(O1 O2 : Fin 2 → ℝ)
-(C1 : Set (Fin 2 → ℝ) := {p : Fin 2 → ℝ | Euclidean.dist p O1 = 1})
-(C2 : Set (Fin 2 → ℝ) := {p : Fin 2 → ℝ | Euclidean.dist p O2 = 3})
-(hO1O2 : Euclidean.dist O1 O2 = 10)
-: {M : Fin 2 → ℝ | ∃ X Y : Fin 2 → ℝ, X ∈ C1 ∧ Y ∈ C2 ∧ M = midpoint ℝ X Y} = putnam_1996_a2_solution O1 O2 :=
+(O1 O2 : EuclideanSpace ℝ (Fin 2))
+(C1 : Set (EuclideanSpace ℝ (Fin 2)) := sphere O1 1)
+(C2 : Set (EuclideanSpace ℝ (Fin 2)) := sphere O2 3)
+(hO1O2 : dist O1 O2 = 10)
+: {M : EuclideanSpace ℝ (Fin 2) | ∃ X Y : Fin 2 → ℝ, X ∈ C1 ∧ Y ∈ C2 ∧ M = midpoint ℝ X Y} = putnam_1996_a2_solution O1 O2 :=
 sorry
diff --git a/lean4/src/putnam_1998_a2.lean b/lean4/src/putnam_1998_a2.lean
index 004bb52c..f2a6050a 100644
--- a/lean4/src/putnam_1998_a2.lean
+++ b/lean4/src/putnam_1998_a2.lean
@@ -2,10 +2,10 @@ import Mathlib
 open BigOperators
 
 theorem putnam_1998_a2
-(quadrant : (Fin 2 → ℝ) → Prop := fun P ↦ P 0 > 0 ∧ P 1 > 0 ∧ Euclidean.dist 0 P = 1)
-(isarc : (Fin 2 → ℝ) → (Fin 2 → ℝ) → Prop := fun P Q ↦ quadrant P ∧ quadrant Q ∧ P 0 > Q 0)
-(arc : (Fin 2 → ℝ) → (Fin 2 → ℝ) → Set (Fin 2 → ℝ) := fun P Q ↦ {R : Fin 2 → ℝ | quadrant R ∧ P 0 > R 0 ∧ R 0 > Q 0})
-(A : (Fin 2 → ℝ) → (Fin 2 → ℝ) → ℝ := fun P Q ↦ (MeasureTheory.volume {S : Fin 2 → ℝ | ∃ R ∈ arc P Q, R 0 = S 0 ∧ R 1 > S 1 ∧ S 1 > 0}).toReal)
-(B : (Fin 2 → ℝ) → (Fin 2 → ℝ) → ℝ := fun P Q ↦ (MeasureTheory.volume {S : Fin 2 → ℝ | ∃ R ∈ arc P Q, R 1 = S 1 ∧ R 0 > S 0 ∧ S 0 > 0}).toReal)
-: (∃ f : ℝ → ℝ, ∀ P Q : (Fin 2 → ℝ), isarc P Q → A P Q + B P Q = f (InnerProductGeometry.angle (toEuclidean P) (toEuclidean Q))) :=
+(quadrant : (EuclideanSpace ℝ (Fin 2)) → Prop := fun P ↦ P 0 > 0 ∧ P 1 > 0 ∧ dist 0 P = 1)
+(isarc : (EuclideanSpace ℝ (Fin 2)) → (EuclideanSpace ℝ (Fin 2)) → Prop := fun P Q ↦ quadrant P ∧ quadrant Q ∧ P 0 > Q 0)
+(arc : (EuclideanSpace ℝ (Fin 2)) → (EuclideanSpace ℝ (Fin 2)) → Set (EuclideanSpace ℝ (Fin 2)) := fun P Q ↦ {R : EuclideanSpace ℝ (Fin 2) | quadrant R ∧ P 0 > R 0 ∧ R 0 > Q 0})
+(A : (EuclideanSpace ℝ (Fin 2)) → (EuclideanSpace ℝ (Fin 2)) → ℝ := fun P Q ↦ (MeasureTheory.volume {S : EuclideanSpace ℝ (Fin 2) | ∃ R ∈ arc P Q, R 0 = S 0 ∧ R 1 > S 1 ∧ S 1 > 0}).toReal)
+(B : (EuclideanSpace ℝ (Fin 2)) → (EuclideanSpace ℝ (Fin 2)) → ℝ := fun P Q ↦ (MeasureTheory.volume {S : EuclideanSpace ℝ (Fin 2) | ∃ R ∈ arc P Q, R 1 = S 1 ∧ R 0 > S 0 ∧ S 0 > 0}).toReal)
+: (∃ f : ℝ → ℝ, ∀ P Q : EuclideanSpace ℝ (Fin 2), isarc P Q → A P Q + B P Q = f (InnerProductGeometry.angle P Q)) :=
 sorry
diff --git a/lean4/src/putnam_1998_a5.lean b/lean4/src/putnam_1998_a5.lean
index b33cdfb1..03721654 100644
--- a/lean4/src/putnam_1998_a5.lean
+++ b/lean4/src/putnam_1998_a5.lean
@@ -5,10 +5,10 @@ open Set Function Metric
 
 theorem putnam_1998_a5
 (k : ℕ)
-(c : Fin k → (ℝ × ℝ))
+(c : Fin k → (EuclideanSpace ℝ (Fin 2)))
 (r : Fin k → ℝ)
 (hr : ∀ i : Fin k, r i > 0)
-(E : Set (ℝ × ℝ))
+(E : Set (EuclideanSpace ℝ (Fin 2)))
 (hE : E ⊆ ⋃ i : Fin k, ball (c i) (r i))
 : ∃ (n : ℕ) (t : Fin n → Fin k), (∀ i j : Fin n, i ≠ j → (ball (c (t i)) (r (t i)) ∩ ball (c (t j)) (r (t j)) = ∅)) ∧ E ⊆ ⋃ i : Fin n, ball (c (t i)) (3 * (r (t i))) :=
 sorry
diff --git a/lean4/src/putnam_1998_a6.lean b/lean4/src/putnam_1998_a6.lean
index 83f15c3e..cc0f8e86 100644
--- a/lean4/src/putnam_1998_a6.lean
+++ b/lean4/src/putnam_1998_a6.lean
@@ -4,10 +4,10 @@ open BigOperators
 open Set Function Metric
 
 theorem putnam_1998_a6
-(A B C : Fin 2 → ℝ)
+(A B C : EuclideanSpace ℝ (Fin 2))
 (hint : ∀ i : Fin 2, ∃ a b c : ℤ, A i = a ∧ B i = b ∧ C i = c)
 (htriangle : A ≠ B ∧ A ≠ C ∧ B ≠ C)
-(harea : (Euclidean.dist A B + Euclidean.dist B C) ^ 2 < 8 * (MeasureTheory.volume (convexHull ℝ {A, B, C})).toReal + 1)
-(threesquare : (Fin 2 → ℝ) → (Fin 2 → ℝ) → (Fin 2 → ℝ) → Prop := fun P Q R ↦ Euclidean.dist Q P = Euclidean.dist Q R ∧ Matrix.dotProduct (P - Q) (R - Q) = 0)
+(harea : (dist A B + dist B C) ^ 2 < 8 * (MeasureTheory.volume (convexHull ℝ {A, B, C})).toReal + 1)
+(threesquare : (EuclideanSpace ℝ (Fin 2)) → (EuclideanSpace ℝ (Fin 2)) → (EuclideanSpace ℝ (Fin 2)) → Prop := fun P Q R ↦ dist Q P = dist Q R ∧ Matrix.dotProduct (P - Q) (R - Q) = 0)
 : (threesquare A B C ∨ threesquare B C A ∨ threesquare C A B) :=
 sorry
diff --git a/lean4/src/putnam_1998_b2.lean b/lean4/src/putnam_1998_b2.lean
index 99c7c3fe..2fc79427 100644
--- a/lean4/src/putnam_1998_b2.lean
+++ b/lean4/src/putnam_1998_b2.lean
@@ -8,9 +8,9 @@ noncomputable abbrev putnam_1998_b2_solution : ℝ → ℝ → ℝ := sorry
 theorem putnam_1998_b2
 (a b : ℝ)
 (hab : 0 < b ∧ b < a)
-: sInf {d : ℝ | ∃ (c : ℝ) (x : ℝ), d = Euclidean.dist (a, b) (c, 0) + Euclidean.dist (c, 0) (x, x) + Euclidean.dist (a, b) (x, x) ∧
-  Euclidean.dist (a, b) (c, 0) + Euclidean.dist (c, 0) (x, x) > Euclidean.dist (a, b) (x, x) ∧
-  Euclidean.dist (a, b) (c, 0) + Euclidean.dist (a, b) (x, x) > Euclidean.dist (c, 0) (x, x) ∧
-  Euclidean.dist (c, 0) (x, x) + Euclidean.dist (a, b) (x, x) > Euclidean.dist (a, b) (c, 0)}
+: sInf {d : ℝ | ∃ (c : ℝ) (x : ℝ), d = Real.sqrt ((a - c)^2 + (b - 0)^2) +  Real.sqrt ((c - x)^2 + (0 - x)^2) + Real.sqrt ((a - x)^2 + (b - x)^2) ∧
+  Real.sqrt ((a - c)^2 + (b - 0)^2) + Real.sqrt ((c - x)^2 + (0 - x)^2) > Real.sqrt ((a - x)^2 + (b - x)^2) ∧
+  Real.sqrt ((a - c)^2 + (b - 0)^2) + Real.sqrt ((a - x)^2 + (b - x)^2) > Real.sqrt ((c - x)^2 + (0 - x)^2) ∧
+  Real.sqrt ((c - x)^2 + (0 - x)^2) + Real.sqrt ((a - x)^2 + (b - x)^2) > Real.sqrt ((a - c)^2 + (b - 0)^2)}
  = putnam_1998_b2_solution a b :=
 sorry
diff --git a/lean4/src/putnam_2000_a5.lean b/lean4/src/putnam_2000_a5.lean
index f0815469..2012e609 100644
--- a/lean4/src/putnam_2000_a5.lean
+++ b/lean4/src/putnam_2000_a5.lean
@@ -5,8 +5,8 @@ open Topology Filter
 
 theorem putnam_2000_a5
 (r : ℝ)
-(z : Fin 2 → ℝ)
-(p : Fin 3 → (Fin 2 → ℝ))
+(z : EuclideanSpace ℝ (Fin 2))
+(p : Fin 3 → (EuclideanSpace ℝ (Fin 2)))
 (rpos : r > 0)
 (pdiff : ∀ n m : Fin 3, (n ≠ m) → (p n ≠ p m))
 (pint : ∀ (n : Fin 3) (i : Fin 2), p n i = round (p n i))
diff --git a/lean4/src/putnam_2002_a2.lean b/lean4/src/putnam_2002_a2.lean
index 9b4d2c9f..15fe366c 100644
--- a/lean4/src/putnam_2002_a2.lean
+++ b/lean4/src/putnam_2002_a2.lean
@@ -1,10 +1,10 @@
 import Mathlib
 open BigOperators
 
-open Nat
+open Nat Metric
 
 theorem putnam_2002_a2
-(sphere : Set (Fin 3 → ℝ) := {P : Fin 3 → ℝ | Euclidean.dist 0 P = 1})
-(hemi : (Fin 3 → ℝ) → Set (Fin 3 → ℝ) := fun V ↦ {P : Fin 3 → ℝ | Matrix.dotProduct P V ≥ 0})
-: (∀ (S : Set (Fin 3 → ℝ)), S ⊆ sphere ∧ S.encard = 5 → ∃ V : (Fin 3 → ℝ), V ≠ 0 ∧ (S ∩ hemi V).encard ≥ 4) :=
+(sphere : Set (EuclideanSpace ℝ (Fin 3)) := sphere 0 1)
+(hemi : (EuclideanSpace ℝ (Fin 3)) → Set (EuclideanSpace ℝ (Fin 3)) := fun V ↦ {P : EuclideanSpace ℝ (Fin 3) | Matrix.dotProduct P V ≥ 0})
+: (∀ (S : Set (EuclideanSpace ℝ (Fin 3))), S ⊆ sphere ∧ S.encard = 5 → ∃ V : (EuclideanSpace ℝ (Fin 3)), V ≠ 0 ∧ (S ∩ hemi V).encard ≥ 4) :=
 sorry
diff --git a/lean4/src/putnam_2003_b5.lean b/lean4/src/putnam_2003_b5.lean
index 0f099719..216b5822 100644
--- a/lean4/src/putnam_2003_b5.lean
+++ b/lean4/src/putnam_2003_b5.lean
@@ -4,9 +4,9 @@ open BigOperators
 open MvPolynomial Set Nat
 
 theorem putnam_2003_b5
-(A B C : Fin 2 → ℝ)
-(hABC : Euclidean.dist 0 A = 1 ∧ Euclidean.dist 0 B = 1 ∧ Euclidean.dist 0 C = 1 ∧ Euclidean.dist A B = Euclidean.dist A C ∧ Euclidean.dist A B = Euclidean.dist B C)
-: (∃ f : ℝ → ℝ, ∀ P : Fin 2 → ℝ, Euclidean.dist 0 P < 1 → ∃ X Y Z : Fin 2 → ℝ,
-      Euclidean.dist X Y = Euclidean.dist P A ∧ Euclidean.dist Y Z = Euclidean.dist P B ∧ Euclidean.dist X Z = Euclidean.dist P C ∧
-      (MeasureTheory.volume (convexHull ℝ {X, Y, Z})).toReal = f (Euclidean.dist 0 P)) :=
+(A B C : EuclideanSpace ℝ (Fin 2))
+(hABC : dist 0 A = 1 ∧ dist 0 B = 1 ∧ dist 0 C = 1 ∧ dist A B = dist A C ∧ dist A B = dist B C)
+: (∃ f : ℝ → ℝ, ∀ P : EuclideanSpace ℝ (Fin 2), dist 0 P < 1 → ∃ X Y Z : EuclideanSpace ℝ (Fin 2),
+      dist X Y = dist P A ∧ dist Y Z = dist P B ∧ dist X Z = dist P C ∧
+      (MeasureTheory.volume (convexHull ℝ {X, Y, Z})).toReal = f (dist 0 P)) :=
 sorry
diff --git a/lean4/src/putnam_2006_b1.lean b/lean4/src/putnam_2006_b1.lean
index 777176a4..9cd598cf 100644
--- a/lean4/src/putnam_2006_b1.lean
+++ b/lean4/src/putnam_2006_b1.lean
@@ -5,6 +5,6 @@ noncomputable abbrev putnam_2006_b1_solution : ℝ := sorry
 -- 3 * Real.sqrt 3 / 2
 theorem putnam_2006_b1
 (curve : Set (ℝ × ℝ) := {(x, y) | x ^ 3 + 3 * x * y + y ^ 3 = 1})
-(equilateral : Set (ℝ × ℝ) → Prop := fun S ↦ S.encard = 3 ∧ ∃ d : ℝ, ∀ P ∈ S, ∀ Q ∈ S, P ≠ Q → Euclidean.dist P Q = d)
+(equilateral : Set (ℝ × ℝ) → Prop := fun S ↦ S.encard = 3 ∧ ∃ d : ℝ, ∀ P ∈ S, ∀ Q ∈ S, P ≠ Q → Real.sqrt ((P.1 - Q.1)^2 + (P.2 - Q.2)^2) = d)
 : ((∃! S : Set (ℝ × ℝ), S ⊆ curve ∧ equilateral S) ∧ (∃ S : Set (ℝ × ℝ), S ⊆ curve ∧ equilateral S ∧ (MeasureTheory.volume (convexHull ℝ S)).toReal = putnam_2006_b1_solution)) :=
 sorry
diff --git a/lean4/src/putnam_2008_b1.lean b/lean4/src/putnam_2008_b1.lean
index 1a361b31..e0e3dcc1 100644
--- a/lean4/src/putnam_2008_b1.lean
+++ b/lean4/src/putnam_2008_b1.lean
@@ -6,8 +6,8 @@ open Filter Topology Set
 abbrev putnam_2008_b1_solution : ℕ := sorry
 -- 2
 def is_rational_point (p : Fin 2 → ℝ) : Prop := ∃ (a b : ℚ), a = p 0 ∧ b = p 1
-def real_circle (c : Fin 2 → ℝ) (r : ℝ) : Set (Fin 2 → ℝ) := {p : Fin 2 → ℝ | Euclidean.dist p c = r}
+def real_circle (c : EuclideanSpace ℝ (Fin 2)) (r : ℝ) : Set (EuclideanSpace ℝ (Fin 2)) := {p | dist p c = r}
 theorem putnam_2008_b1 :
-∀ (c : Fin 2 → ℝ) (r : ℝ), ¬ is_rational_point c → (Set.ncard {p : Fin 2 → ℝ | p ∈ real_circle c r ∧ is_rational_point p} ≤ putnam_2008_b1_solution)
-∧ ∃ (c : Fin 2 → ℝ) (r : ℝ), ¬ is_rational_point c ∧ (Set.ncard {p : Fin 2 → ℝ | p ∈ real_circle c r ∧ is_rational_point p} = putnam_2008_b1_solution) :=
+∀ (c : EuclideanSpace ℝ (Fin 2)) (r : ℝ), ¬ is_rational_point c → (Set.ncard {p : EuclideanSpace ℝ (Fin 2) | p ∈ real_circle c r ∧ is_rational_point p} ≤ putnam_2008_b1_solution)
+∧ ∃ (c : EuclideanSpace ℝ (Fin 2)) (r : ℝ), ¬ is_rational_point c ∧ (Set.ncard {p : EuclideanSpace ℝ (Fin 2) | p ∈ real_circle c r ∧ is_rational_point p} = putnam_2008_b1_solution) :=
 sorry
diff --git a/lean4/src/putnam_2008_b3.lean b/lean4/src/putnam_2008_b3.lean
index df6ad24e..fc1acfbb 100644
--- a/lean4/src/putnam_2008_b3.lean
+++ b/lean4/src/putnam_2008_b3.lean
@@ -6,7 +6,7 @@ open Filter Topology Set Nat
 noncomputable abbrev putnam_2008_b3_solution : ℝ := sorry
 -- Real.sqrt 2 / 2
 theorem putnam_2008_b3
-(hypercube : Set (Fin 4 → ℝ) := {P : Fin 4 → ℝ | ∀ i : Fin 4, |P i| ≤ 1 / 2})
-(contains : ℝ → (Fin 4 → ℝ) → (Fin 4 → ℝ) → (Fin 4 → ℝ) → Prop := fun r O P Q ↦ ∀ s t : ℝ, (s • P + t • Q ≠ 0 ∧ Euclidean.dist 0 (s • P + t • Q) = r) → O + s • P + t • Q ∈ hypercube)
+(hypercube : Set (EuclideanSpace ℝ (Fin 4)) := {P : Fin 4 → ℝ | ∀ i : Fin 4, |P i| ≤ 1 / 2})
+(contains : ℝ → (EuclideanSpace ℝ (Fin 4)) → (EuclideanSpace ℝ (Fin 4)) → (EuclideanSpace ℝ (Fin 4)) → Prop := fun r O P Q ↦ ∀ s t : ℝ, (s • P + t • Q ≠ 0 ∧ dist 0 (s • P + t • Q) = r) → O + s • P + t • Q ∈ hypercube)
 : (∃ O P Q, contains putnam_2008_b3_solution O P Q) ∧ (∀ r > putnam_2008_b3_solution, ¬∃ O P Q, contains r O P Q) :=
 sorry
diff --git a/lean4/src/putnam_2009_b4.lean b/lean4/src/putnam_2009_b4.lean
index a19e7aa0..64009b17 100644
--- a/lean4/src/putnam_2009_b4.lean
+++ b/lean4/src/putnam_2009_b4.lean
@@ -6,7 +6,7 @@ open Topology MvPolynomial Filter Set Metric
 abbrev putnam_2009_b4_solution : ℕ := sorry
 -- 2020050
 theorem putnam_2009_b4
-(balanced : MvPolynomial (Fin 2) ℝ → Prop := fun P ↦ ∀ r > 0, (∫ x in Metric.sphere 0 r, MvPolynomial.eval x P) / (2 * Real.pi * r) = 0)
+(balanced : MvPolynomial (Fin 2) ℝ → Prop := fun P ↦ ∀ r > 0, (∫ x in Metric.sphere (0 : EuclideanSpace ℝ (Fin 2)) r, MvPolynomial.eval x P) / (2 * Real.pi * r) = 0)
 (V : Set (MvPolynomial (Fin 2) ℝ)) [AddCommGroup V] [Module ℝ V]
 (hV : ∀ P : MvPolynomial (Fin 2) ℝ, P ∈ V ↔ balanced P ∧ P.totalDegree ≤ 2009)
 : (Module.rank V = putnam_2009_b4_solution) :=
diff --git a/lean4/src/putnam_2010_b2.lean b/lean4/src/putnam_2010_b2.lean
index e4b7b07a..9114c4ca 100644
--- a/lean4/src/putnam_2010_b2.lean
+++ b/lean4/src/putnam_2010_b2.lean
@@ -2,15 +2,14 @@ import Mathlib
 open BigOperators
 
 open Filter Topology Set
-
 abbrev putnam_2010_b2_solution : ℕ := sorry
 -- 3
 theorem putnam_2010_b2
-(ABCintcoords : (Fin 2 → ℝ) → (Fin 2 → ℝ) → (Fin 2 → ℝ) → Prop)
-(ABCintdists : (Fin 2 → ℝ) → (Fin 2 → ℝ) → (Fin 2 → ℝ) → Prop)
-(ABCall : (Fin 2 → ℝ) → (Fin 2 → ℝ) → (Fin 2 → ℝ) → Prop)
-(hABCintcoords : ∀ A B C : Fin 2 → ℝ, ABCintcoords A B C = (∀ i : Fin 2, A i = round (A i) ∧ B i = round (B i) ∧ C i = round (C i)))
-(hABCintdists : ∀ A B C : Fin 2 → ℝ, ABCintdists A B C = (Euclidean.dist A B = round (Euclidean.dist A B) ∧ Euclidean.dist A C = round (Euclidean.dist A C) ∧ Euclidean.dist B C = round (Euclidean.dist B C)))
-(hABCall : ∀ A B C : Fin 2 → ℝ, ABCall A B C = (¬Collinear ℝ {A, B, C} ∧ ABCintcoords A B C ∧ ABCintdists A B C))
-: (∃ A B C : Fin 2 → ℝ, ABCall A B C ∧ Euclidean.dist A B = putnam_2010_b2_solution) ∧ (∀ A B C : Fin 2 → ℝ, ABCall A B C → Euclidean.dist A B ≥ putnam_2010_b2_solution) :=
+(ABCintcoords : EuclideanSpace ℝ (Fin 2) → EuclideanSpace ℝ (Fin 2) → EuclideanSpace ℝ (Fin 2) → Prop)
+(ABCintdists : EuclideanSpace ℝ (Fin 2) → EuclideanSpace ℝ (Fin 2) → EuclideanSpace ℝ (Fin 2) → Prop)
+(ABCall : EuclideanSpace ℝ (Fin 2) → EuclideanSpace ℝ (Fin 2) → EuclideanSpace ℝ (Fin 2) → Prop)
+(hABCintcoords : ∀ A B C : EuclideanSpace ℝ (Fin 2), ABCintcoords A B C = (∀ i : Fin 2, A i = round (A i) ∧ B i = round (B i) ∧ C i = round (C i)))
+(hABCintdists : ∀ A B C : EuclideanSpace ℝ (Fin 2), ABCintdists A B C = (dist A B = round (dist A B) ∧ dist A C = round (dist A C) ∧ dist B C = round (dist B C)))
+(hABCall : ∀ A B C : EuclideanSpace ℝ (Fin 2), ABCall A B C = (¬Collinear ℝ {A, B, C} ∧ ABCintcoords A B C ∧ ABCintdists A B C))
+: (∃ A B C : EuclideanSpace ℝ (Fin 2), ABCall A B C ∧ dist A B = putnam_2010_b2_solution) ∧ (∀ A B C : EuclideanSpace ℝ (Fin 2), ABCall A B C → dist A B ≥ putnam_2010_b2_solution) :=
 sorry
diff --git a/lean4/src/putnam_2018_a6.lean b/lean4/src/putnam_2018_a6.lean
index a7e677b0..88bdcbab 100644
--- a/lean4/src/putnam_2018_a6.lean
+++ b/lean4/src/putnam_2018_a6.lean
@@ -2,8 +2,8 @@ import Mathlib
 open BigOperators
 
 theorem putnam_2018_a6
-(A B C D : Fin 2 → ℝ)
-(PPprops : (Fin 2 → ℝ) → (Fin 2 → ℝ) → Prop := (fun P1 P2 : Fin 2 → ℝ => P1 ≠ P2 ∧ (∃ q : ℚ, (Euclidean.dist P1 P2) ^ 2 = q)))
+(A B C D : EuclideanSpace ℝ (Fin 2))
+(PPprops : (EuclideanSpace ℝ (Fin 2)) → (EuclideanSpace ℝ (Fin 2)) → Prop := (fun P1 P2 : EuclideanSpace ℝ (Fin 2) => P1 ≠ P2 ∧ (∃ q : ℚ, (dist P1 P2) ^ 2 = q)))
 (ABCDnoline : ¬Collinear ℝ {A, B, C} ∧ ¬Collinear ℝ {A, B, D} ∧ ¬Collinear ℝ {A, C, D} ∧ ¬Collinear ℝ {B, C, D})
 (ABCDsqrrat : PPprops A B ∧ PPprops A C ∧ PPprops A D ∧ PPprops B C ∧ PPprops B D ∧ PPprops C D)
 : ∃ q : ℚ, (MeasureTheory.volume (convexHull ℝ {A, B, C}) / MeasureTheory.volume (convexHull ℝ {A, B, D})).toReal = q :=
diff --git a/lean4/src/putnam_2019_a4.lean b/lean4/src/putnam_2019_a4.lean
index d1cf354d..b9e86547 100644
--- a/lean4/src/putnam_2019_a4.lean
+++ b/lean4/src/putnam_2019_a4.lean
@@ -6,7 +6,7 @@ open Topology Filter
 abbrev putnam_2019_a4_solution : Prop := sorry
 -- False
 theorem putnam_2019_a4
-(fint : ((Fin 3 → ℝ) → ℝ) → Prop)
-(hfint : ∀ f : (Fin 3 → ℝ) → ℝ, fint f = (∀ S : Fin 3 → ℝ, (∫ x in {p : Fin 3 → ℝ | Euclidean.dist p S = 1}, f x) = 0))
-: (∀ f : (Fin 3 → ℝ) → ℝ, (Continuous f ∧ fint f) → (∀ x : Fin 3 → ℝ, f x = 0)) ↔ putnam_2019_a4_solution :=
+(fint : ((EuclideanSpace ℝ (Fin 3)) → ℝ) → Prop)
+(hfint : ∀ f : (EuclideanSpace ℝ (Fin 3)) → ℝ, fint f = (∀ S : EuclideanSpace ℝ (Fin 3), (∫ x in {p : EuclideanSpace ℝ (Fin 3) | dist p S = 1}, f x) = 0))
+: (∀ f : (EuclideanSpace ℝ (Fin 3)) → ℝ, (Continuous f ∧ fint f) → (∀ x : EuclideanSpace ℝ (Fin 3), f x = 0)) ↔ putnam_2019_a4_solution :=
 sorry
diff --git a/lean4/src/putnam_2021_a3.lean b/lean4/src/putnam_2021_a3.lean
index d9fd14dc..847af9d4 100644
--- a/lean4/src/putnam_2021_a3.lean
+++ b/lean4/src/putnam_2021_a3.lean
@@ -7,9 +7,9 @@ abbrev putnam_2021_a3_solution : Set ℕ := sorry
 -- {3 * m ^ 2 | m > 0}
 theorem putnam_2021_a3
 (N : ℕ)
-(Nsphere : Set (Fin 3 → ℝ) := {p : Fin 3 → ℝ | (p 0) ^ 2 + (p 1) ^ 2 + (p 2) ^ 2 = N})
-(intcoords : (Fin 3 → ℝ) → Prop := (fun p : Fin 3 → ℝ => ∀ i : Fin 3, p i = round (p i)))
-(Ntetra : Prop := ∃ A B C D : Fin 3 → ℝ, A ∈ Nsphere ∧ B ∈ Nsphere ∧ C ∈ Nsphere ∧ D ∈ Nsphere ∧ intcoords A ∧ intcoords B ∧ intcoords C ∧ intcoords D ∧
-(∃ s > 0, Euclidean.dist A B = s ∧ Euclidean.dist A C = s ∧ Euclidean.dist A D = s ∧ Euclidean.dist B C = s ∧ Euclidean.dist B D = s ∧ Euclidean.dist C D = s))
+(Nsphere : Set (EuclideanSpace ℝ (Fin 3)) := {p : EuclideanSpace ℝ (Fin 3) | (p 0) ^ 2 + (p 1) ^ 2 + (p 2) ^ 2 = (N : ℝ)})
+(intcoords : (EuclideanSpace ℝ (Fin 3)) → Prop := (fun p : EuclideanSpace ℝ (Fin 3) => ∀ i : Fin 3, p i = round (p i)))
+(Ntetra : Prop := ∃ A B C D : EuclideanSpace ℝ (Fin 3), A ∈ Nsphere ∧ B ∈ Nsphere ∧ C ∈ Nsphere ∧ D ∈ Nsphere ∧ intcoords A ∧ intcoords B ∧ intcoords C ∧ intcoords D ∧
+  (∃ s > 0, dist A B = s ∧ dist A C = s ∧ dist A D = s ∧ dist B C = s ∧ dist B D = s ∧ dist C D = s))
 : (N > 0 ∧ Ntetra) ↔ N ∈ putnam_2021_a3_solution :=
 sorry
diff --git a/lean4/src/putnam_2021_b3.lean b/lean4/src/putnam_2021_b3.lean
index 36fc010a..96355245 100644
--- a/lean4/src/putnam_2021_b3.lean
+++ b/lean4/src/putnam_2021_b3.lean
@@ -1,14 +1,12 @@
 import Mathlib
 open BigOperators
 
-open Filter Topology
+open Filter Topology Metric
 
 abbrev putnam_2021_b3_solution : Prop := sorry
 -- True
 theorem putnam_2021_b3
-(vec : ℝ → ℝ → (Fin 2 → ℝ))
-(rho : ((Fin 2 → ℝ) → ℝ) → (Fin 2 → ℝ) → ℝ := (fun (h : (Fin 2 → ℝ) → ℝ) (p : Fin 2 → ℝ) => (p 1) * deriv (fun x' : ℝ => h (vec x' (p 1))) (p 0) - (p 0) * deriv (fun y' : ℝ => h (vec (p 0) y')) (p 1)))
-(circint : (Fin 2 → ℝ) → ℝ → Set (Fin 2 → ℝ) := (fun (c : Fin 2 → ℝ) (r : ℝ) => {p : Fin 2 → ℝ | Euclidean.dist p c < r}))
-(hvec : ∀ x y : ℝ, (vec x y) 0 = x ∧ (vec x y 1) = y)
-: (∀ h : (Fin 2 → ℝ) → ℝ, ContDiff ℝ 2 h → (∀ d > 0, ∀ r > 0, d > r → (∃ c : Fin 2 → ℝ, Euclidean.dist c 0 = d ∧ (∫ p in (circint c r), rho h p) = 0))) ↔ putnam_2021_b3_solution :=
+(rho : ((EuclideanSpace ℝ (Fin 2)) → ℝ) → (EuclideanSpace ℝ (Fin 2)) → ℝ := (fun (h : (EuclideanSpace ℝ (Fin 2)) → ℝ) (p : EuclideanSpace ℝ (Fin 2)) => (p 1) * deriv (fun x' : ℝ => h (![x', p 1])) (p 0) - (p 0) * deriv (fun y' : ℝ => h (![p 0, y'])) (p 1)))
+(circint : (EuclideanSpace ℝ (Fin 2)) → ℝ → Set (EuclideanSpace ℝ (Fin 2)) := (fun (c : EuclideanSpace ℝ (Fin 2)) (r : ℝ) => ball c r))
+: (∀ h : (EuclideanSpace ℝ (Fin 2)) → ℝ, ContDiff ℝ 2 h → (∀ d > 0, ∀ r > 0, d > r → (∃ c : EuclideanSpace ℝ (Fin 2), dist c 0 = d ∧ (∫ p in (circint c r), rho h p) = 0))) ↔ putnam_2021_b3_solution :=
 sorry