Fix some minor Lean misformalisations #203
Conversation
There is one change which is required to fix the misformalisation: * Make sure `n / 2` use rational number division There are two changes which are not required but are nice to have: * Use notation for `Nat.ceil` * Use `+ 1` instead of `- 1` to avoid natural number subtraction
The error in the original formalisation was that `P` was not fully characterised (using an iff criterion). In fact we provide a complete restatement since the original form was unnecessarily complicated.
There were two errors in the original statement: * The set `Q` is not fully characterised (e.g., it could be empty) * The solution should intersect with the positive integers A complete restatement seemed best.
The hypothesis `hasum` implies `False`. This issue could be fixed by adding parentheses around the ` ∧ ` but I think a rewrite is better.
The limit should be a right-hand limit. (In fact the singularity at `r = 0` is removable and we could also use `𝓝[≠] 0` but this statement matches the question.)
The hypothesis `hM` implied `False` because it implied that every function on [0, 1] had a maximum. We could fix this by specifying `M` only for continuous functions and making no other changes but it is more faithful to the question to restrict all functionals to C([0, 1], ℝ).
The hypotheses `hSABpart` and `hLS` jointly implied `False` for slightly
subtle reasons. To be precise, because `A ≠ B` is not demanded in
`hSABpart`, `Set.encard {AB | SABpart ∅ AB}.encard` is infinite and thus
cannot equal `LS ∅` since this is finite. We thus fix the statement by
adding `A ≠ B`.
We also include some stylistic changes, specifically:
* We express the goal using `IsGreatest`
* We rename `SABpart` to `IsLinearPartition` since this is the
terminology of the question statement.
* We drop some unnecessary type ascriptions.
The condition `hnmat` did not refer to `nmat` at all and so the proposition `nmat` was free (and thus the statement could be disproved). To fix this, `nmat` has been turned into a predicate which is characterised by `hnmat`. In addition some minor stylistic changes are made, notably the use of `Pairwise`.
There was a problem hiding this comment.
Thank you so much for the PR! We really appreciate the contribution. Good catches with the subtle mistakes, we missed these in our verification. There also appeared to be some issues which probably arose from doing too many global syntactic edits at once. We did the most recent years first so hopefully there are less in the remaining problems. We also were not previously aware of IsGreatest and IsLeast, there are a fair amount of problems which still spell it out directly. We can get to those, but it might be several weeks as the semester is starting up soon so most of the team will be busy, and I'll be traveling shortly.
We'll also make some modifications in the corresponding Isabelle & Coq files to match any edits. Will leave this PR until we have made those changes. I also noted in putnam_2021_b2 that the held out solution is not mentioned in the theorem statement, but don't worry about this we can make this change on our end.
It was accidentally included in 3e4fc86
You're very welcome :)
Yes I was intending to highlight this. It's good to hear you might use these more widely, but there's no rush here. I think fixing misformalisations is much more urgent.
Of course it's your project so you should certainly act as you see fit. However I'm not convinced that there is benefit to keeping a consistency of misformalisations across the three languages. This is just a batch of the first 10 problems I decided to fix and I should be able to fix many more. However if I have to wait for the Isabelle & Coq changes each time, I may not have further PRs. |
Yeah, on second thought I agree with you. I'll merge and open an issue for the other languages. Let me know if you have any other suggestions! |
No description provided.