Fix Lean versions of 2023 A2 and 2023 B1 #254
Conversation
| @@ -22,6 +22,6 @@ theorem putnam_2023_b1 | |||
| → coins1 i' j' = coins2 i' j')) | |||
| (IsLegalSeq : List (ℕ → ℕ → Bool) → Prop) | |||
| (IsLegalSeq_def : ∀ seq, IsLegalSeq seq ↔ seq.length ≥ 1 ∧ seq[0]! = initcoins ∧ (∀ i < seq.length - 1, IsLegalMove seq[i]! seq[i + 1]!)) | |||
| (mnpos : m ≥ 1 ∧ n ≥ 1) | |||
| (mnpos : 1 < m ∧ 1 < n) | |||
There was a problem hiding this comment.
Could you add a comment explaining why this diverges from the prose?
There was a problem hiding this comment.
The issue is m - 2 and n - 2 appearing in hinitcoins.
It should be possible to support m = n = 1 but time was short so I opted for this conservative approach (since the problem is trivially just 1 for m = 1 or n = 1).
If I get time later (or if George requests) I can try to rewrite the formalisation to be valid for m = 1 or n = 1.
There was a problem hiding this comment.
I think the formalization has an off-by-one choice, maybe because the author thought it was easier to use \N. It is probably best to at least have the same content of the problem, even if the difference is a trivial case. What about a short modification to hinitcoins that puts a guard for m \or n = 1?
There was a problem hiding this comment.
@ocfnash Any thoughts on the above? I don't think it would be necessary to do a larger revision.
| @@ -15,5 +15,5 @@ theorem putnam_2023_a2 | |||
| (S : Set ℝ) | |||
| (hS : S = {x : ℝ | ∃ k : ℤ, x = k ∧ 1 ≤ |k| ∧ |k| ≤ n}) | |||
| (hpinv : ∀ k ∈ S, p.eval (1/k) = k^2) | |||
| : {x : ℝ | p.eval (1/x) = x^2} \ S = putnam_2023_a2_solution n := | |||
| : {x : ℝ | x ≠ 0 ∧ p.eval (1/x) = x^2} \ S = putnam_2023_a2_solution n := | |||
There was a problem hiding this comment.
Surprising to see that a mistake like this one was still in here - good catch!
No description provided.