Zulip Chat Archive

Stream: IMO-grand-challenge

Topic: 1959 problem 1


view this post on Zulip Kevin Lacker (Sep 30 2020 at 19:00):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Sep 30 2020 at 19:23):

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

view this post on Zulip 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

view this post on Zulip Bryan Gin-ge Chen (Sep 30 2020 at 19:27):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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:

view this post on Zulip 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.

view this post on Zulip Scott Morrison (Oct 01 2020 at 02:26):

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

view this post on Zulip Bryan Gin-ge Chen (Oct 01 2020 at 02:35):

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

view this post on Zulip Johan Commelin (Oct 01 2020 at 04:40):

[I should read what others reply before shouting.]

view this post on Zulip Rob Lewis (Oct 01 2020 at 08:32):

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

view this post on Zulip Rob Lewis (Oct 01 2020 at 08:33):

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.


Last updated: Aug 05 2021 at 05:09 UTC