From 25bc648386b666409b15ab7f3eb21b57dfe0cb2f Mon Sep 17 00:00:00 2001 From: Ivan Smirnov Date: Tue, 30 Dec 2025 02:56:44 +0000 Subject: [PATCH] Fixed statements for 15 problems. MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Here is the reason for each of the problems: putnam_1963_a6: - Renamed hypothesis: (hM : M = midpoint ℝ U V) → (hMuv : M = midpoint ℝ U V) - Avoids name shadowing with the later hypothesis hM : M ∈ segment ℝ A B ∧ M ∈ segment ℝ C D - Added (hAC : A ≠ C) - Required for line AC to be well-defined (P is the intersection of lines AC and UV) - Added (hBD : B ≠ D) - Required for line BD to be well-defined (Q is the intersection of lines BD and UV) - Fixed typo in hQ: Collinear ℝ {P, B, D} → Collinear ℝ {Q, B, D} - The hypothesis should state that Q (not P) is collinear with B and D putnam_1964_b4: - Added (hCinj : Function.Injective C) - Ensures the n circles are distinct. - The problem statement says "n great circles" which implicitly assumes n different circles, but the original formalization allowed duplicates. putnam_1977_a2 - Repositioned nonzero hypotheses - Changed from ∀ a b c d, solution ↔ (a ≠ 0 → b ≠ 0 → c ≠ 0 → d ≠ 0 → equations) to ∀ a b c d, a ≠ 0 → b ≠ 0 → c ≠ 0 → d ≠ 0 → (solution ↔ equations). - The original was logically incorrect: when variable a equals to 0, the implication becomes vacuously true (False → ...), making the statement claim that (0,b,c,d) satisfies the solution predicate. - The corrected version properly restricts to the nonzero domain where divisions are well-defined. putnam_1977_b6: - Added [Finite H] constraint - The problem states "a subgroup of G with h elements" which implicitly assumes H is finite. - Without this constraint, h = Nat.card H doesn't properly capture the cardinality (since Nat.card of infinite types is 0), and the bound 3*h^2 becomes meaningless. putnam_1980_a4: - Added negation: ¬(a = 0 ∧ b = 0 ∧ c = 0) - The problem requires integers "not all zero", but the original formalization said (a = 0 ∧ b = 0 ∧ c = 0) which is the opposite condition. putnam_1989_b6: - Fixed function evaluation in Riemann sum: f (i + 1) → f (x i.succ) - The problem defines the Riemann sum as $\sum_{i=0}^n (x_{i+1}-x_i)f(x_{i+1})$, where $f$ is evaluated at the partition point value $x_{i+1}$. - The original formalization incorrectly evaluated f (i + 1), passing the index i+1 (a natural number) to a function f : ℝ → ℝ that expects a real number. This is mathematically nonsensical - the function should be evaluated at the actual partition point value x i.succ, not at the index. - Without this fix, the Riemann sum definition doesn't match the problem. putnam_1997_a5: - Removed monotonicity constraint: (∀ i j : Fin n, i < j → t i <= t j) ∧ removed from the definition of N - The problem asks for the number of ordered n-tuples $(a_1, a_2, \ldots, a_n)$ such that $1/a_1 + 1/a_2 + \ldots + 1/a_n = 1$. - The word "ordered" means we count each arrangement separately. The original formalization incorrectly added a constraint requiring the tuple to be sorted (non-decreasing), which would only count each set of values once in sorted order, not all possible orderings. putnam_1999_b3: - Added explicit type casts: 1/2 ≤ m/n → (1 : ℝ)/2 ≤ (m : ℝ)/n and m/n ≤ 2 → (m : ℝ)/n ≤ 2 - The problem requires checking if the ratio $m/n$ falls within $[1/2, 2]$ where $m, n$ are positive integers. - Without explicit type annotations, Lean could interpret m/n as natural number division (which truncates), giving wrong results - e.g., 3/4 would equal 0 instead of 0.75. The explicit casts force division in the real numbers, ensuring the condition matches the mathematical meaning putnam_2003_a5: - Fixed typo in return condition: (∀ k ∈ Ioc i j, p i = -1) → (∀ k ∈ Ioc i j, p k = -1) - A return in a Dyck path is a maximal sequence of contiguous downsteps. The condition should check that each step p k in the interval (i, j] equals -1. - The original incorrectly wrote p i = -1, checking the same fixed value for all indices k - nonsensical. The corrected version properly checks that each step in the interval is a downstep. putnam_2003_a6: - Fixed type error: A ∪ B = ℕ → A ∪ B = (Set.univ : Set ℕ) - The problem asks whether we can partition the nonnegative integers into two sets $A$ and $B$. - The original wrote A ∪ B = ℕ, but in Lean 4's type theory, ℕ is the type of natural numbers, not a set. The union A ∪ B has type Set ℕ, so we need to compare it with Set.univ : Set ℕ (the universal set of all natural numbers) for the statement to be well-typed. putnam_2003_b5: - Added non-degeneracy constraint: ∧ dist A B ≠ 0 - The problem states "$A, B$, and $C$ be equidistant points on the circumference" which implicitly means three distinct points forming an equilateral triangle. - Without this constraint, the original conditions dist A B = dist A C ∧ dist A B = dist B C are satisfied when A = B = C (all three points coincide at the same location on the circle). - In this degenerate case, for any interior point P, the constructed triangle would have all three sides equal to dist P A. But dist P A depends on both the distance ‖P‖ from the origin and P's angular direction. For example, with A = (1, 0), the point P = (0.5, 0) has ‖P‖ = 0.5 and dist P A = 0.5, while P = (0, 0.5) also has ‖P‖ = 0.5 but dist P A ≈ 1.118. These give different triangle areas despite having the same dist 0 P, so no function f(dist 0 P) exists that works for all P. This makes the original statement false and unprovable putnam_2019_a6: - Added explicit type cast to WithTop ℝ in limsup: {x' ^ r * abs (...) | ...} → {(x' ^ r * abs (...) : WithTop ℝ) | ...} - The problem asks to prove that $\limsup_{x \to 0^+} x^r |g''(x)| = \infty$. - In the original formalization, sSup operates on a set of real numbers, but in ℝ, an unbounded set has no supremum. To express "limsup = ∞", we need sSup to be computed in WithTop ℝ (reals with an additional ⊤ element for infinity), where an unbounded set has supremum ⊤. - The modified version casts set elements to WithTop ℝ so that sSup produces ⊤ for unbounded sets, making Tendsto ... atTop well-formed to express divergence to infinity. putnam_2019_a5: - Changed polynomial specification: (hnpoly : ∀ n x, (npoly n).eval x = (x - 1) ^ n) → (hnpoly : ∀ n : ℕ, npoly n = (Polynomial.X - 1) ^ n) - The problem asks about divisibility of polynomials in $\mathbb{F}_p[x]$ (the finite field $\mathbb{F}_p = \text{ZMod } p$). - The original formulation only specified the evaluation function: "for all n and x, evaluating npoly n at x gives (x-1)^n". In finite fields, this is ambiguous because two different polynomials can have identical evaluation functions. By Fermat's Little Theorem, $X^p$ and $X$ evaluate to the same value at every point in $\mathbb{F}_p$ (since $a^p = a$ for all $a \in \mathbb{F}_p$), yet they are distinct polynomials with different coefficients. - The original condition allowed npoly n to be $(X-1)^n + (X^p - X) \cdot f(X)$ for any polynomial $f$, since adding terms that vanish on all field elements doesn't change evaluations. However, polynomial divisibility depends on actual coefficients, not evaluation behavior. The modified version directly defines npoly n as the polynomial $(X-1)^n$, unambiguously specifying the intended polynomial and making the divisibility condition well-defined. putnam_2019_b5: - Added positivity constraints: (P.eval 2019 = F j - F k) → (P.eval 2019 = F j - F k ∧ 1 ≤ j ∧ 1 ≤ k) - The problem defines the Fibonacci sequence starting at index 1: "$F_1 = F_2 = 1$ and $F_m = F_{m-1} + F_{m-2}$ for all $m \geq 3$". - The formalization uses F : ℕ → ℤ, which includes F 0. However, the hypotheses only constrain F 1 = 1, F 2 = 1, and the recurrence for indices ≥ 1. The value F 0 is completely unconstrained and could be any integer. putnam_2022_a4: - The original used X l ω < X (l + 1) ω, characterizing an increasing sequence - the opposite of what's intended. Before reaching k, the sequence should be decreasing: $X_0 \geq X_1 \geq ... \geq X_{k-1} \geq X_k$, then $X_k < X_{k+1}$ breaks this pattern. The modified version correctly uses X l ω > X (l + 1) ω to capture the decreasing portion. - Fixed solution sign and type: 2*Real.exp (-1/2) - 3 → 2*Real.exp ((1 : ℝ) / 2) - 3 - The commented solution had a negative exponent, but the correct answer requires positive exp(1/2). Added explicit type cast (1 : ℝ) to ensure real division instead of natural number division, avoiding truncation (1/2 → 0.5, not 0). --- lean4/src/putnam_1963_a6.lean | 6 ++++-- lean4/src/putnam_1964_b4.lean | 1 + lean4/src/putnam_1977_a2.lean | 6 ++++-- lean4/src/putnam_1977_b6.lean | 1 + lean4/src/putnam_1980_a4.lean | 2 +- lean4/src/putnam_1989_b6.lean | 2 +- lean4/src/putnam_1997_a5.lean | 2 +- lean4/src/putnam_1999_b3.lean | 2 +- lean4/src/putnam_2003_a5.lean | 2 +- lean4/src/putnam_2003_a6.lean | 2 +- lean4/src/putnam_2003_b5.lean | 2 +- lean4/src/putnam_2019_a5.lean | 2 +- lean4/src/putnam_2019_a6.lean | 2 +- lean4/src/putnam_2019_b5.lean | 2 +- lean4/src/putnam_2022_a4.lean | 4 ++-- 15 files changed, 22 insertions(+), 16 deletions(-) diff --git a/lean4/src/putnam_1963_a6.lean b/lean4/src/putnam_1963_a6.lean index 7add62d5..ef7c41ff 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 cf8f6d2f..e5b370f6 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 c5ea4600..9ade887b 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 18d3241e..5f570132 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 07cd8836..40557fca 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 fbb18c67..ed83543b 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 5862a948..2fbb609d 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 e12b1728..cc2d9bd5 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 5392c7be..a67bd33c 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 895b1b1a..5ded8f90 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 83a122e4..13d01355 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 46bb51d3..5d0ea8c1 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 cad869ad..bf2f9bb7 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 3f22c963..64919b9a 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 401a0e61..a0420e2f 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