From 68e16f8aa83cbb1e56e9a8b527056de8abf64834 Mon Sep 17 00:00:00 2001 From: Oliver Nash Date: Wed, 16 Oct 2024 11:53:12 +0000 Subject: [PATCH 1/4] Fix 2022 A1 The informal solution provided at: https://kskedlaya.org/putnam-archive/2022s.pdf contains some typos. The condition: $$ b < \ln(1 - r_{-})^2 - |a|r_{-} $$ should be: $$ b < \ln(1 + r_{-}^2) - ar_{-} $$ Similarly for the $r_{+}$ case. The argument given in the PDF correctly derives that for $0 < a < 1$ one should have: $$ b < g(r_{-}) $$ where $g(x) = \ln(1 + x ^ 2) - ax$ (and similarly for the $r_{+}$ case. However there are some typos when transcribing this to the headline solution (given higher up). --- informal/putnam.json | 2 +- lean4/src/putnam_2022_a1.lean | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/informal/putnam.json b/informal/putnam.json index 47ff069b..61bc9c43 100644 --- a/informal/putnam.json +++ b/informal/putnam.json @@ -5044,7 +5044,7 @@ { "problem_name": "putnam_2022_a1", "informal_statement": "Determine all ordered pairs of real numbers $(a,b)$ such that the line $y = ax+b$ intersects the curve $y = \\ln(1+x^2)$ in exactly one point.", - "informal_solution": "Show that the solution is the set of ordered pairs $(a,b)$ which satisfy at least one of (1) $a = b = 0$, (2) $|a| \\geq 1$, and (3) $0 < |a| < 1$ and $b < \\log(1 - r_{-})^2 - |a|r_{-}$ or $b > \\log(1 + r_{+})^2 + |a|r_{+}$ where $r_{\\pm} = \\frac{1 \\pm \\sqrt{1 - a^2}}{a}$.", + "informal_solution": "Show that the solution is the set of ordered pairs $(a,b)$ which satisfy at least one of (1) $a = b = 0$, (2) $|a| \\geq 1$, and (3) $0 < |a| < 1$ and $b < \\log(1 + r_{-}^2) - ar_{-}$ or $b > \\log(1 + r_{+}^2) - ar_{+}$ where $r_{\\pm} = \\frac{1 \\pm \\sqrt{1 - a^2}}{a}$.", "tags": [ "algebra" ] diff --git a/lean4/src/putnam_2022_a1.lean b/lean4/src/putnam_2022_a1.lean index cbfc5c97..a8bd7e00 100644 --- a/lean4/src/putnam_2022_a1.lean +++ b/lean4/src/putnam_2022_a1.lean @@ -4,7 +4,7 @@ open BigOperators open Polynomial abbrev putnam_2022_a1_solution : Set (ℝ × ℝ) := sorry --- {(a, b) | (a = 0 ∧ b = 0) ∨ (|a| ≥ 1) ∨ (0 < |a| ∧ |a| < 1 ∧ (b < (Real.log (1 - (1 - Real.sqrt (1 - a^2))/a))^2 - |a| * (1 - Real.sqrt (1 - a^2))/a ∨ b > (Real.log (1 - (1 + Real.sqrt (1 - a^2))/a))^2 - |a| * (1 + Real.sqrt (1 - a^2))/a))} +-- {(a, b) | (a = 0 ∧ b = 0) ∨ 1 ≤ |a| ∨ (0 < |a| ∧ |a| < 1 ∧ letI rm := (1 - √(1 - a ^ 2)) / a; letI rp := (1 + √(1 - a ^ 2)) / a; (b < Real.log (1 + rm ^ 2) - a * rm ∨ b > Real.log (1 + rp ^ 2) - a * rp))} /-- Determine all ordered pairs of real numbers $(a,b)$ such that the line $y = ax+b$ intersects the curve $y = \ln(1+x^2)$ in exactly one point. -/ From bd3fee16841bb8fa99a8eeb3cfb5705f104b5a5c Mon Sep 17 00:00:00 2001 From: Oliver Nash Date: Thu, 24 Oct 2024 13:33:56 +0000 Subject: [PATCH 2/4] Fix 2009 B4 MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This was disprovable because the integral was using the two-dimensional measure from the plane in the integral on the one-dimensional set that is the circle (and thus was always zero). We could fix this by supplying the one-dimensional Hausdorff measure but this is too heavy-weight given that we can just parameterise and use the interval integral. A second error was the inclusion of the typeclasses `[AddCommGroup V] [Module ℝ V]`. The subset already has this algebraic structure and by supplying these there is ambiguity of which structure applies, as well as the fact that these are arbitrary typeclasses with no relation to the ambient structure on `MvPolynomial (Fin 2) ℝ`. --- lean4/src/putnam_2009_b4.lean | 15 ++++++++------- 1 file changed, 8 insertions(+), 7 deletions(-) diff --git a/lean4/src/putnam_2009_b4.lean b/lean4/src/putnam_2009_b4.lean index 4cd7bea2..6e4c16cf 100644 --- a/lean4/src/putnam_2009_b4.lean +++ b/lean4/src/putnam_2009_b4.lean @@ -1,6 +1,6 @@ import Mathlib -open Topology MvPolynomial Filter Set Metric +open intervalIntegral MvPolynomial Real abbrev putnam_2009_b4_solution : ℕ := sorry -- 2020050 @@ -8,9 +8,10 @@ abbrev putnam_2009_b4_solution : ℕ := sorry Say that a polynomial with real coefficients in two variables, $x,y$, is \emph{balanced} if the average value of the polynomial on each circle centered at the origin is $0$. The balanced polynomials of degree at most $2009$ form a vector space $V$ over $\mathbb{R}$. Find the dimension of $V$. -/ theorem putnam_2009_b4 -(balanced : MvPolynomial (Fin 2) ℝ → Prop) -(hbalanced : balanced = 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) := -sorry + (IsBalanced : MvPolynomial (Fin 2) ℝ → Prop) + (IsBalanced_def : ∀ P, IsBalanced P ↔ ∀ r > 0, + (∫ t in (0 : ℝ)..(2 * π), eval ![r * cos t, r * sin t] P) / (2 * π * r) = 0) + (V : Submodule ℝ (MvPolynomial (Fin 2) ℝ)) + (V_def : ∀ P, P ∈ V ↔ IsBalanced P ∧ P.totalDegree ≤ 2009) : + Module.rank ℝ V = putnam_2009_b4_solution := + sorry From a1fb63c0ff5dfb5dda63fb9c9ea56b37a12f8b78 Mon Sep 17 00:00:00 2001 From: Oliver Nash Date: Thu, 24 Oct 2024 14:44:22 +0000 Subject: [PATCH 3/4] Fix 2017 A2 This was disprovable because of division-by-zero silliness. The fix is to restate the problem in the language of rational functions. --- lean4/src/putnam_2017_a2.lean | 13 ++++++++----- 1 file changed, 8 insertions(+), 5 deletions(-) diff --git a/lean4/src/putnam_2017_a2.lean b/lean4/src/putnam_2017_a2.lean index ec3b697b..35a5fa43 100644 --- a/lean4/src/putnam_2017_a2.lean +++ b/lean4/src/putnam_2017_a2.lean @@ -1,11 +1,14 @@ import Mathlib +open Polynomial + /-- Let $Q_0(x)=1$, $Q_1(x)=x$, and $Q_n(x)=\frac{(Q_{n-1}(x))^2-1}{Q_{n-2}(x)}$ for all $n \geq 2$. Show that, whenever $n$ is a positive integer, $Q_n(x)$ is equal to a polynomial with integer coefficients. -/ theorem putnam_2017_a2 -(Q : ℕ → ℝ → ℝ) -(hQbase : ∀ x : ℝ, Q 0 x = 1 ∧ Q 1 x = x) -(hQn : ∀ n ≥ 2, ∀ x : ℝ, Q n x = ((Q (n - 1) x) ^ 2 - 1) / Q (n - 2) x) -: ∀ n > 0, ∃ P : Polynomial ℝ, (∀ i : ℕ, P.coeff i = round (P.coeff i)) ∧ Q n = P.eval := -sorry + (Q : ℕ → RatFunc ℚ) + (hQbase : Q 0 = 1 ∧ Q 1 = (X : ℚ[X])) + (hQn : ∀ n, Q (n + 2) = (Q (n + 1) ^ 2 - 1) / Q n) + (n : ℕ) (hn : 0 < n) : + ∃ P : ℤ[X], Q n = P.map (Int.castRingHom ℚ) := + sorry From f91d6848381f07a035930a6043aeea4d7ffa1940 Mon Sep 17 00:00:00 2001 From: Oliver Nash Date: Thu, 24 Oct 2024 16:02:43 +0000 Subject: [PATCH 4/4] Fix 1963 A3 (again) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This was disprovable because `y` could fail to be differentiable at `1`. E.g., one could define `y` such that: `y x = ∫ t in (1 : ℝ)..x, putnam_1963_a3_solution f n x t` for `x ≥ 1` and `y x = 0` for `x < 1`. This will satisfy the RHS of the iff in the goal but not the left. I see two obvious ways to resolve the issue: 1. Demand that `y` is C^n on `[1, ∞)` 2. Require that `y x = ∫ t in (1 : ℝ)..x, putnam_1963_a3_solution f n x t` holds on a neighbourhood of `[1, ∞)` The informal statement is very vague so I have somewhat arbitrarily opted for the first of these resolutions. This was previously "fixed" in 7a9215271b97b0d3a87f747c3828fea29e0d9ef7 but unfortunately an error remained. --- lean4/src/putnam_1963_a3.lean | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/lean4/src/putnam_1963_a3.lean b/lean4/src/putnam_1963_a3.lean index 07471de0..a16ea888 100644 --- a/lean4/src/putnam_1963_a3.lean +++ b/lean4/src/putnam_1963_a3.lean @@ -13,7 +13,8 @@ theorem putnam_1963_a3 (n : ℕ) (hn : 0 < n) (f y : ℝ → ℝ) - (hf : ContinuousOn f (Ici 1)) : - ContDiffOn ℝ n y (Ici 1) ∧ (∀ i < n, deriv^[i] y 1 = 0) ∧ (Ici 1).EqOn (P n y) f ↔ + (hf : ContinuousOn f (Ici 1)) + (hy : ContDiffOn ℝ n y (Ici 1)) : + (∀ i < n, deriv^[i] y 1 = 0) ∧ (Ici 1).EqOn (P n y) f ↔ ∀ x ≥ 1, y x = ∫ t in (1 : ℝ)..x, putnam_1963_a3_solution f n x t := sorry