feat(archive/imo): formalize IMO 1964 problem 1 #4369
Conversation
knaka3435
added
the
awaiting-review
archive/imo/imo1964_q1.lean
Outdated
| * (a) Find all positive integers `n` for which `2^n-1` is divisble by `7`. | ||
| * (b) Prove that there is no positive integer `n` for which `2^n+1` is divisible by `7`. | ||
| -/ | ||
| example (n : ℕ) (gt_zero : 0 < n) : ((2^n -1) : zmod 7) = 0 ↔ (n : zmod 3) = 0 := |
There was a problem hiding this comment.
I'm not exactly sure what our principles are for formalizing statements like this, but I think we could phrase this a smidge more literally, without causing any serious problems.
Would this be difficult?
| example (n : ℕ) (gt_zero : 0 < n) : ((2^n -1) : zmod 7) = 0 ↔ (n : zmod 3) = 0 := | |
| example (n : ℤ) (gt_zero : 0 < n) : 7 | (2^n -1) ↔ 3 | n := |
There was a problem hiding this comment.
For the other proof it seems to be no problem to change this directly, but for this one, I've ran into (\u(2^n-1 : nat) : zmod 7) = 2^n-1 which is giving me some problems.
There was a problem hiding this comment.
For questions of the form "Find all numbers for which blah", I've been formalizing it as, first write a problem_predicate which is what the problem is giving, then write a solution_predicate for what you claim the solution is, in some sort of simple form, and then the main theorem is that the two are equal. If it's a pain to muck around with converting between modular arithmetic and regularly arithmetic, well basically yeah, that's one of the main difficulties with formalizing things. For any sort of IMO challenge we won't get the problems in the most convenient form, so it's better to describe the problem in the way most similar to the problem statement.
archive/imo/imo1964_q1.lean
Outdated
| norm_num } | ||
| end | ||
|
|
||
| example (n : ℕ) (gt_zero : 0 < n) : ¬((2^n + 1) : zmod 7) = 0 := |
There was a problem hiding this comment.
| example (n : ℕ) (gt_zero : 0 < n) : ¬((2^n + 1) : zmod 7) = 0 := | |
| example (n : ℤ) (gt_zero : 0 < n) : ¬ (7 | 2^n + 1) := |
awainverse
added
awaiting-author
| haveI : fact (nat.prime 7) := by { delta fact, norm_num }, | ||
| have h2 : (2 % 7) ≠ 0 := dec_trivial, | ||
| rw ← nat.mod_add_div n 6, | ||
| have : 6 * (n / 6) % 3 = 0, sorry, |
There was a problem hiding this comment.
Do you need help with these sorrys? Or are you working on them?
There was a problem hiding this comment.
I'm working on them, since the past few days have been rather busy.
This is an alternative approach to #4369, where progress seems to have stalled. I avoid integers completely by working with `nat.modeq`, and deal with the cases of n mod 3 by simply breaking into three cases. Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
The problem states:
(a) Find all positive n such that 2^n-1 is divisible by 7
(b) Prove that for all positive n, 2^n+1 is not divisible by 7
It might be more desirable to have it be in a more literal formalization of the problem statements, however, coercions seem painful to get to zmod.
Also features a nice simp lemma, thanks to @jcommelin (as well as main fact) as discussed here.