## Stream: IMO-grand-challenge

### Topic: 1959 problem 1

#### Kevin Lacker (Sep 30 2020 at 19:00):

I opened second formalized IMO problem pull request. https://github.com/leanprover-community/mathlib/pull/4340

#### Kevin Lacker (Sep 30 2020 at 19:00):

I was wrong about the earlier one - this one has to be the easiest IMO problem of all time

#### Kevin Lacker (Sep 30 2020 at 19:01):

I spent more time searching for the definition of "coprime" in the docs than actually solving the problem

#### Mario Carneiro (Sep 30 2020 at 19:13):

Oh, when I read the problem I thought it was saying that (21n+4)/(14n+3) is a prime number

#### Kevin Lacker (Sep 30 2020 at 19:22):

one thing I have to say is incredible about the lean community is how fast my pull requests get reviews

#### Kevin Lacker (Sep 30 2020 at 19:23):

for most open source projects, I am used to like waiting a week, then finding some random people to bug, then arguing for why anyone should pay any attention at all

#### Mario Carneiro (Sep 30 2020 at 19:23):

ha, I am sure the maintainer team will be glad to hear you think so

#### Kevin Lacker (Sep 30 2020 at 19:23):

lean is more like, ten people jump on immediately to say i could replace 3 lines with 1 line by using some random library function i've never heard of

#### Bryan Gin-ge Chen (Sep 30 2020 at 19:27):

Small & easy-to-review PRs tend to get quicker responses, for better or worse.

#### Kevin Lacker (Sep 30 2020 at 19:28):

yeah, these are pretty basic mathematics, since by definition you dont need college math to understand an IMO problem. plus i am trying to pick off easier ones

#### Rob Lewis (Sep 30 2020 at 19:32):

This is by far the easiest kind of PR to review. 7 lines of content, it will never have any dependencies, somehow we decided at some point that IMO problems are in scope for the library.

#### Alex J. Best (Sep 30 2020 at 21:12):

Theres definitely an advantage to formal verification (+CI tooling) over open source projects in "normal" programming languages too, you don't have to worry about whether peoples work is correct! As long as the types of the statements make sense and agree with what they claim its just a question of style after that :grinning:

#### Scott Morrison (Oct 01 2020 at 02:25):

@Rob Lewis, could you remind me how to find your continuous-integration-for-non-mathlib-projects webpage? I couldn't find it anywhere.

#### Scott Morrison (Oct 01 2020 at 02:26):

If there really aren't links direct from the main community page we should at some!

#### Bryan Gin-ge Chen (Oct 01 2020 at 02:35):

Here's the page, by the way: https://leanprover-community.github.io/lean_projects.html