diff --git a/lean4/src/putnam_1963_a6.lean b/lean4/src/putnam_1963_a6.lean index 7add62d..ef7c41f 100644 --- a/lean4/src/putnam_1963_a6.lean +++ b/lean4/src/putnam_1963_a6.lean @@ -11,14 +11,16 @@ theorem putnam_1963_a6 (E : Set (EuclideanSpace ℝ (Fin 2))) (hE : E = {H : EuclideanSpace ℝ (Fin 2) | dist F1 H + dist F2 H = r}) (M : EuclideanSpace ℝ (Fin 2)) -(hM : M = midpoint ℝ U V) +(hMuv : M = 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) +(hAC : A ≠ C) +(hBD : B ≠ D) (hdistinct : segment ℝ A B ≠ segment ℝ U V ∧ segment ℝ C D ≠ segment ℝ U V ∧ segment ℝ A B ≠ segment ℝ C D) (hM : M ∈ segment ℝ A B ∧ M ∈ segment ℝ C D) (hP : Collinear ℝ {P, A, C} ∧ Collinear ℝ {P, U, V}) -(hQ : Collinear ℝ {P, B, D} ∧ Collinear ℝ {Q, U, V}) +(hQ : Collinear ℝ {Q, B, D} ∧ Collinear ℝ {Q, U, V}) : M = midpoint ℝ P Q := sorry diff --git a/lean4/src/putnam_1964_b4.lean b/lean4/src/putnam_1964_b4.lean index cf8f6d2..e5b370f 100644 --- a/lean4/src/putnam_1964_b4.lean +++ b/lean4/src/putnam_1964_b4.lean @@ -19,6 +19,7 @@ theorem putnam_1964_b4 (hv : ∀ i, C i = Metric.sphere 0 1 ∩ {x : EuclideanSpace ℝ (Fin 3) | ⟪v i, x⟫_ℝ = 0 }) --all the `v_i`'s are non-zero (hv' : ∀ i, v i ≠ 0) + (hCinj : Function.Injective C) -- The circles in `C` are in general position (hT₂ : ∀ᵉ (x ∈ Metric.sphere 0 1) (y ∈ Metric.sphere 0 1), (Finset.univ.filter (fun i => {x, y} ⊆ (C i))).card ≤ 2) diff --git a/lean4/src/putnam_1977_a2.lean b/lean4/src/putnam_1977_a2.lean index c5ea460..9ade887 100644 --- a/lean4/src/putnam_1977_a2.lean +++ b/lean4/src/putnam_1977_a2.lean @@ -6,6 +6,8 @@ abbrev putnam_1977_a2_solution : ℝ → ℝ → ℝ → ℝ → Prop := sorry Find all real solutions $(a, b, c, d)$ to the equations $a + b + c = d$, $\frac{1}{a} + \frac{1}{b} + \frac{1}{c} = \frac{1}{d}$. -/ theorem putnam_1977_a2 : - ∀ a b c d : ℝ, putnam_1977_a2_solution a b c d ↔ - a ≠ 0 → b ≠ 0 → c ≠ 0 → d ≠ 0 → (a + b + c = d ∧ 1 / a + 1 / b + 1 / c = 1 / d) := + ∀ a b c d : ℝ, + a ≠ 0 → b ≠ 0 → c ≠ 0 → d ≠ 0 → + (putnam_1977_a2_solution a b c d ↔ + (a + b + c = d ∧ 1 / a + 1 / b + 1 / c = 1 / d)) := sorry diff --git a/lean4/src/putnam_1977_b6.lean b/lean4/src/putnam_1977_b6.lean index 18d3241..5f57013 100644 --- a/lean4/src/putnam_1977_b6.lean +++ b/lean4/src/putnam_1977_b6.lean @@ -9,6 +9,7 @@ theorem putnam_1977_b6 {G : Type*} [Group G] (H : Subgroup G) +[Finite H] (h : ℕ) (h_def : h = Nat.card H) (a : G) diff --git a/lean4/src/putnam_1980_a4.lean b/lean4/src/putnam_1980_a4.lean index 07cd883..40557fc 100644 --- a/lean4/src/putnam_1980_a4.lean +++ b/lean4/src/putnam_1980_a4.lean @@ -8,7 +8,7 @@ import Mathlib -/ theorem putnam_1980_a4 (abcvals : ℤ → ℤ → ℤ → Prop) - (habcvals : ∀ a b c : ℤ, abcvals a b c ↔ (a = 0 ∧ b = 0 ∧ c = 0) ∧ |a| < 1000000 ∧ |b| < 1000000 ∧ |c| < 1000000) : + (habcvals : ∀ a b c : ℤ, abcvals a b c ↔ ¬(a = 0 ∧ b = 0 ∧ c = 0) ∧ |a| < 1000000 ∧ |b| < 1000000 ∧ |c| < 1000000) : (∃ a b c : ℤ, abcvals a b c ∧ |a + b * Real.sqrt 2 + c * Real.sqrt 3| < 10 ^ (-(11 : ℝ))) ∧ diff --git a/lean4/src/putnam_1989_b6.lean b/lean4/src/putnam_1989_b6.lean index fbb18c6..ed83543 100644 --- a/lean4/src/putnam_1989_b6.lean +++ b/lean4/src/putnam_1989_b6.lean @@ -13,7 +13,7 @@ theorem putnam_1989_b6 (X : Set (Fin n → ℝ)) (X_def : ∀ x, x ∈ X ↔ 0 < x 0 ∧ x (-1) < 1 ∧ StrictMono x) (S : (ℝ → ℝ) → (Fin (n + 2) → ℝ) → ℝ) - (S_def : ∀ f x, S f x = ∑ i : Fin n.succ, (x i.succ - x i.castSucc) * f (i + 1)) : + (S_def : ∀ f x, S f x = ∑ i : Fin n.succ, (x i.succ - x i.castSucc) * f (x i.succ)) : ∃ P : Polynomial ℝ, P.degree = n ∧ (∀ t ∈ Icc 0 1, P.eval t ∈ Icc 0 1) ∧ diff --git a/lean4/src/putnam_1997_a5.lean b/lean4/src/putnam_1997_a5.lean index 5862a94..2fbb609 100644 --- a/lean4/src/putnam_1997_a5.lean +++ b/lean4/src/putnam_1997_a5.lean @@ -9,6 +9,6 @@ Let $N_n$ denote the number of ordered $n$-tuples of positive integers $(a_1,a_2 -/ theorem putnam_1997_a5 (N : (n : ℕ+) → Set (Fin n → ℕ+)) -(hN : N = fun (n : ℕ+) => {t : Fin n → ℕ+ | (∀ i j : Fin n, i < j → t i <= t j) ∧ (∑ i : Fin n, (1 : ℝ)/(t i) = 1) }) +(hN : N = fun (n : ℕ+) => {t : Fin n → ℕ+ | (∑ i : Fin n, (1 : ℝ)/(t i) = 1) }) : Odd (N 10).ncard ↔ putnam_1997_a5_solution := sorry diff --git a/lean4/src/putnam_1999_b3.lean b/lean4/src/putnam_1999_b3.lean index e12b172..cc2d9bd 100644 --- a/lean4/src/putnam_1999_b3.lean +++ b/lean4/src/putnam_1999_b3.lean @@ -11,6 +11,6 @@ theorem putnam_1999_b3 (A : Set (ℝ × ℝ)) (hA : A = {xy | 0 ≤ xy.1 ∧ xy.1 < 1 ∧ 0 ≤ xy.2 ∧ xy.2 < 1}) (S : ℝ → ℝ → ℝ) -(hS : S = fun x y => ∑' m : ℕ, ∑' n : ℕ, if (m > 0 ∧ n > 0 ∧ 1/2 ≤ m/n ∧ m/n ≤ 2) then x^m * y^n else 0) +(hS : S = fun x y => ∑' m : ℕ, ∑' n : ℕ, if (m > 0 ∧ n > 0 ∧ (1 : ℝ)/2 ≤ (m : ℝ)/n ∧ (m : ℝ)/n ≤ 2) then x^m * y^n else 0) : Tendsto (fun xy : (ℝ × ℝ) => (1 - xy.1 * xy.2^2) * (1 - xy.1^2 * xy.2) * (S xy.1 xy.2)) (𝓝[A] ⟨1,1⟩) (𝓝 putnam_1999_b3_solution) := sorry diff --git a/lean4/src/putnam_2003_a5.lean b/lean4/src/putnam_2003_a5.lean index 5392c7b..a67bd33 100644 --- a/lean4/src/putnam_2003_a5.lean +++ b/lean4/src/putnam_2003_a5.lean @@ -12,7 +12,7 @@ theorem putnam_2003_a5 range p ⊆ {-1, 1} ∧ ∑ k, p k = 0 ∧ ∀ j, ∑ k, ite (k ≤ j) (p k) 0 ≥ 0}) (noevenreturn : (m : ℕ) → Set ((Fin (2 * m)) → ℤ)) (hnoevenreturn : noevenreturn = fun m ↦ {p | - ¬∃ i j, i < j ∧ p i = 1 ∧ (∀ k ∈ Ioc i j, p i = -1) ∧ + ¬∃ i j, i < j ∧ p i = 1 ∧ (∀ k ∈ Ioc i j, p k = -1) ∧ Even (j.1 - i.1) ∧ ∑ k, ite (k ≤ j) (p k) 0 = 0}) : ∃ f : ((Fin (2 * n)) → ℤ) → (Fin (2 * (n - 1)) → ℤ), ∀ y ∈ dyckpath (n - 1), ∃! x, x ∈ dyckpath n ∩ noevenreturn n ∧ f x = y := diff --git a/lean4/src/putnam_2003_a6.lean b/lean4/src/putnam_2003_a6.lean index 895b1b1..5ded8f9 100644 --- a/lean4/src/putnam_2003_a6.lean +++ b/lean4/src/putnam_2003_a6.lean @@ -10,5 +10,5 @@ For a set $S$ of nonnegative integers, let $r_S(n)$ denote the number of ordered theorem putnam_2003_a6 (r : Set ℕ → ℕ → ℕ) (hr : ∀ S n, r S n = ∑' s1 : S, ∑' s2 : S, if (s1 ≠ s2 ∧ s1 + s2 = n) then 1 else 0) -: (∃ A B : Set ℕ, A ∪ B = ℕ ∧ A ∩ B = ∅ ∧ (∀ n : ℕ, r A n = r B n)) ↔ putnam_2003_a6_solution := +: (∃ A B : Set ℕ, A ∪ B = (Set.univ : Set ℕ) ∧ A ∩ B = ∅ ∧ (∀ n : ℕ, r A n = r B n)) ↔ putnam_2003_a6_solution := sorry diff --git a/lean4/src/putnam_2003_b5.lean b/lean4/src/putnam_2003_b5.lean index 83a122e..13d0135 100644 --- a/lean4/src/putnam_2003_b5.lean +++ b/lean4/src/putnam_2003_b5.lean @@ -7,7 +7,7 @@ Let $A,B$, and $C$ be equidistant points on the circumference of a circle of uni -/ theorem putnam_2003_b5 (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) +(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 ∧ dist A B ≠ 0) : (∃ 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)) := diff --git a/lean4/src/putnam_2019_a5.lean b/lean4/src/putnam_2019_a5.lean index 46bb51d..5d0ea8c 100644 --- a/lean4/src/putnam_2019_a5.lean +++ b/lean4/src/putnam_2019_a5.lean @@ -17,6 +17,6 @@ theorem putnam_2019_a5 (hq : ∀ k : ℕ, q.coeff k = a k) (ha0 : a 0 = 0 ∧ ∀ k > p - 1, a k = 0) (haother : ∀ k : Set.Icc 1 (p - 1), a k = ((k : ℕ) ^ ((p - 1) / 2)) % p) - (hnpoly : ∀ n x, (npoly n).eval x = (x - 1) ^ n) : + (hnpoly : ∀ n : ℕ, npoly n = (Polynomial.X - 1) ^ n) : IsGreatest {n | npoly n ∣ q} (putnam_2019_a5_solution p) := sorry diff --git a/lean4/src/putnam_2019_a6.lean b/lean4/src/putnam_2019_a6.lean index cad869a..bf2f9bb 100644 --- a/lean4/src/putnam_2019_a6.lean +++ b/lean4/src/putnam_2019_a6.lean @@ -12,5 +12,5 @@ theorem putnam_2019_a6 (hdiff : ContDiffOn ℝ 1 g (Set.Ioo 0 1) ∧ DifferentiableOn ℝ (deriv g) (Set.Ioo 0 1)) (hr : r > 1) (hlim : Tendsto (fun x => g x / x ^ r) (𝓝[>] 0) (𝓝 0)) -: (Tendsto (deriv g) (𝓝[>] 0) (𝓝 0)) ∨ (Tendsto (fun x : ℝ => sSup {x' ^ r * abs (iteratedDeriv 2 g x') | x' ∈ Set.Ioc 0 x}) (𝓝[>] 0) atTop) := +: (Tendsto (deriv g) (𝓝[>] 0) (𝓝 0)) ∨ (Tendsto (fun x : ℝ => sSup {((x' ^ r * abs (iteratedDeriv 2 g x') : ℝ) : WithTop ℝ) | x' ∈ Set.Ioc 0 x}) (𝓝[>] 0) atTop) := sorry diff --git a/lean4/src/putnam_2019_b5.lean b/lean4/src/putnam_2019_b5.lean index 3f22c96..64919b9 100644 --- a/lean4/src/putnam_2019_b5.lean +++ b/lean4/src/putnam_2019_b5.lean @@ -14,5 +14,5 @@ theorem putnam_2019_b5 (F12 : F 1 = 1 ∧ F 2 = 1) (Pdeg: Polynomial.degree P = 1008) (hp: ∀ n : ℕ, (n ≤ 1008) → P.eval (2 * n + 1 : ℝ) = F (2 * n + 1)) -: ∀ j k : ℕ, (P.eval 2019 = F j - F k) ↔ ⟨j, k⟩ = putnam_2019_b5_solution := +: ∀ j k : ℕ, (P.eval 2019 = F j - F k ∧ 1 ≤ j ∧ 1 ≤ k) ↔ ⟨j, k⟩ = putnam_2019_b5_solution := sorry diff --git a/lean4/src/putnam_2022_a4.lean b/lean4/src/putnam_2022_a4.lean index 401a0e6..a0420e2 100644 --- a/lean4/src/putnam_2022_a4.lean +++ b/lean4/src/putnam_2022_a4.lean @@ -3,7 +3,7 @@ import Mathlib open MeasureTheory ProbabilityTheory Classical abbrev putnam_2022_a4_solution : ℝ := sorry --- 2*Real.exp (-1/2) - 3 +-- 2*Real.exp ((1 : ℝ) / 2) - 3 /-- Suppose $X_1, X_2, ...$ real numbers between 0 and 1 that are chosen independently and uniformly at random. Let $S = \sum_{i=1}^k X_i / 2^i $ where $k$ is the least positive integer such that $X_k < X_{k+1}$ or $k = \infty$ if there is no such integer. Find the expected value of $S$ @@ -21,7 +21,7 @@ theorem putnam_2022_a4 Otherwise, this is `sSup { (Set.Iic m : Set ℕ) | (m : ℕ) } = Set.univ` -/ (hk : ∀ ω, k ω = sSup { s : Set ℕ | - ∃ m, s = Set.Iic m ∧ ∀ l ∈ s, X l ω < X (l + 1) ω }) + ∃ m, s = Set.Iic m ∧ ∀ l, l < m → X l ω > X (l + 1) ω }) (S : Ω → ℝ) (hS : ∀ ω, S ω = ∑' (i : k ω), (X i ω) / (2 ^ (i.val + 1))) : ∫ ω, S ω ∂(ℙ : Measure Ω) = putnam_2022_a4_solution := by