IMO 2026 Problem 1: exactly one entry survives, and its value is independent of the choices
ProvedIMO2026P1.imo2026_p1The goal: parts (a) and (b) of the problem. Starting from integers all greater than , the conclusion asserts two things at once.
First, a terminal board is actually reached — this is "after finitely many moves", and it keeps the rest from being vacuous.
Second, there is a value such that every reachable terminal board has exactly as its entries above . That bigPart t is the singleton is part (a): exactly one integer exceeds . That is quantified outside the is part (b): the value does not depend on Confucius's choices. Were quantified inside, the statement would say only that each terminal board carries some large entry, leaving different runs free to disagree — part (a) alone, with the independence claim silently dropped.
The hypothesis that the board has exactly entries is retained from the source, though no step of the argument uses it; the result holds for any nonempty board of entries greater than .
import Definitions.Def_IMO2026P1_Blackboard import Mathlib.Tactic
open IMO2026P1
theorem IMO2026P1.imo2026_p1 (s : Board)
(hcard : Multiset.card s = 2026) (hgt : ∀ x ∈ s, 1 < x) :
(∃ t, Reachable s t ∧ IsTerminal t) ∧
∃ M : ℕ, 1 < M ∧ ∀ t, Reachable s t → IsTerminal t → bigPart t = {M} := by sorryRead-back
What the Lean code literally says, in plain math · claude-opus-5
Read-backs
Throughout, a board is a finite multiset of natural numbers (repetitions allowed and counted, order irrelevant). For a board and a value , denotes the multiplicity of in , the product of all entries of (with repetition), and the number of entries of (with repetition). For , denotes the exponent of in the prime factorization of ; this is whenever is not prime, and for every when or .
Three auxiliary notions are used and are expanded inline below wherever they occur; they are recorded here once.
One move. (" is obtained from by one move") means: there exist natural numbers and with
where is with exactly one copy of deleted, and such that
That is: delete one copy of and one copy of from and insert the two values and . The division is truncated natural-number division. Note that and are values: the condition permits when that value occurs at least twice in , and it forces to contain at least two entries greater than (counted with multiplicity). The two inserted values are not required to exceed . Every move preserves the number of entries: .
Reachability. means is obtained from by a finite (possibly empty) chain of moves — the reflexive–transitive closure of . In particular always holds.
Terminal. is terminal means there is no board with . Since the target board in the definition of a move is produced by an explicit equation, this is the same as saying no admissible pair can be selected at all: does not contain two entries (with multiplicity) both greater than .
Big part. is the sub-multiset of consisting of exactly those entries that are greater than , with their multiplicities.
Exponent gcd. For and a board , is obtained by replacing each entry of by and folding the resulting multiset of natural numbers with , starting from the value ; since , this is the greatest common divisor of the numbers over all entries of , with . Entries equal to or contribute the value and therefore do not change the result. If is not prime then for every and for every board .
IMO2026P1.imo2026_p1
Let be a board (explicit argument: a finite multiset of natural numbers) satisfying two hypotheses:
- : the number of entries of , counted with multiplicity, is exactly ;
- every entry of satisfies .
Then the conjunction of the following two claims holds.
(A) Existence of a terminal descendant. There exists a board that is reachable from by a finite (possibly empty) chain of moves and is terminal, i.e. admits no move: contains no two entries (with multiplicity) both greater than .
(B) A single value serving every terminal descendant. There exists a natural number such that and such that, for every board , if is reachable from and is terminal, then
i.e. the sub-multiset of entries of that exceed is exactly the one-element multiset — exactly one entry of is greater than (multiplicity one, so no repetition of above ), and that entry equals ; all other entries of are or .
Which part is existence and which is uniqueness-style, and where the quantifiers sit. Claim (A) is a pure existence claim: . In claim (B) the existential comes first, and the universal is nested inside it: the order is
So is chosen once, before is considered, and is therefore not allowed to depend on the terminal board ; it may depend only on (and on the hypotheses about ). The existence half of (B) is ", "; the uniqueness-style half is the inner universal statement, which says that all reachable terminal boards have the same big part, and that this common big part is a singleton. Had the quantifiers been ordered the other way — — the claim would only be that each reachable terminal board has exactly one entry above , with different terminal boards permitted to carry different such values. The order as written rules that out: one value must work for all of them. Note also that is introduced with , not ; no uniqueness of itself is written down, though claim (A) guarantees at least one reachable terminal board exists, so the inner universal is not vacuous.
Use of the cardinality hypothesis. The number appears only in the hypothesis . It occurs nowhere in the conclusion: neither (A) nor (B) mentions , , or any numeral. The hypothesis therefore restricts which boards the statement speaks about, but the asserted conclusion is word-for-word the same sentence about as it would be for a board of any other size; the statement conveys no information about how the conclusion depends on , and in particular does not assert that is necessary, sufficient, or special.
Conditionality. The statement is conditional on the two hypotheses about the starting board ; it is not conditional on a move existing from , and is not assumed reachable from anything. Inside (B), the claim about a board is conditional on being reachable from and terminal; for any failing either condition, that implication is vacuously true and (B) says nothing about such a — in particular nothing about reachable boards that are not terminal, and nothing about terminal boards not reachable from .
Degenerate cases. The hypotheses exclude the empty board () and any board containing a or a (every entry must exceed ), so the empty board and the all-s board fall outside the statement entirely. The two hypotheses are jointly satisfiable — for instance consisting of copies of — so the statement is not vacuous. A board satisfying both hypotheses has at least two entries greater than , so the defining condition of a move is met and such an is never itself terminal; the reflexive case of (B) therefore does not arise under these hypotheses, and no board for which "already terminal" and the hypotheses hold simultaneously exists. Boards of entries containing a or a are excluded by the second hypothesis; boards of entries all greater than but of a size other than are excluded by the first. Nothing is claimed about any excluded board.
Not asserted. No formula, construction, or characterization of is given — not in terms of the entries of , their gcd, their lcm, their product, or anything else; only is stated about it. No claim that is an entry of , or divides or is divisible by anything. No claim about the non-big part of the reachable terminal boards: the number of s, the presence or absence of s, and are all unconstrained by (B), so (B) does not assert that reachable terminal boards are equal — only that their entries above coincide. No uniqueness of the terminal board in (A), no bound on the number of moves needed, no claim that every sequence of moves terminates, and no claim of confluence beyond what the shared value states. No claim that is unique as an , no claim about boards reachable from that are not terminal, and no claim about what happens for starting boards violating either hypothesis.