How to help?

Stream: IMO-grand-challenge

[Jason Rute]

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

[Daniel Selsam]

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.

[Daniel Selsam]

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

[Daniel Selsam]

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

[Floris van Doorn]

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.

[Daniel Selsam]

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

[Johan Commelin]

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.

[Patrick Massot]

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.

[Johan Commelin]

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.

[Daniel Selsam]

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.

[Daniel Selsam]

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.

[Daniel Selsam]

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?

[Floris van Doorn]

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

[Daniel Selsam]

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

[Floris van Doorn]

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.

[Daniel Selsam]

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

[Daniel Selsam]

Even finiteness is too weak.

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

[Floris van Doorn]

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

[Johan Commelin]

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.

[Daniel Selsam]

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.

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Chris Hughes]

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)

[Daniel Selsam]

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

[Johan Commelin]

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.

[Johan Commelin]

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

[Johan Commelin]

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

[Patrick Massot]

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?

[Johan Commelin]

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 (-;

[Johan Commelin]

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

[Daniel Selsam]

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

[Daniel Selsam]

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

[Daniel Selsam]

(deleted)

[Daniel Selsam]

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.

[Blake Elias]

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?

[Daniel Selsam]

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

[Daniel Selsam]

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.

[Johan Commelin]

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.

[Daniel Selsam]

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.

[Johan Commelin]

Alas...