diff --git a/lean4/src/putnam_1998_a6.lean b/lean4/src/putnam_1998_a6.lean
index 9a75f868..6765dd50 100644
--- a/lean4/src/putnam_1998_a6.lean
+++ b/lean4/src/putnam_1998_a6.lean
@@ -2,6 +2,7 @@ import Mathlib
 open BigOperators
 
 open Set Function Metric
+open scoped InnerProductSpace
 
 /--
 Let $A, B, C$ denote distinct points with integer coordinates in $\mathbb R^2$. Prove that if
@@ -14,6 +15,6 @@ theorem putnam_1998_a6
 (htriangle : A ≠ B ∧ A ≠ C ∧ B ≠ C)
 (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)
-(threesquare_def : threesquare = fun P Q R ↦ dist Q P = dist Q R ∧ Matrix.dotProduct (P - Q) (R - Q) = 0)
+(threesquare_def : threesquare = fun P Q R ↦ dist Q P = dist Q R ∧ ⟪P - Q, R - Q⟫_ℝ = 0)
 : (threesquare A B C ∨ threesquare B C A ∨ threesquare C A B) :=
 sorry
diff --git a/lean4/src/putnam_2002_a2.lean b/lean4/src/putnam_2002_a2.lean
index 8a0a317a..441af7f7 100644
--- a/lean4/src/putnam_2002_a2.lean
+++ b/lean4/src/putnam_2002_a2.lean
@@ -2,6 +2,7 @@ import Mathlib
 open BigOperators
 
 open Nat Metric
+open scoped InnerProductSpace
 
 /--
 Given any five points on a sphere, show that some four of them must lie on a closed hemisphere.
@@ -9,7 +10,7 @@ Given any five points on a sphere, show that some four of them must lie on a clo
 theorem putnam_2002_a2
 (unit_sphere : Set (EuclideanSpace ℝ (Fin 3)))
 (hsphere : unit_sphere = sphere 0 1)
-(hemi : (EuclideanSpace ℝ (Fin 3)) → Set (EuclideanSpace ℝ (Fin 3)))
-(hhemi : hemi = fun V ↦ {P : EuclideanSpace ℝ (Fin 3) | Matrix.dotProduct P V ≥ 0})
-: (∀ (S : Set (EuclideanSpace ℝ (Fin 3))), S ⊆ unit_sphere ∧ S.encard = 5 → ∃ V : (EuclideanSpace ℝ (Fin 3)), V ≠ 0 ∧ (S ∩ hemi V).encard ≥ 4) :=
+(hemi : EuclideanSpace ℝ (Fin 3) → Set (EuclideanSpace ℝ (Fin 3)))
+(hhemi : hemi = fun V ↦ {P : EuclideanSpace ℝ (Fin 3) | ⟪P, V⟫_ℝ ≥ 0})
+: (∀ (S : Set (EuclideanSpace ℝ (Fin 3))), S ⊆ unit_sphere ∧ S.encard = 5 → ∃ V : EuclideanSpace ℝ (Fin 3), V ≠ 0 ∧ (S ∩ hemi V).encard ≥ 4) :=
 sorry