Here is a classic math olympiad problem (but this is NOT my question!): Each of the girls A and B tells the teacher a positive integer but neither of them knows the other's number. The teacher writes two distinct positive integers on the blackboard and announces that one of them is the sum of the numbers they told her. Then she asks A, “Do you know the sum of the two numbers?” If the answer is "no" then the teacher asks B the same question, and so on. Suppose the girls are truthful and intelligent. Prove that one of the answers will eventually be "yes".
(Source: "Mathematical Miniatures" by Svetoslav Savchev, Titu Andreescu, Mathematical Association of America, 2003).
(Solving this problem is not difficult, see e.g. the answers in https://math.stackexchange.com/questions/2819971/a-riddle-on-positive-integers)
Question: What is a good restatement of this problem in formal mathematical language? The informal statement of the problem above involves the concepts of knowledge and intelligence, which without careful formalization can lead to paradoxes (e.g. https://en.wikipedia.org/wiki/Unexpected_hanging_paradox). Clearly, one possible formalization is to define payoffs for the girls for answering the teachers question (e.g. payoff zero for answering "no", payoff minus infinity for answering "yes" and stating the wrong sum, payoff plus one for answering "yes" and stating the correct sum) and then setting this up as a two-player sequential game where the girls rationally maximize payoffs. I wonder whether there is a better formalization that stays closer to the informal statement above and avoids defining arbitrary payoffs?
(COMMENT: My original formulation of this question was not good, because it did not clarify right away that this "classic math olympiad problem" is not my question, and careful reading of the whole post was required to understand that. Therefore, within just a few hours of posting the question, it received 6 downvotes and only 1 upvote, and then was almost immediately closed. I strongly suspect that most of those 6 downvotes did only read the "classic math olympiad problem" and not my actual question. Within less than a day I then edited the question to avoid any misunderstanding for casual readers. Since that edit until now (within 30 days), this question has received 2 downvotes and 3 upvotes, but unfortunately has not been reopened, yet. Providing careful logical formalizations is clearly a question at the very heart of mathematics, e.g. the formalization in terms of rationally maximizing payoffs that I am alluding to above is simply a standard sequential game. So I am clearly asking a math question within the scope of this forum. I am obviously not interested in this little math olympiad problem itself -- that would not be research relevant -- but in the mathematical framework required for its formalization. For example, the Mathematics Magazine articles on "A Calculus for Know/Don't Know Problems" and "Goldbach, Lemoine, and a Know/Don't Know Problem" referenced by Gerald Edgar in his answer below are very relevant and interesting in that regard. By closing this question you have deprived other researchers from posting equally insightful answers, and you have deprived me of the benefit of those answers. I really hope you will reopen this question.)
