formalizing IMO problems

Stream: IMO-grand-challenge

[Kevin Lacker]

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:

[Kevin Lacker]

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.

[Kevin Lacker]

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

[David Shin]

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

[Kevin Buzzard]

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.

[Kevin Lacker]

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

[Miroslav Olšák]

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.

[Miroslav Olšák]

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? :-)

[Kevin Buzzard]

no because there is no notation for natural number division

[Kevin Buzzard]

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.

[Kevin Lacker]

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

[Kevin Lacker]

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

[Qian Hong (wechat: fracting)]

Has IMO 2019 been formalized in Lean?

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

[Kevin Buzzard]

Not the geometry questions, but some of the rest.

[Qian Hong (wechat: fracting)]

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

[Kevin Buzzard]

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

[Kevin Lacker]

@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

[Daniel Selsam]

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

[Daniel Selsam]

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

[Daniel Selsam]

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.

[Kevin Lacker]

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

[Daniel Selsam]

Theirs uses blast, smt, auto, and simp.

[Rob Lewis]

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.

[Rob Lewis]

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.

[Daniel Selsam]

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

[Daniel Selsam]

@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

[Joseph Myers]

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?

[Rob Lewis]

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.

[Daniel Selsam]

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.

[Rob Lewis]

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

[Joseph Myers]

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).

[Rob Lewis]

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

[Daniel Selsam]

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.

[Rob Lewis]

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

[Rob Lewis]

Aha, you're ahead of me :)

[Joseph Myers]

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

[Patrick Massot]

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.

[Rob Lewis]

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

[Rob Lewis]

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

[Rob Lewis]

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

[Daniel Selsam]

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.

[Daniel Selsam]

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

[Joseph Myers]

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

[Rob Lewis]

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.

[Joseph Myers]

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.

[Joseph Myers]

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.

[Daniel Selsam]

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

[Oliver Nash]

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?

[Joseph Myers]

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?

[Joseph Myers]

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)?

[Rob Lewis]

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.

[Oliver Nash]

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.

[Daniel Selsam]

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

[Oliver Nash]

OK go for it!

[Joseph Myers]

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.

[Oliver Nash]

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!

[Kevin Lacker]

@Oliver Nash which problem?

[Oliver Nash]

1998 Q2

[Kevin Lacker]

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

[Kevin Lacker]

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

[Daniel Selsam]

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

[Kevin Lacker]

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

[Joseph Myers]

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.

[Kevin Lacker]

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

[Kevin Lacker]

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"

[Rob Lewis]

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.

[Daniel Selsam]

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

[Rob Lewis]

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

[Rob Lewis]

The perfectoid CI is way out of date

[Daniel Selsam]

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

[Rob Lewis]

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.

[Rob Lewis]

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.

[Rob Lewis]

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

[Daniel Selsam]

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

[Rob Lewis]

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

[Joseph Myers]

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.)

[Daniel Selsam]

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

[Rob Lewis]

@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

[Daniel Selsam]

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

[Scott Morrison]

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.

[Scott Morrison]

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.

[Scott Morrison]

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

[Scott Morrison]

(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.)

[Joseph Myers]

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

[Joseph Myers]

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.

[Joseph Myers]

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).

[Daniel Selsam]

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

[Daniel Selsam]

Only a very small sunk cost if we rollback.

[Scott Morrison]

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. :-)

[Scott Morrison]

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.

[Scott Morrison]

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.

[Joseph Myers]

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).

[Daniel Selsam]

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

[Scott Morrison]

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.

[Scott Morrison]

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

[Daniel Selsam]

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.

[Joseph Myers]

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.

[Reid Barton]

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.

[Reid Barton]

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.

[Reid Barton]

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.

[Daniel Selsam]

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

[Daniel Selsam]

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.

[Johan Commelin]

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.

[Rob Lewis]

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.

[Rob Lewis]

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.

[Rob Lewis]

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.

[Joseph Myers]

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.

[Joseph Myers]

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.)

[Kevin Lacker]

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

[Kevin Lacker]

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

[Rob Lewis]

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

[Kevin Lacker]

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

[Daniel Selsam]

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

[Kevin Lacker]

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

[Daniel Selsam]

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.

[Floris van Doorn]

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

[James Gallicchio]

Is there a list being maintained somewhere of which problems haven't been done yet and might be on the easier side? I have some motivated Lean newbies who are looking for cool problems to try and tackle :)

[Joseph Myers]

There are 380 past IMO problems and only 30 in the mathlib archive plus 4 more with open PRs; anything not on either of those lists probably hasn't been done yet. Most algebra and number theory problems should be accessible (provided you start with a good mathematical understanding of the informal solution you are trying to formalize, as is always important for formalizing anything), most geometry will be inaccessible because of missing API in mathlib (I'm working towards the API needed for IMO 2019 Q2) and accessibility of combinatorics problems will vary. Note archive/imo/README.md: much of the benefit of such formalizations comes from the resulting additions to mathlib proper, whenever they suggest some missing piece of more generally applicable API.

[Joseph Myers]

I have a maximalist view of what's appropriate for mathlib right now - anything adding definitions or proving results that can reasonably be considered known mathematics from the literature should by default be appropriate for mathlib or the mathlib archive (the choice depending on how likely other results are to build on the definitions and results in question), once up to mathlib quality standards - and "mathematics" here broadly covers those mathematical sciences where formalization makes sense (including for software verification). That includes all IMO problems for the mathlib archive.

[James Gallicchio]

Good to know, thanks! I'll look for some good algebra/number theory ones to suggest for them :)

[Trieu Trinh]

For geometry, even humans solve the problem by relying on the diagram. Unordered geometry helps with reducing case analysis but not a guarantee. I don't see much value from similar proofs for different cases (e.g.C is inside or outside segment AB) For the IMO grand challenge, wouldn't it make sense to, as 1st goal, relax geometry problems to "Given a problem description and an accurate diagram (Krueger 2021), solve it". So now facts like "AB = AC + CB" or "AB = AC - CB" (similar for angle algebra), ... will be taken from the diagram and used as part of the proof (just like how humans do it).

[Joseph Myers]

I don't see any reason to treat geometry differently from other subject areas in IMO Grand Challenge rules - the formal statement should accurately correspond to the informal one, and then it's up to the AI writing the formal proof to fill in all the trivialities that could be skipped over in an informal proof - just as in other subject areas. Of course an AI might well draw a diagram internally and use that to work out conjectures for intermediate steps to prove.

It does seem that when the informal proof is straightforward, proving the trivialities required to apply the formal lemmas corresponding to the steps of the informal proof can actually take up most of the formal proof - that's what I'm finding as I move from building up API anticipated to be needed for IMO 2019 Q2 to actually filling out the formal proof of the problem itself.

[Trieu Trinh]

Joseph Myers said:

I don't see any reason to treat geometry differently from other subject areas in IMO Grand Challenge rules - the formal statement should accurately correspond to the informal one, and then it's up to the AI writing the formal proof to fill in all the trivialities that could be skipped over in an informal proof - just as in other subject areas. Of course an AI might well draw a diagram internally and use that to work out conjectures for intermediate steps to prove.

In terms of formalizing the problem I completely agree.

On the other hand, I want to understand more what is considered an acceptable "solution" coming from an actual IMO human contestant. When seeing point C lying in between A and B, would it make sense for an IMO contestant to (1) use "AB = AC + CB", or do they have to (2) prove that C is indeed in between A and B, or (3) choose a different path that does not involve such algebra?

My understanding is that it has to be either (2) - which sometimes can be hard and/or tedious, or (1) with additional case analysis where C is not in between AB. Further, if (1) is done without extra cases, how would judges go about evaluating such solutions?

One example I have in mind is

Here what to prove is, for example, F being in between B and C; So we need to prove the projection of the intersection of two internal bisectors lies inside the triangle's side. I suppose this is what you mean by:

It does seem that when the informal proof is straightforward, proving the trivialities required to apply the formal lemmas corresponding to the steps of the informal proof can actually take up most of the formal proof.

Does forcing the AI going through this make the problem significantly harder than it is for a human? If so, lowering the bar to human-level seems like a reasonable intermediate goal regarding "IMO grand AI challenge". Of course, if we can do away with this and AI can go all the way then this will be a distraction, but is it?

[Joseph Myers]

Typically recent IMO geometry problems will include e.g. betweenness conditions in the problem statement to avoid contestants needing to deal with multiple configurations, and contestants won't be expected to prove e.g. a betweenness property that is obvious from a diagram of the one permitted configuration.

Of course a contestant's solution might introduce its own configuration dependence. I'm formalising solution 1 to IMO 2019 Q2, but solution 2 involves a case distinction on whether two lines are parallel, and contestants using that approach did have to deal with both cases (rather than just using the intersection point of those lines and ignoring or not noticing the case where they are parallel) to get full marks.

Or sometimes the use of configuration information is nontrivial and important to the problem in some way. E.g. IMO 2002 problem 2, where the angle condition was needed to get the incentre rather than the excentre and failing to say anything about the use of that condition lost a mark.

In the example you mention, "an intouch point is in the interior of a face" (for a general simplex, not just the two-dimensional case) seems like a result appropriate for mathlib proper (just as in any area of mathematics, there are many trivial lemmas to put in mathlib to get a good API).

The IMO Grand Challenge being F2F does indeed make some things harder than for humans, but I don't think requiring geometrical trivialities to be justified is any different from requiring trivialities in other subject areas to be justified in the F2F IMO Grand Challenge.

An I2I version (AI receives the paper in up to three human languages, as provided to contestants, writes an informal solution and has it graded by coordinators familiar with the mark scheme and how it was applied in coordination of human solutions) would be perfectly reasonable - any AI that can achieve enough points in that (on a future IMO, using a version of the AI from before contestants started sitting that IMO's papers) to reach the gold medal boundary for that IMO would have made a very major achievement in AI.

But F2F has obvious advantages for people developing such an AI, that may well outweigh needing to prove trivialities (which it might well be possible to write tactics to prove). The mark schemes aren't generally public and aren't systematically collected anywhere. If you find willing coordinators from past IMOs to grade I2I attempts, the number of attempts they can grade is limited, whereas an F2F AI can have millions of attempts graded automatically, as well as getting instant feedback while working on a problem about what is or isn't a valid argument. You still need conventions about how to translate the informal problem to the formal one, but those can be written in a very detailed and objective way (and conventions for other proof assistants could be written and agreed to be equivalent to the Lean ones in the sense of giving the AI the same information).

[David Wärn]

Trieu Trinh said:

One example I have in mind is

I would say the scalable way to deal with this kind of case analysis is to remember the order in which you compare segments. E.g. when you say CJ = KC, what you really mean is the one bit stronger statement that CJ maps to (a translate of) KC after reclection in HC. I don't know any situation where one still has to do a case analysis after working with directed things in this way (it somehow wouldn't make sense -- when proving a polynomial identity, you never say "if x < 0, then ... else ..."). Students often write arguments with undirected angles where there's some case analysis missing that becomes unnecessary using directed angles. People have different ideas about how to mark such scripts, but many seem to agree it would be unfair to punish students for not knowing about directed angles. But I do think an AI solver should understand this sort of thing