archive(imo1988_q6): a formalization of Q6 on IMO1988 #1455
Conversation
|
You have a bunch of nonterminal |
|
Mostly, |
|
@jcommelin |
|
@jcommelin, shall we make |
|
@semorrison I don't care too much. This can wait for a |
archive/imo1988_q6.lean
Outdated
| We need a long list of assumptions for this lemma. | ||
| The upside is that it takes care of several annoying edge cases. | ||
| First of all, the user should provide x and y | ||
| that satisfy the predicate H(x,y). |
There was a problem hiding this comment.
I had a hard time following this, and I already know roughly how to solve the IMO problem. I think it would help to give as an example the particular H(x,y) which is used for the IMO problem. Also, you never mention claim, which is pretty important (at least if you are trying to understand the lemma just from the docstring, and not from looking at its type).
There was a problem hiding this comment.
I have thoroughly rewritten the docstring. I hope it is better now.
archive/imo1988_q6.lean
Outdated
| let p : ℕ × ℕ := ⟨x,y⟩, | ||
| have hp : p ∈ upper_branch := ⟨h₀, hxy⟩, | ||
| -- We also consider the exceptional set of solutions (a,b) that satisfy | ||
| -- a = 0 or a = b or B a = b or B a = b + a. |
There was a problem hiding this comment.
This comment doesn't seem to match the definition--it's missing the "base case". It would be better to say why we doing this, that is, move the "strategy" comment a bit earlier and probably also expand it to contain an outline of the entire rest of the proof.
It seems that the strategy is really: Do descent starting from the given (x, y). The exceptional locus is where we can't keep descending, but our assumptions were chosen to handle those cases.
There was a problem hiding this comment.
I've tried to improve these comments a bit.
semorrison
added
the
awaiting-author
jcommelin
added
awaiting-review
|
This looks mergeable to me. @rwbarton @jcommelin is this waiting on anything? |
|
I think I've processed all the comments. So now it's up to the other mathlib overlords (-; |
robertylewis
added
ready-to-merge
…munity#1455) * archive(imo1988_q6): a formalization of Q6 on IMO1988 * WIP * Clean up, document, and use omega * Remove some non-terminal simps * Non-terminal simp followed by ring is fine * Include copyright statement * Add comment justifying example * Process review comments * Oops, forgot a line * Improve comments in the proof
Another attempt at formalizing Q6 of IMO1988