1959 problem 1

Stream: IMO-grand-challenge

[Kevin Lacker]

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

[Kevin Lacker]

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

[Kevin Lacker]

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

[Mario Carneiro]

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

[Kevin Lacker]

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

[Kevin Lacker]

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]

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

[Kevin Lacker]

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]

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

[Kevin Lacker]

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]

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]

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]

@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]

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

[Bryan Gin-ge Chen]

Rob actually added some links today: https://github.com/leanprover-community/leanprover-community.github.io/pull/134

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

[Johan Commelin]

[I should read what others reply before shouting.]

[Rob Lewis]

The other relevant link is https://leanprover-community.github.io/ci.html

[Rob Lewis]

But I do think we should reconsider the information layout on the web page at some point. There's a lot of stuff hidden behind a few layers of links.