Zulip Chat Archive

Stream: IMO-grand-challenge

Topic: formalizing IMO problems


view this post on Zulip Kevin Lacker (Sep 24 2020 at 21:08):

I looked through the IMO problems looking for ones that would be easy to formalize. At first I thought inequalities might be a good place to focus on, but there really aren't as many as I expected. Number theory seems a bit easier. Maybe I'll try formalizing one up tomorrow. Also, for what's it's worth, I suspect that 1979 problem 1 will be the easiest IMO problem for a Lean-based prover to automatically solve:

view this post on Zulip Kevin Lacker (Sep 24 2020 at 21:09):

1979 problem 1: if p and q are natural numbers such that p/q = 1 - (1/2) + (1/3) - (1/4) + ... + (1/1319), prove that p is divisible by 1979.

view this post on Zulip Kevin Lacker (Sep 24 2020 at 21:10):

i believe you could also fairly easily autogenerate problems of this form, if it were useful to construct such a dataset

view this post on Zulip David Shin (Sep 25 2020 at 04:21):

Is the automated solution you have in mind a brute force arithmetic computation?

view this post on Zulip Kevin Buzzard (Sep 25 2020 at 08:29):

The art of this question is of course to prove the result without doing the computation! pari-gp does the sum instantly (unformalised, of course). This is one of those questions where you can read the solution and say "yeah, I guess that's pretty simple", but actually finding it is tough because 1319 is a bit random.

view this post on Zulip Kevin Lacker (Sep 25 2020 at 15:22):

fortunately, the computer is not required to do it the "artful" way ;-) there's just a teeny bit of extra work on top of the brute force to come to the "p is divisible by 1979" conclusion. still, we don't actually have a solver that will solve this whole problem today, right? so it seems like a relatively simple one that should get cracked early

view this post on Zulip Miroslav Olšák (Sep 25 2020 at 15:34):

Well, this problem in particular is "only" human infeasible to calculate, but it is quite easy to make it also computer-infeasible, just replace the 1979 by a significantly higher prime number, and 1319 by the appropriate (p+1)*2/3-1.

view this post on Zulip Miroslav Olšák (Sep 25 2020 at 15:35):

By the way, the problem reminds me of a discussion we had some time ago -- since p,q are natural numbers, p/q is a natural number as well, right? :-)

view this post on Zulip Kevin Buzzard (Sep 25 2020 at 15:41):

no because there is no notation for natural number division

view this post on Zulip Kevin Buzzard (Sep 25 2020 at 15:42):

That division should really have some modification attached to it indicating that it does 100% represent what a mahtematician means when they use that symbol.

view this post on Zulip Kevin Lacker (Sep 25 2020 at 15:47):

I believe technically it's computer-infeasible right now - a computer can calculate the sum, but AFAIK there is nothing that would go from the entire problem statement, to concluding that the sum needs to be calculated, to deducing that p must be divisible by 1979

view this post on Zulip Kevin Lacker (Sep 25 2020 at 15:49):

maybe some existing proof search mechanism would work, i'm not familiar with everything out there

view this post on Zulip Qian Hong (wechat: fracting) (Oct 01 2020 at 14:32):

Has IMO 2019 been formalized in Lean?

https://www.isa-afp.org/browser_info/current/AFP/IMO2019/index.html

view this post on Zulip Kevin Buzzard (Oct 01 2020 at 14:35):

Not the geometry questions, but some of the rest.

view this post on Zulip Qian Hong (wechat: fracting) (Oct 01 2020 at 14:38):

Someone might want to move them into https://github.com/leanprover-community/mathlib/tree/master/archive/imo ?

view this post on Zulip Kevin Buzzard (Oct 01 2020 at 14:42):

https://gist.github.com/kbuzzard/b337639d471a135108511f4fab850e8b

view this post on Zulip Kevin Lacker (Oct 01 2020 at 15:26):

@Kevin Buzzard would you mind sticking that one and any other IMO problems you have formalized in the archive/imo directory? i have been just picking IMO problems so it would be nice to see which ones you've already done so I don't try redoing it

view this post on Zulip Daniel Selsam (Oct 01 2020 at 16:01):

FYI here are some formalizations in Isabelle: https://github.com/filipmaric/IMO/tree/master/IMO_files/solutions

view this post on Zulip Daniel Selsam (Oct 01 2020 at 16:04):

Floris proved 2019-P4: https://gist.github.com/fpvandoorn/e0bd9d116a59a5f01d1d661f3677b72f

view this post on Zulip Daniel Selsam (Oct 01 2020 at 16:09):

Kevin Buzzard said:

https://gist.github.com/kbuzzard/b337639d471a135108511f4fab850e8b

I recall somebody posted a very short proof of this one in Isabelle/HOL last year, but I cannot seem to find it. Does anybody have the link handy? It would be good to know what automation was useful for it.

view this post on Zulip Kevin Lacker (Oct 01 2020 at 16:12):

they got 10 of them eh. we're behind!

view this post on Zulip Daniel Selsam (Oct 01 2020 at 16:13):

Theirs uses blast, smt, auto, and simp.

view this post on Zulip Rob Lewis (Oct 01 2020 at 16:18):

There are three IMO problems in the mathlib archive, fewer than I thought. I think it might be nice for someone to create and maintain an IMO problem repository, separate from mathlib. We have CI scripts and ways to publicize external projects now. The benefits of an external project are that it can have its own style and doc standards and avoid the overhead of the mathlib PR/review process.

view this post on Zulip Rob Lewis (Oct 01 2020 at 16:20):

If someone is interested in maintaining this kind of repo, we can talk about ways to simplify getting extra lemmas and stuff from there into mathlib.

view this post on Zulip Daniel Selsam (Oct 01 2020 at 17:02):

@Rob Lewis I think this makes sense. I will create a repo for it today.

view this post on Zulip Daniel Selsam (Oct 01 2020 at 18:37):

@Rob Lewis created repo here: https://github.com/IMO-grand-challenge/olympiad-problems what are best practices to port? Baseline would be for me to push mathlib's imo files to the new repo, and issue a PR removing them from mathlib

view this post on Zulip Joseph Myers (Oct 01 2020 at 18:41):

Should this be for any competition problems (many thousands of potential problems, including IMO shortlists, national olympiads, etc.), or just for the 368 IMO problems? Are undergraduate competitions such as Putnam and IMC in scope as well?

view this post on Zulip Rob Lewis (Oct 01 2020 at 18:42):

Daniel Selsam said:

Rob Lewis created repo here: https://github.com/IMO-grand-challenge/olympiad-problems what are best practices to port? Baseline would be for me to push mathlib's imo files to the new repo, and issue a PR removing them from mathlib

Cool! That sounds reasonable.

view this post on Zulip Daniel Selsam (Oct 01 2020 at 18:42):

Joseph Myers said:

Should this be for any competition problems (many thousands of potential problems, including IMO shortlists, national olympiads, etc.), or just for the 368 IMO problems? Are undergraduate competitions such as Putnam and IMC in scope as well?

Any Olympiad problems, the more the merrier. We can add directories e.g. src/putnam and src/imc.

view this post on Zulip Rob Lewis (Oct 01 2020 at 18:43):

@Johan Commelin was worried that small lemmas and additions might not make it into mathlib if these problems move to a new repo, which is a reasonable concern.

view this post on Zulip Joseph Myers (Oct 01 2020 at 18:43):

Rob Lewis said:

If someone is interested in maintaining this kind of repo, we can talk about ways to simplify getting extra lemmas and stuff from there into mathlib.

I suggest "put lemmas and definitions in mathlib first if mathlib-relevant, don't accept anything appropriate for mathlib in this repository" as a good starting point, avoiding adding anything to this repository that could be in mathlib instead unless there is a very good reason (e.g. a simple ad hoc definition suffices for the problem but mathlib should have something much more complicated and more general).

view this post on Zulip Rob Lewis (Oct 01 2020 at 18:43):

Do you think it would make sense to have a for_mathlib directory in your project that gets regularly emptied into mathlib?

view this post on Zulip Daniel Selsam (Oct 01 2020 at 18:43):

Rob Lewis said:

Do you think it would make sense to have a for_mathlib directory in your project that gets regularly emptied into mathlib?

Such a directory exists. I got the idea from the perfectoid repo.

view this post on Zulip Rob Lewis (Oct 01 2020 at 18:44):

Or @Joseph Myers suggestion is also reasonable, but puts a bigger burden on IMO contributors.

view this post on Zulip Rob Lewis (Oct 01 2020 at 18:44):

Aha, you're ahead of me :)

view this post on Zulip Joseph Myers (Oct 01 2020 at 18:44):

When covering all competitions, you need to think about naming conventions. (Does BMO stand for Balkan or British olympiad?)

view this post on Zulip Patrick Massot (Oct 01 2020 at 18:45):

Daniel, as you can see from the perfectoid repo, it isn't such a great idea if you are not determined enough to actually PR stuff from this folder.

view this post on Zulip Rob Lewis (Oct 01 2020 at 18:46):

Maybe it's good to enforce that only little scattered things go in there. Little lemmas are easy to flush and PR into mathlib.

view this post on Zulip Rob Lewis (Oct 01 2020 at 18:46):

And any development beyond a few scattered lemmas should go to mathlib before the IMO problem is merged in that repo.

view this post on Zulip Rob Lewis (Oct 01 2020 at 18:48):

@Daniel Selsam there are a few GitHub Actions scripts here that would be good to put in the repo.

view this post on Zulip Daniel Selsam (Oct 01 2020 at 18:48):

Note that we will eventually have some background material that may not make sense to put into Mathlib, e.g. MDP/Game types for combinatorics problems.

view this post on Zulip Daniel Selsam (Oct 01 2020 at 18:56):

Joseph Myers said:

When covering all competitions, you need to think about naming conventions. (Does BMO stand for Balkan or British olympiad?)

Good point. First thought: spell out e.g. british-olympiad whenever there may otherwise be ambiguity

view this post on Zulip Joseph Myers (Oct 01 2020 at 19:01):

Someone will need to update the mathlib version used in this repository frequently (and fix up proofs that break).

view this post on Zulip Rob Lewis (Oct 01 2020 at 19:02):

Joseph Myers said:

Someone will need to update the mathlib version used in this repository frequently (and fix up proofs that break).

The CI scripts do this. It'll try to upgrade every night and open an issue if the upgrade fails.

view this post on Zulip Joseph Myers (Oct 01 2020 at 19:02):

I expect most mathlib conventions, at least those that are really about good Lean practice, should apply to this repository as well. E.g. proofs should avoid non-terminal simp.

view this post on Zulip Joseph Myers (Oct 01 2020 at 19:04):

How should multiple solutions to the same problem (which might or might not share lemmas) be handled? Formalising multiple solutions plausibly makes sense both for machines to learn from, and to help show humans which approaches are easier or harder in Lean and which might benefit from more automation.

view this post on Zulip Daniel Selsam (Oct 01 2020 at 19:05):

Perhaps we should always write the statements as definitions. Then it is easy to provide multiple (or zero) proofs.

view this post on Zulip Oliver Nash (Oct 01 2020 at 19:06):

Is it definitely a win to create a separate repo for the IMO problems? I agree we have to draw the line somewhere and obviously they are not research problems but I felt that storing this stuff in archive was just the right balance. Aren't we creating work for several people by splitting this stuff out?

view this post on Zulip Joseph Myers (Oct 01 2020 at 19:07):

Will this repository follow the approach used in mathlib where people PR from non-master branches of the same repository (more visibility of in-progress work, possible CI benefits, etc.), or that of people PRing from their own forks?

view this post on Zulip Joseph Myers (Oct 01 2020 at 19:11):

Should this repository try to establish conventions from the start on how particular concepts / phrases in problem statements are translated into Lean, or should it accept anything that could be considered a reasonable formal version of the statement, and worry later about consistent conventions (where such consistent conventions might well require extra definitions to be added to mathlib)?

view this post on Zulip Rob Lewis (Oct 01 2020 at 19:12):

Oliver Nash said:

Is it definitely a win to create a separate repo for the IMO problems? I agree we have to draw the line somewhere and obviously they are not research problems but I felt that storing this stuff in archive was just the right balance. Aren't we creating work for several people by splitting this stuff out?

To be clear, I wasn't trying to speak for the mathlib maintainers when I suggested this, just my own opinion. But I think IMO problems are a perfect thing to put in their own repo. This kind of thing deserves its own visibility, its own review process, its own style and documentation guidelines. To me it seems better to let it grow on its own then force it through the mathlib bottleneck.

view this post on Zulip Oliver Nash (Oct 01 2020 at 19:16):

I don't have strong feelings and I agree with all of these comments. I was just observing that there doesn't seem to be a problem at the moment and the thread indicates a moderate amount of work may result.

view this post on Zulip Daniel Selsam (Oct 01 2020 at 19:19):

Here are some possible advantages of separate repo:

  1. more convenient when we need concepts that don't belong in mathlib, e.g. MDP/Game
  2. we can store problem statements (without proofs), which might not be desired in mathlib
  3. it might make sense for us to allow sorry for steps that specific not-yet-implemented automation will definitely solve. This documentation is actually more useful for IMO-GC than a verbose proof of something "trivial"
  4. we might want to port to Lean4 before mathlib does, e.g. by auto-porting kernel terms from mathlib

view this post on Zulip Oliver Nash (Oct 01 2020 at 19:22):

OK go for it!

view this post on Zulip Joseph Myers (Oct 01 2020 at 19:22):

Daniel Selsam said:

Note that we will eventually have some background material that may not make sense to put into Mathlib, e.g. MDP/Game types for combinatorics problems.

I'd expect mathlib to have whatever definitions are needed to talk about any type of game. Indeed, it already has some (in set_theory/game rather than something like combinatorics/game or game_theory/combinatorial), including definitions of particular games.

view this post on Zulip Oliver Nash (Oct 01 2020 at 19:23):

Btw I just watched your talk from AITP yesterday and it inspired me to attempt to formalise an IMO problem this evening, which is why I'm looking at this thread. Hopefully I'll have a PR for that new repo in a few days!

view this post on Zulip Kevin Lacker (Oct 01 2020 at 19:23):

@Oliver Nash which problem?

view this post on Zulip Oliver Nash (Oct 01 2020 at 19:23):

1998 Q2

view this post on Zulip Kevin Lacker (Oct 01 2020 at 19:24):

cool. i have 1960 q1 in progress, just hoping to not duplicate work

view this post on Zulip Kevin Lacker (Oct 01 2020 at 19:24):

for the record, I am indifferent to what repo IMO problems go into, as long as someone else is responsible for stuff like making sure the continuous integration works

view this post on Zulip Daniel Selsam (Oct 01 2020 at 19:25):

I set up travis for the new repo, but this was my first time so there might be some issues to fix later

view this post on Zulip Kevin Lacker (Oct 01 2020 at 19:25):

i'm sure that will be a fulfilling experience for you :grinning:

view this post on Zulip Joseph Myers (Oct 01 2020 at 19:25):

If we do decide to use a separate repository (that covers all olympiads) I can add my British MO solutions there (but the geometry one still requires me to get more pieces into mathlib first). As even if IMO problems are suitable for the mathlib archive, maybe the scope of the mathlib archive shouldn't be extended to cover the much greater number of problems from olympiads all over the world.

view this post on Zulip Kevin Lacker (Oct 01 2020 at 19:26):

I think we should have problems not just from olympiads, but from like, ARML, california math league, any sort of thing that someone can be bothered to enter in

view this post on Zulip Kevin Lacker (Oct 01 2020 at 19:27):

modern AI techniques really love having tons of data, the real bottleneck is just what people will enter. and if the IMO problems end up too hard for automation, maybe a simpler level of problem will be good for something like "curriculum learning"

view this post on Zulip Rob Lewis (Oct 01 2020 at 19:27):

Daniel Selsam said:

I set up travis for the new repo, but this was my first time so there might be some issues to fix later

Travis to do what? The GitHub actions you installed should build every push to every branch.

view this post on Zulip Daniel Selsam (Oct 01 2020 at 19:28):

Rob Lewis said:

Daniel Selsam said:

I set up travis for the new repo, but this was my first time so there might be some issues to fix later

Travis to do what? The GitHub actions you installed should build every push to every branch.

I copied the travis script from the perfectoid project (updating the ubuntu dist to fix build errors), and added the build-status to the README

view this post on Zulip Rob Lewis (Oct 01 2020 at 19:28):

As well as update the lean-x.y.z feature branches and try to upgrade the Lean/mathlib version once a day.

view this post on Zulip Rob Lewis (Oct 01 2020 at 19:29):

The perfectoid CI is way out of date

view this post on Zulip Daniel Selsam (Oct 01 2020 at 19:31):

@Rob Lewis the new repo does have the beautiful 'build-passing' icon thanks to the perfectoid script ... could you please clarify what you suggest?

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

Oh, I just mean that the Travis script is redundant. The files here do everything it does and more. You'll get a green check at the top of the page (like by leanprover-community/mathlib) certifying that the build passed.

view this post on Zulip Rob Lewis (Oct 01 2020 at 19:34):

The perfectoid project is basically archived, it doesn't build past Lean 3.4.2, so it can't take advantage of the other features of the Actions scripts.

view this post on Zulip Rob Lewis (Oct 01 2020 at 19:34):

So there's no reason to replace the old Travis script there.

view this post on Zulip Daniel Selsam (Oct 01 2020 at 19:34):

@Rob Lewis fantastic, I will delete travis script and update the README banner

view this post on Zulip Rob Lewis (Oct 01 2020 at 19:35):

You can get the build passing badge from Actions too (https://github.com/leanprover-community/mathlib/workflows/continuous%20integration/badge.svg?branch=master)

view this post on Zulip Joseph Myers (Oct 01 2020 at 19:35):

Before I add any of my British MO solutions, do people have comments on whether it would be appropriate to add a definition of odd (for nat and int) to mathlib, which simp would rewrite to ¬ even, to allow problem statements using "odd" to be expressed more literally? (As right now one of my solutions contains a local definition of odd, but if such a definition is appropriate in mathlib, it should go there instead.)

view this post on Zulip Daniel Selsam (Oct 01 2020 at 19:36):

FWIW I am strongly in favor of having a definition for odd.

view this post on Zulip Rob Lewis (Oct 01 2020 at 19:38):

@Daniel Selsam Oh, the current Actions script doesn't like it when you force push to master. If you force the lean-3.20.0 branch to match master it will be happy

view this post on Zulip Daniel Selsam (Oct 01 2020 at 23:30):

@Floris van Doorn your proof of IMO-2019-q4 https://gist.github.com/fpvandoorn/e0bd9d116a59a5f01d1d661f3677b72f and the gist it refers to prove a bunch of basic facts that presumably merit being in Mathlib. Might you have time at some point to add these to Mathlib so we can revive a clean proof for the new repo https://github.com/IMO-grand-challenge/olympiad-problems/tree/master/src/imo ? I am not sufficiently up-to-speed yet on library status/style/organization.

view this post on Zulip Scott Morrison (Oct 01 2020 at 23:39):

I really hope this won't get in the way of contributing stuff into mathlib. e.g. seeing suggestions above that a separate repository would allow for definitions of games, etc, worries me --- combinatorial game theory should definitely be in scope. In fact, I would say that any definition appropriate for setting up the statement of an IMO problem is appropriate for mathlib.

view this post on Zulip Scott Morrison (Oct 01 2020 at 23:40):

I'd suggest writing clear contributor guidelines for this new repository, stating explicitly that PR requests that introduce new definitions and lemmas of general interest can not be merged until those parts have been merged into mathlib.

view this post on Zulip Scott Morrison (Oct 01 2020 at 23:40):

And I would recommend not creating a for_mathlib directory. It serves no purpose, except to accumulate debt.

view this post on Zulip Scott Morrison (Oct 01 2020 at 23:44):

(I think this ship has sailed, but my preference would have been to follow a suggestion I think @Heather Macbeth made --- that we should continue to add IMO problems to mathlib, but to think of this as an incubation period, with the intention that once we have about ~100 IMO problems formalised, we will break them out into a separate repository. After this period we can be reasonably confident that the background mathematics to "do the IMO" is largely in mathlib, so we're at less risk from losing good material. In the meantime perhaps we could appoint an IMO-specific maintainer --- e.g. @Daniel Selsam --- with the intention that they would also help organise the transition out of incubation.)

view this post on Zulip Joseph Myers (Oct 02 2020 at 00:04):

Filed #4357 to define odd (for integers and natural numbers), to allow a more literal formal translation of problems mentioning odd numbers.

view this post on Zulip Joseph Myers (Oct 02 2020 at 00:08):

Scott Morrison said:

And I would recommend not creating a for_mathlib directory. It serves no purpose, except to accumulate debt.

So the for_mathlib directory currently there should be deleted.

view this post on Zulip Joseph Myers (Oct 02 2020 at 00:11):

Scott Morrison said:

(I think this ship has sailed, but my preference would have been to follow a suggestion I think Heather Macbeth made --- that we should continue to add IMO problems to mathlib, but to think of this as an incubation period, with the intention that once we have about ~100 IMO problems formalised, we will break them out into a separate repository. After this period we can be reasonably confident that the background mathematics to "do the IMO" is largely in mathlib, so we're at less risk from losing good material. In the meantime perhaps we could appoint an IMO-specific maintainer --- e.g. Daniel Selsam --- with the intention that they would also help organise the transition out of incubation.)

You could easily do 100 IMO problems without having much of the background mathematics needed to do problems involving geometry or graph theory (the weakest areas of IMO mathematics in mathlib at present).

view this post on Zulip Daniel Selsam (Oct 02 2020 at 00:12):

@Scott Morrison Ship has definitely not sailed -- I only made the repo this morning since Rob suggested it.

view this post on Zulip Daniel Selsam (Oct 02 2020 at 00:12):

Only a very small sunk cost if we rollback.

view this post on Zulip Scott Morrison (Oct 02 2020 at 00:13):

Sorry, maybe I overstated my objection. I also really don't want to get in the way of you making stuff happen! On the IMO front I'm not actually going to contribute much either way, so I'm definitely in the category of armchair critics here. :-)

view this post on Zulip Scott Morrison (Oct 02 2020 at 00:13):

That said, I'm happy to review PRs about IMO problems, and to encourage moving material into src/. I definitely think we want as many IMO problems formalised as we can get.

view this post on Zulip Scott Morrison (Oct 02 2020 at 00:14):

They are also a great opportunity for people to practice and contribute to Lean even if they don't want to do "theory building" type mathematics.

view this post on Zulip Joseph Myers (Oct 02 2020 at 00:15):

I know there's various graph theory stuff on branches. I'd like to see more PRs of that work so none of it lives on a branch for too long. At present, it would be awkward to formalise solutions of 2019 problem 3 or 2020 problem 3 without duplicating such not-on-master graph theory work (e.g. about connected graphs / connected components). If we try to keep things so that almost all graph theory work is on master, it's easier for problem solutions to build on it (and thus to add lemmas to the graph theory in mathlib when they are found to be useful for problems).

view this post on Zulip Daniel Selsam (Oct 02 2020 at 00:20):

@Scott Morrison I interpreted Rob's original suggestion as a request, i.e. as a polite way of saying that the IMO formalizations might put unwanted burden on mathlib. I was more just trying to be helpful than "making stuff happen". If the mathlib community is serious about wanting almost all the background math in mathlib (so the separate repo wouldn't even have a separate lib or for-mathlib), then I agree with you and @Heather Macbeth that incubating them in mathlib for now is the way to go.

view this post on Zulip Scott Morrison (Oct 02 2020 at 00:22):

I think there's still a spread of opinion about what belongs in mathlib. I think Rob very correctly wants us to work out how to do development across multiple repositories. He has set up a nice scheme for doing cross-project CI, and we really should try it out (more). With the IMO work having some momentum now, and an obvious lead (i.e. you) it seems like a good candidate.

view this post on Zulip Scott Morrison (Oct 02 2020 at 00:23):

Mostly I'm just scared of for_mathlib directories. I've made them too. :-)

view this post on Zulip Daniel Selsam (Oct 02 2020 at 00:25):

It seems problematic if every IMO PR is now split into 2, one for mathlib (where the lemmas are not even used) and one for the olympiad-problems repository.

view this post on Zulip Joseph Myers (Oct 02 2020 at 00:27):

The IMO Grand Challenge may eventually need some way to mark up the parts of a problem that a solver must fill in, but I'm not even sure of that. (A solver could be presented with a series of definitions, where those defined to sorry must be filled in. If such a definition has a non-Prop type, it must be filled in with a human-acceptable witness for a "determine" problem, while if it has a Prop type (which may reference the non-Prop definitions, for the term proving the witness has the desired property) there are no such requirements on the term.) Beyond that, I'd expect any lemma or definition that's generic mathematics rather than specific to one problem to go in mathlib.

view this post on Zulip Reid Barton (Oct 02 2020 at 00:29):

I agree, there will (hopefully!) come a time when the IMO problem formalization effort can stand on its own outside mathlib, but at this point I think the technical and social overhead of splitting it off is too high.

view this post on Zulip Reid Barton (Oct 02 2020 at 00:30):

Consider that people continue to make workarounds for Lean core library issues in mathlib, when it would be quite easy to fix the issues upstream.

view this post on Zulip Reid Barton (Oct 02 2020 at 00:32):

It's basically the same principle that gives rise to for_mathlib directories in the first place--it's too much trouble to make coordinated PRs to multiple projects.

view this post on Zulip Daniel Selsam (Oct 02 2020 at 00:34):

@Scott Morrison There seems to be a consensus that incubating in mathlib for now is the way to go. Do we have quorum? Should we consult more stakeholders before deciding?

view this post on Zulip Daniel Selsam (Oct 02 2020 at 00:35):

If we stick with mathlib for now, I will cancel my mathlib PR removing the IMO problems, issue a mathlib PR reviving Kevin's imo2019_q1, and delete the new repo.

view this post on Zulip Johan Commelin (Oct 02 2020 at 06:09):

I'm in favour of keeping mathlibs archive/imo for the time being. But I guess I'm like Scott: I won't be actively formalizing IMO problems, but I'm happy to review them.

view this post on Zulip Rob Lewis (Oct 02 2020 at 09:15):

So, I'm happy either way, as I haven't done more than trivial reviewing of IMO problem PRs and don't plan to in the future. But we've been having this discussion about external projects for a year and a half now. I guess my question is, if not now, then when? Yes, there's friction splitting a project off, but we won't find tools or workflows to reduce that friction unless we try. And I stand by what I wrote above (and agree with Daniel's additions) that IMO problems are a perfect case for a separate project.

view this post on Zulip Rob Lewis (Oct 02 2020 at 09:18):

For all the fear of for-mathlib directories: they work fine if someone feels responsible for flushing them. The witt_vector_preps file (on a branch of mathlib, but same idea) saw at least 2k lines go in and out. It's empty now.

view this post on Zulip Rob Lewis (Oct 02 2020 at 09:21):

I don't think there's tension between an IMO repo and mathlib -- the IMO repo depends on mathlib being maintained and growing, and from the mathlib side, it's cool to see fun problems being formalized using the library, not to mention future automation that could come from it. There's plenty of incentive on both sides to get the mathlib-appropriate material into mathlib.

view this post on Zulip Joseph Myers (Oct 02 2020 at 10:40):

My view: I'm not very concerned with whether a separate repository is used or not, as long as we don't have for_mathlib and have a strong policy to put relevant definitions and lemmas in mathlib proper before using them in an olympiad solution on master. If the scope grows beyond the 368 past IMO problems to a formal version of the AoPS contests collection with thousands of problems from different competitions, that probably belongs outside mathlib, but even then it could reasonably incubate in the mathlib archive for a while until big enough.

view this post on Zulip Joseph Myers (Oct 02 2020 at 10:54):

Most algebra and number theory problems and many combinatorics problems could probably be formalised now with at most a few small definitions and lemmas arising that are appropriate for mathlib. Geometry and combinatorial geometry are more likely to need hundreds or thousands of lines of preliminaries PRed to mathlib first, especially when a more literal geometrical interpretation is taken of combinatorial geometry problems that means there are lots of trivial-to-humans preliminaries to formalise first. (A good example might be IMO 2004 problem 3. Taken as a problem about fin m × fin n, there would be no particular obstruction to formalising it. Taking it literally as a geometrical problem, you also have to prove that the tiles are all aligned with the grid of squares in the rectangle containing them (obvious to humans) in order to reduce it to a combinatorics problem. I can come up with various suitably general statements about tilings (not just in the plane) that imply this, but that would involve a large amount of work on formalising things about tilings in mathlib before we get to the point of being able to reduce the geometrical problem to a combinatorial one.)

view this post on Zulip Kevin Lacker (Oct 02 2020 at 16:11):

so what's the status on this - @Daniel Selsam are we sticking with mathlib? I have another PR and want to know what repo to send it to

view this post on Zulip Kevin Lacker (Oct 02 2020 at 16:24):

if everyone agrees to keep it in mathlib, just stay silent

view this post on Zulip Rob Lewis (Oct 02 2020 at 16:26):

Just send it to mathlib for now, if things change it won't be lost.

view this post on Zulip Kevin Lacker (Oct 02 2020 at 16:30):

great, here we go: https://github.com/leanprover-community/mathlib/pull/4366

view this post on Zulip Daniel Selsam (Oct 02 2020 at 16:34):

@Rob Lewis @Reid Barton @Johan Commelin @Kevin Lacker @Heather Macbeth @Scott Morrison Thank you all for taking the time to weigh in on this. I apologize for any confusion or complication caused by my rash repository-creation. Let's continue to incubate the IMO problems in mathlib for now. Summary:

  • At this stage, almost every new IMO problem will require new lemmas, and most mathlibbers seem interested in getting most of these lemmas into mathlib. Almost every PR would need to be a double PR.
  • The goal right now is less about accumulating IMO problems and prototyping automation, and more about using it as an exercise to fill in important gaps in mathlib.
  • I prefer not to take a leadership role with the IMO formalizations until Lean4 is in place and we can co-develop the formalizations with the automation.
  • We can easily port to a separate repository in the future, e.g. once most new problems do not require significant for-mathlib components, and when we can write automation in Lean4.

view this post on Zulip Kevin Lacker (Oct 02 2020 at 16:36):

great. the next step IMO (in my opinion... sigh) is getting all the random IMO formalizations that somebody stuck in a gist, into the repo

view this post on Zulip Daniel Selsam (Oct 02 2020 at 16:40):

I revived Kevin Buzzard's imo2019_q1, and can issue a mathlib PR for it. Floris' imo2019_q4 https://gist.github.com/fpvandoorn/e0bd9d116a59a5f01d1d661f3677b72f introduces a bunch of new lemmas.

view this post on Zulip Floris van Doorn (Oct 02 2020 at 18:35):

I will submit a PR for my IMO 2019 Q4 solution soon!


Last updated: Aug 05 2021 at 04:14 UTC