## Stream: IMO-grand-challenge

### Topic: 2013 Q5

#### David Renshaw (Jan 17 2021 at 03:29):

It took me two weeks, but I now finally have a proof for Q5 from IMO 2013:

theorem imo2013Q5
(f: ℚ → ℝ)
(f_i:  ∀ x y, 0 < x → 0 < y → f (x * y) ≤ f x * f y)
(f_ii: ∀ x y, 0 < x → 0 < y → f x + f y ≤ f (x + y))
(f_iii: ∃ a, 1 < a ∧ f a = a)
: ∀ x, 0 < x → f x = x


https://github.com/dwrensha/mathematical-puzzles-in-lean/blob/master/src/imo2013_q5.lean

#### David Renshaw (Jan 17 2021 at 03:30):

(The code could definitely use some cleaning up, and I probably am doing some silly noobish things.)

#### Heather Macbeth (Jan 17 2021 at 03:43):

Will you contribute it to the repository? https://github.com/leanprover-community/mathlib/tree/master/archive/imo

#### David Renshaw (Jan 17 2021 at 03:45):

Yes, I'd like to eventually submit a pull request.

#### David Renshaw (Jan 17 2021 at 03:46):

I wanted to put some effort into cleanup first.

#### Alex J. Best (Jan 17 2021 at 03:58):

Wow, cool!
Looks like you've (re)proved quite a few library lemmas though like your nth_power_gt_one would follow from docs#one_lt_pow or nat_abs_pos would be a one-liner from docs#nat_abs_pos_of_ne_zero I believe, hope you didn't spend too long on those! It's true that the library does have many gaps, but for lemmas like those I would usually assume they are already in the library somewhere, finding them can be tough though of course :smile:

#### David Renshaw (Jan 17 2021 at 04:08):

does mathlib have anything that I could have used instead of this lemma?

lemma factor_xn_m_yn
(x : ℝ)
(y:ℝ)
(n: ℕ)
:  x^n - y^n = (x - y) * (∑ (i:ℕ) in finset.range n, (x ^(i) * y ^(n - 1 -i)))


#### Alex J. Best (Jan 17 2021 at 04:22):

There is docs#polynomial.pow_sub_pow_factor but its not quite the same I think?

ah, nice!

#### David Renshaw (Jan 17 2021 at 20:10):

I've submitted https://github.com/leanprover-community/mathlib/pull/5786.

#### Bryan Gin-ge Chen (Jan 17 2021 at 20:17):

Thanks! I've sent you an invite to the mathlib repo. Please open a PR from a branch on the mathlib repo per the instructions here.

#### David Renshaw (Jan 17 2021 at 20:28):

I'm having trouble running the linter locally:

$./scripts/lint-style.sh + touch scripts/style-exceptions.txt + find src archive -name '*.lean' + xargs ./scripts/lint-style.py Traceback (most recent call last): File "/home/dwrensha/src/mathlib/./scripts/lint-style.py", line 212, in <module> lint(Path(fn)) File "/home/dwrensha/src/mathlib/./scripts/lint-style.py", line 206, in lint errs = reserved_notation_check(lines, fn) File "/home/dwrensha/src/mathlib/./scripts/lint-style.py", line 87, in reserved_notation_check if fn.relative_to(ROOT_DIR) == Path('src/tactic/reserved_notation.lean'): File "/usr/lib64/python3.9/pathlib.py", line 928, in relative_to raise ValueError("{!r} is not in the subpath of {!r}" ValueError: 'src/logic/embedding.lean' is not in the subpath of '/home/dwrensha/src/mathlib' OR one path is relative and the other is absolute.  #### Bryan Gin-ge Chen (Jan 17 2021 at 20:35): Hmm, it's failing for me too for an unrelated reason: $ ./scripts/lint-style.sh
+ touch scripts/style-exceptions.txt
+ find src archive -name '*.lean'
+ xargs ./scripts/lint-style.py
++ find . -name '*.lean' -type f -executable
find: -executable: unknown primary or operator
+ executable_files=


I guess the version of find in my version of macOS doesn't support -executable.

@Julian Berman #5721 was supposed to make it easier to run the linter, right? Want to take a look?

#### Alex J. Best (Jan 17 2021 at 20:46):

This is quite weird, on my setup (MINGW64 on windows) using the fixes suggested at
https://apple.stackexchange.com/questions/116367/find-all-executable-files-within-a-folder-in-terminal don't work, maybe using an approach like
is most portable?

#### Julian Berman (Jan 17 2021 at 21:15):

Bryan Gin-ge Chen said:

Hmm, it's failing for me too for an unrelated reason:

$./scripts/lint-style.sh + touch scripts/style-exceptions.txt + find src archive -name '*.lean' + xargs ./scripts/lint-style.py ++ find . -name '*.lean' -type f -executable find: -executable: unknown primary or operator + executable_files=  I guess the version of find in my version of macOS doesn't support -executable. Julian Berman #5721 was supposed to make it easier to run the linter, right? Want to take a look? Oy, yes will have a look in a few hours #### Julian Berman (Jan 18 2021 at 02:26): @David Renshaw an immediate fix is this diff: ⊙ g diff julian@Home ● diff --git a/scripts/lint-style.sh b/scripts/lint-style.sh index d20887efd..5d00a6a4a 100755 --- a/scripts/lint-style.sh +++ b/scripts/lint-style.sh @@ -35,7 +35,7 @@ set -exo pipefail touch scripts/style-exceptions.txt -find src archive -name '*.lean' | xargs ./scripts/lint-style.py +find$PWD/src $PWD/archive -name '*.lean' | xargs ./scripts/lint-style.py # 2. Global checks on the mathlib repository  i.e. to add $PWD/ in front of archive and src in lint-style.sh.

I'll send a PR to mathlib to fix, but given I've broken it once already and CI passed, I think it deserves a few unit tests to make sure I'm not breaking any other combination of absolute/relative, so will take me a day or so to get that sent over.

#### Julian Berman (Jan 18 2021 at 02:34):

@Bryan Gin-ge Chen if you're adventurous, you can use GNU find on macOS. (I do, it works fine, and only once in a blue moon do I need to tell something to use regular BSD find). brew install findutils and then placing it first on your PATH.

#### Julian Berman (Jan 18 2021 at 02:34):

(Though yeah that sounds worth fixing too... will have a look tomorrow when I poke around more. Possibly the whole thing can just be a Python script...)

Last updated: Aug 05 2021 at 04:14 UTC