Stream: Machine Learning for Theorem Proving

Topic: meaning of "determine number"

Tomas Skrivan (Nov 24 2022 at 18:02):

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.

Damiano Testa (Nov 24 2022 at 18:15):

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 (Nov 24 2022 at 18:23):

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

Eric Wieser (Nov 24 2022 at 18:23):

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

Johan Commelin (Nov 24 2022 at 18:26):

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 (Nov 24 2022 at 18:29):

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 (Nov 24 2022 at 18:29):

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

Eric Wieser (Nov 24 2022 at 18:30):

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

Damiano Testa (Nov 24 2022 at 18:30):

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

Eric Wieser (Nov 24 2022 at 18:31):

What if the question was asking for the least integer?

Johan Commelin (Nov 24 2022 at 18:31):

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 (Nov 24 2022 at 18:32):

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 (Nov 24 2022 at 18:32):

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

Johan Commelin (Nov 24 2022 at 18:33):

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

Damiano Testa (Nov 24 2022 at 18:33):

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

Damiano Testa (Nov 24 2022 at 18:37):

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 (Nov 24 2022 at 18:48):

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 (Nov 24 2022 at 18:49):

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

Kyle Miller (Nov 24 2022 at 19:02):

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 (Nov 24 2022 at 19:52):

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 sorry`s 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 (Nov 24 2022 at 20:04):

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

Last updated: Dec 20 2023 at 11:08 UTC