Fixed Euclidean dist issues w.t.t. Eric Wieser for his suggestion

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')

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)

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

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

lean4/src/putnam_1965_a1.lean

@@ -3,15 +3,14 @@ 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
 (π : ℝ := Real.pi)
 (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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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