meaning of "determine number"

Stream: Machine Learning for Theorem Proving

[Tomas Skrivan]

In the Meta IMO result thread, the IMO 2006 problem 3 was mentioned and it got me wondering. How one formalizes the "Determine the least real number such and such ...". What does "determine" mean?

I'm suspecting that showing the set of all the number satisfying the inequality, proving it is bounded from belo, closed and taking its infimum is not sufficient. Mainly because it involves noncomputable operation infimum. But with reals it is a bit tricky to say what is computable and what not.

The only way I can make sense out of it is to first define an inductive data type for expressions involving rational numbers and allowed binary and unary functions like +,-,*,/,√,... Also define a map from these expression to reals.
The "determine" means, find a computable element of these expressions such that it satisfies the inequality if interpreted as a real number.

What I find interesting is that the only way I can come up with formalization of it involves computability.

I know very little about this topic, do people use (non)computability to formalize IMO problems?

[Damiano Testa]

In this particular case, you could argue that the infimum is actually a minimum, since, by homogeneity, you can restrict the computation to the a, b, cs on the unit sphere, a compact manifold. Since the resulting function is differentiable, the minimum will be achieved at a point where the derivatives vanish, so the choices of a, b, c will be contained in a set defined by polynomial equations. Thus, the "infimum" is actually an algebraic number: these should be computable!

Still, I agree with you that the interpretation "the set of Ms is closed, non-empty and bounded below" could be viewed as sufficient.

[Eric Wieser]

"determine the least x such that P x" could be interpreted as "fill in the blank in is_least {x | P x} _"

[Eric Wieser]

Just like "determine the value of 2 + 2" means "fill in the blank in 2 + 2 = _ "

[Johan Commelin]

[Troll alert!]
I think that second blank can be filled in really well with the term 2 + 2.
In a similar vein, I think min {x | P x} is a great way to fill in the first blank.

---

This observation isn't new. But so far, it has posed a really annoying problem to formally posing a large class of "exercises"/"problems".

[Eric Wieser]

In a similar vein, I think min {x | P x} is a great way to fill in the first blank.

Seems pretty lousy to me, that's a type error :upside_down:

[Damiano Testa]

When the answer is an algebraic number, you could ask for a non-zero polynomial with integer coefficients satisfied by the solution.

[Eric Wieser]

Sure, i'll use X - C (Inf {x | P x}) as my polynomial

[Damiano Testa]

you need to prove the answer is an integer...

[Eric Wieser]

What if the question was asking for the least integer?

[Johan Commelin]

Damiano Testa said:

When the answer is an algebraic number, you could ask for a non-zero polynomial with integer coefficients satisfied by the solution.

I would just use minpoly ℤ x.

[Damiano Testa]

Then I would reformulate the question, but would need to think about how to formulate it. An answer could be write it in the form succ (succ (succ ... 0)... :upside_down:

[Johan Commelin]

But that's not something that can be checked using the type system. A tactic could inspect the expression.

[Johan Commelin]

And I think we should look in that direction for a solution.

[Damiano Testa]

as for the minpoly: you could similarly require the coefficients to be written in "iterated succ" form.

[Damiano Testa]

but this is now veering towards the discussion of "what is a closed expression": for instance, is the sum of the first natural numbers $\sum_{i \le n}i$? Is $\binom{n+1}{2}$ "better"? Why?
[Of course the binomial is the "correct" answer, but actually justifying it in absolute terms is tricky.]

[Damiano Testa]

I might be too strict, but if the answer is 9, I would probably just require that the expr of the answer equals `(9)...

[Damiano Testa]

Thus, no 9+0 or 3 ^ 2 allowed either! :smile:

[Kyle Miller]

How are IMO problem solutions evaluated? It seems to me that the collection of terms that would actually be accepted would be relatively small -- it's like the problem is "what number am I thinking of?" along with an elaborate hint, and in the end the goal is to guess an acceptible form.

[Joseph Myers]

I'll repeat my previous suggestion: a formal problem statement involves a series of definitions, some of which have a type provided and sorry as the definition, where some of the types may refer back to previous definitions. A solver must exhibit terms for all the types where sorry was the definition. If such a type was not a Prop, the term provided by the solver must also satisfy human review as being a legitimate answer to the problem. So for "determine the least real number", there would be at two sorrys to fill in, one to be filled in with a real number (subject to human review for whether it's a legitimate answer) and one to be filled in with a proof that that real number satisfies the conditions of the problem (to be verified automatically by whether the proof type-checks). No computability is involved.

[Joseph Myers]

I checked the mark scheme for IMO 2006 problem 3 (I was at that IMO as an observer). It doesn't say anything about what expressions count as legitimate forms of $9\sqrt{2}/32$.