From 1c469e6880798db8a3d38ed032a900824660bd4a Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Wed, 21 Aug 2024 21:07:02 +0000 Subject: [PATCH] fix the problems --- lean4/src/putnam_2007_a3.lean | 1 + lean4/src/putnam_2016_a2.lean | 2 +- 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/lean4/src/putnam_2007_a3.lean b/lean4/src/putnam_2007_a3.lean index 2dd7fc02..0b8a3ec3 100644 --- a/lean4/src/putnam_2007_a3.lean +++ b/lean4/src/putnam_2007_a3.lean @@ -2,6 +2,7 @@ import Mathlib open BigOperators open Set +open scoped Nat abbrev putnam_2007_a3_solution : ℕ → ℚ := sorry -- fun k ↦ (k)! * (k + 1)! / ((3 * k + 1) * (2 * k)!) diff --git a/lean4/src/putnam_2016_a2.lean b/lean4/src/putnam_2016_a2.lean index bf058516..645aa804 100644 --- a/lean4/src/putnam_2016_a2.lean +++ b/lean4/src/putnam_2016_a2.lean @@ -4,7 +4,7 @@ open BigOperators open Polynomial Filter Topology Real Set Nat noncomputable abbrev putnam_2016_a2_solution : ℝ := sorry --- (3 + sqrt 5) / 2 +-- (3 + √ 5) / 2 theorem putnam_2016_a2 (p : ℕ → ℕ → Prop) (hp : p = fun n ↦ fun m ↦ Nat.choose m (n - 1) > Nat.choose (m - 1) n)