Zulip Chat Archive

Stream: IMO-grand-challenge

Topic: How to help?


view this post on Zulip Jason Rute (Sep 09 2019 at 13:06):

@Daniel Selsam What you are most looking for from the Lean community. How would you like the community to help?

view this post on Zulip Daniel Selsam (Sep 09 2019 at 13:25):

I was in top-10 in Team Russia try outs for IMO 2002, so if you need a help from someone familiar with this type of problems, you may ping me.

@Yury G. Kudryashov Hi Yury, thanks for the offer.

view this post on Zulip Daniel Selsam (Sep 09 2019 at 15:00):

Daniel Selsam What you are most looking for from the Lean community. How would you like the community to help?

@Jason Rute Great question! I would love for the community to continue discussing design issues in the formal encoding and to start (pseudo-)formalizing many historical problem statements. The main goal now is not to accumulate formal statements but to discover the conceptual challenges with the F2F formulation as efficiently as possible.

I will soon push a description of a few of the design challenges to https://github.com/IMO-grand-challenge/formal-encoding

view this post on Zulip Daniel Selsam (Sep 09 2019 at 15:47):

@Jason Rute FYI pushed https://github.com/IMO-grand-challenge/formal-encoding/blob/master/design/determine.lean

view this post on Zulip Floris van Doorn (Sep 09 2019 at 18:05):

In response to the determine file: I was also thinking a bit about this exact problem how to translate these problems.
The third proposal, using the solution set, is also not adequate. determineSolutionSet X s_0 is equivalent to showing that s_0 is countable: I can define (with a little bit of work) a SolutionSet witness using choice if I have proven that s_0 is countable.

I think a reasonable (but not completely satisfactory) solution is to change all problems of the form "determine all f that satisfy P f" to "Show that for all f we have P f iff f is in an explicitly given solution set". Of course, this is unsatisfactory, since we're already "giving the answer" to the program. Though I think that everyone will agree that finding the answer is not the "hard part" of a problem.

Another possible option is that we do require the F2F programs to find the solutions themselves, but that the solution can only use certain specific "whitelisted" definitions from the library, and no other definitions. There might be issues in deciding which definitions are allowed so that we avoid all unsatisfactory answers.

view this post on Zulip Daniel Selsam (Sep 09 2019 at 18:12):

@Floris van Doorn Hi Floris, thanks for pointing out that countablyInfinite is not "sound", in that it permits unacceptable solutions using choice. I will add that to the document, and to remove any possibility of a similar issue, I will remove the entire clause in the tentative proposal that allows for specific solution formats to be accepted without inspection. As for the "whitelist", this would be great but I am skeptical that it will be possible. Do you find the tentative proposal to be a reasonable compromise?

view this post on Zulip Johan Commelin (Sep 09 2019 at 18:15):

In some sense this just shows that the IMO problem is badly specified... we have this issue with exams as well. If you ask a question like this in Germany, you will always have students who will prove this by the informal analogue of \<_, iff.refl _\>. And if you don't give them full points, they might even threaten to sue the university... things like this have really happened.

view this post on Zulip Patrick Massot (Sep 09 2019 at 18:15):

Floris, I don't think you can say "everyone will agree that finding the answer is not the "hard part" of a problem". Even the easy 2019 Q1 becomes much easier if you give the solution set.

view this post on Zulip Johan Commelin (Sep 09 2019 at 18:16):

I do agree that it would be nice to keep the "find the solution" part. But I don't know how to formalize what that means.

view this post on Zulip Daniel Selsam (Sep 09 2019 at 18:16):

Though I think that everyone will agree that finding the answer is not the "hard part" of a problem.

@Floris van Doorn I think the challenge must include the finding part as well as the proving part.

view this post on Zulip Daniel Selsam (Sep 09 2019 at 18:18):

In some sense this just shows that the IMO problem is badly specified...

@Johan Commelin Imprecisely specified, yes, but one could argue that it is an interesting part of the challenge that one must have enough common sense to distinguish acceptable solutions from unacceptable ones.

view this post on Zulip Daniel Selsam (Sep 09 2019 at 18:20):

If you ask a question like this in Germany, you will always have students who will prove this by the informal analogue of \<_, iff.refl _\>. And if you don't give them full points, they might even threaten to sue the university... things like this have really happened.

@Johan Commelin Seriously? Is that folklore or do you have a source?

view this post on Zulip Floris van Doorn (Sep 09 2019 at 18:23):

@Daniel Selsam I don't think the proposal is reasonable. Looking at IMO 2019-4, It is decidable to check whether a specific pair (n,k) is a solution, so I think the degenerate solution falls into the category "will get full score without inspection" (if I understand your proposal correctly).

Even finiteness is too weak. Suppose a program proves that if (n,k) is a solution to IMO 2019-4, then the inequality n, k < 10^(10^100) holds. We can then apply the degenerate solution. A human solution like that will be rejected (you are not allowed to omit a finite but infeasible amount of work).

view this post on Zulip Daniel Selsam (Sep 09 2019 at 18:25):

@Floris van Doorn I removed that clause. Please reload the page.

view this post on Zulip Floris van Doorn (Sep 09 2019 at 18:25):

Ok, I agree that giving the answer does make the problem easier. It's a useful hint to determine what proof approaches are likely to work.

view this post on Zulip Daniel Selsam (Sep 09 2019 at 18:25):

I agree that we should not try to be clever and should require all witnesses be sanity-checked by humans.

view this post on Zulip Daniel Selsam (Sep 09 2019 at 18:29):

Even finiteness is too weak.

@Floris van Doorn Thanks, great example. I will add that to the page.

view this post on Zulip Floris van Doorn (Sep 09 2019 at 18:29):

Oh sorry, you want to manually check all answers.
That is a reasonable compromise. It will be an extra challenge to the solvers: they have to define the solution set in a human-understandable way (so not buried behind a ton of definitions).

view this post on Zulip Johan Commelin (Sep 09 2019 at 18:33):

I don't have a precise source, but I hear these stories now and then... the professors in my department are really careful nowadays with how they handle students, exams, and all that. I've been present at several "Klausureinsichten" (where students come to see their grade, and the corrected exam). It's completely absurd. Never seen anything like that before. But I guess the most juicy stories are actually folklore, and jucier than what used to be their source in distant past.

view this post on Zulip Daniel Selsam (Sep 09 2019 at 18:34):

It will be an extra challenge to the solvers: they have to define the solution set in a human-understandable way (so not buried behind a ton of definitions).

@Floris van Doorn Yes, it is an extra challenge to the solvers, compared to a completely F2F version.

view this post on Zulip Kevin Buzzard (Sep 09 2019 at 19:06):

I was once personally faced with this: https://bmos.ukmt.org.uk/home/fist-1986.pdf . Question 2 is "find the real number which is the supremum of this explicit non-empty bounded set". I realise I am a bit confused about how to formalise this. I feel like the real question is "give a finite sequence of buttons which one can press on a calculator, such that after you've pressed them, the answer is on the screen".

view this post on Zulip Kevin Buzzard (Sep 09 2019 at 19:07):

[NB I got that paper from here: https://bmos.ukmt.org.uk/home/bmo.shtml -- big library of the training materials used by the UK for many years]

view this post on Zulip Chris Hughes (Sep 09 2019 at 19:26):

You can always ask for an explicit term of this type for the witness. I'm not sure if this covers every single "find this real" question

import analysis.complex.exponential
open real

inductive calculatorable :   Type
| one : calculatorable 1
| zero : calculatorable 0
| pi   : calculatorable real.pi
| add :  x y, calculatorable x  calculatorable y 
  calculatorable (x + y)
| mul :  x y, calculatorable x  calculatorable y 
  calculatorable (x * y)
| div :  x y, calculatorable x  calculatorable y 
  calculatorable (x / y)
| sub :  x y, calculatorable x  calculatorable y 
  calculatorable (x - y)
| sqrt :  x, calculatorable x  calculatorable (sqrt x)
| sin :  x, calculatorable x  calculatorable (sin x)
| cos :  x, calculatorable x  calculatorable (cos x)
| exp :  x, calculatorable x  calculatorable (exp x)
| log :  x, calculatorable x  calculatorable (log x)

view this post on Zulip Daniel Selsam (Sep 09 2019 at 19:36):

@Chris Hughes Thanks. I would put this approach in the "whitelist" category. I am open to this kind of approach in principle but I fear that a fleshed out proposal would not only be complicated but would probably still be at risk of being either too forgiving or too restrictive or both.

view this post on Zulip Johan Commelin (Sep 09 2019 at 19:44):

If we do "inspection of results by humans" then we'll still have to engineer the tactics in such a way that they produce convincing results.

view this post on Zulip Johan Commelin (Sep 09 2019 at 19:44):

Once that is done, proving that the result is calculatorable for a some reasonable definition of calculatorable is of course trivial.

view this post on Zulip Johan Commelin (Sep 09 2019 at 19:45):

So I guess it doesn't really matter too much what we do.

view this post on Zulip Patrick Massot (Sep 09 2019 at 20:06):

https://github.com/IMO-grand-challenge/formal-encoding/blob/master/design/determine.lean

My Lean 4 expertise suggests this is meant to be Lean 4 code (I mean I see Camel case). Does it mean you actually use Lean 4? Is it already possible to so interactively (say with a VScode extension)? Or do you have to write the file and call Lean 4 on the command line?

view this post on Zulip Johan Commelin (Sep 09 2019 at 20:10):

It also seems \lam x, formula(x) got replaced with \lam x => formula(x). I very much applaud moving away from the comma, because it was used for too many other things. Even if Lean didn't get confused, I did (-;

view this post on Zulip Johan Commelin (Sep 09 2019 at 20:11):

Now we only need to make \mapsto notation for => and it will almost read like mathematics :stuck_out_tongue_wink:

view this post on Zulip Daniel Selsam (Sep 09 2019 at 20:32):

My Lean 4 expertise suggests this is meant to be Lean 4 code (I mean I see Camel case). Does it mean you actually use Lean 4? Is it already possible to so interactively (say with a VScode extension)? Or do you have to write the file and call Lean 4 on the command line?

@Patrick Massot Hi Patrick. Yes, I have been using Lean4 for my pseudo-formalizing (and also my actual programming), but it is not ready for proving theorems yet (there is not even a tactic framework).

view this post on Zulip Daniel Selsam (Sep 09 2019 at 20:33):

Emacs mode works just as well, after a little setup. I have never used VScode.

view this post on Zulip Daniel Selsam (Sep 09 2019 at 20:40):

(deleted)

view this post on Zulip Daniel Selsam (Sep 09 2019 at 20:45):

Daniel Selsam What you are most looking for from the Lean community. How would you like the community to help?

FYI To get started, I put a few "help requested"s in https://github.com/IMO-grand-challenge/formal-encoding/blob/master/design/transition_systems.lean (though I will probably switch to using GitHub Issues with RFC in the name). The high-level strategy I suggest is for us to go problem-class by problem-class (with some degree of parallelism), trying to encode a range of problem statements within each class in a uniform way while taking note of outliers and being conscious not to over-fit the details of historical problems.

view this post on Zulip Blake Elias (Sep 17 2019 at 18:54):

My two initial thoughts:

1) What is the simplest IMO problem for which we can produce a satisfactory formal statement in Lean?

Perhaps if we start with a few such examples, it will be easier to generalize to certain classes of such "simple" problems -- and then move on to trickier ones -- rather than immediately jumping in to ones with the trickiest issues.

2) IMO problems ask one to "find and prove", rather than just "prove".

The fact that one must first decide what theorem to prove, and then subsequently prove it, differentiates IMO from other theorem proving / synthesis tasks. I'm not sure what the tried-and-true way to represent such problems is - and perhaps that's part of the difficulty others have been running into when formalizing this task. I've seen discussions here distinguishing between "proof" and "witness" - I take it that gets at this distinction between one's answer and one's proof the answer is correct. Perhaps someone can explain with an example how those terms are being used?

view this post on Zulip Daniel Selsam (Sep 17 2019 at 19:12):

@Blake Elias Hi Blake, welcome!

1) What is the simplest IMO problem for which we can produce a satisfactory formal statement in Lean?
Perhaps if we start with a few such examples, it will be easier to generalize to certain classes of such "simple" problems -- and then move on to trickier ones -- rather than immediately jumping in to ones with the trickiest issues.

I'll just note that most historical problems in algebra and number theory are easy to state. The combinatorics ones are usually pretty easy to state individually, but it may still require careful design to state them in a convenient, uniform way.

view this post on Zulip Daniel Selsam (Sep 17 2019 at 19:17):

2) IMO problems ask one to "find and prove", rather than just "prove".

The fact that one must first decide what theorem to prove, and then subsequently prove it, differentiates IMO from other theorem proving / synthesis tasks. I'm not sure what the tried-and-true way to represent such problems is - and perhaps that's part of the difficulty others have been running into when formalizing this task. I've seen discussions here distinguishing between "proof" and "witness" - I take it that gets at this distinction between one's answer and one's proof the answer is correct. Perhaps someone can explain with an example how those terms are being used?

See https://github.com/IMO-grand-challenge/formal-encoding/blob/master/design/determine.lean for some notes on this issue. If we knew what type of object we were looking for, the "find" part would arguably be a standard synthesis problem. The issue is that we don't how to formally distinguish between "degenerate" solutions/witnesses and "acceptable" ones.

view this post on Zulip Johan Commelin (Sep 17 2019 at 19:28):

Would it help to require the "witness" part to be constructive? That would counter one of Floris's attacks, where he pointed out that one could use choice to get the witness.

view this post on Zulip Daniel Selsam (Sep 17 2019 at 19:39):

Would it help to require the "witness" part to be constructive? That would counter one of Floris's attacks, where he pointed out that one could use choice to get the witness.

@Johan Commelin Note that the Axiom of Choice is a theorem for encodeable types: https://github.com/leanprover-community/mathlib/blob/master/src/data/equiv/encodable.lean#L280-L283 . Also note that in the finite example Floris gave (https://leanprover.zulipchat.com/#narrow/stream/208328-IMO-grand-challenge/topic/How.20to.20help.3F/near/175269074) the witness type is List and yet the proof can be checked without actually computing the list.

view this post on Zulip Johan Commelin (Sep 17 2019 at 19:40):

Alas...


Last updated: Aug 05 2021 at 04:14 UTC