Glossary

Defined in this project

Every definition in this project, under its own name: the first paragraph of its description, or how it is declared when it has none. Theorems are not listed here: they are results, not words.

A · B · C · D · E · F · G · H · I · J · K · L · M · N · O · P · Q · R · S · T · U · V · W · X · Y · Z · Other

A

A def

def A (m : ℕ) (hm : 0 < m) : ℕ → ℤ · Canada1998P5.A

A def

def A : ℕ · Imo1975P4.A

A abbrev

abbrev A : Fin 8 · Imo1979P6.A

A def

def A (i : Fin n) : Finset ℕ · Imo1989P1.A

A def

def A · Imo1989P6.A

A def

def A (n : ℕ) [NeZero n] : Prop · Imo1993P6.A

A def

All incidences of agreement. · Imo1998P2.A

a def

def a (href : String) (attrs : List Attr · Html.a

a def

def a (n : ℕ) : ℕ · Imo1971P3.a

a def

The lower Wythoff sequence ⌊n·φ⌋, which is the function f in the problem. · Imo1978P3.a

a def

def a (n : ℕ) · Imo1979P6.a

a def

def a (n : ℕ) : ℤ · Imo2005P4.a

a def

def a (x : Finset.Icc 1 2023 → ℝ) (n : Finset.Icc 1 2023) : ℝ · Imo2023P4.a

a def

def a : ℕ → ℕ · Poland1998P4.a

a def

reindexed to start at 0 · Usa1973P2.a

a def

The sequence of the problem, with indices shifted by one so that a n 0 = n: for k ≥ 1, a n k is the unique integer in [0, k] for which k + 1 divides s n k = a n 0 + ... + a n k. · Usa2007P1.a

a def

The number of ways to advance around the circle exactly twice without repeating a move: sequences starting with u = 0 end in v = 1, and sequences starting with w = 2 end in w = 2. · Usa2013P2.a

a' def

def a' (n : ℕ) : ZMod 7 · Poland1998P4.a'

a1 def

First circle when 13 ∤ n. · Usa1990P3.a1

a2 def

First circle when 13 ∣ n. · Usa1990P3.a2

a_avg def

a_avg x n is the average of the terms x 0, x 1, ..., x n. · Usa1993P5.a_avg

A_equiv_B def

def A_equiv_B [NeZero n] : Equiv (A n) (B n) · Imo1989P6.A_equiv_B

aa def

def aa (m : ℕ) (x : Finset.Icc 1 (2 * m + 1) → ℝ) (n : Finset.Icc 1 (2 * m + 1)) : ℝ · Imo2023P4.aa

aang def

The angle a(X) from the problem statement: the measure in radians, counterclockwise from OA, of the angle between OA and OX, taking values in [0, 2 * π). (The problem only uses this for X ≠ O; we define it for all X.) · Imo1984P3.aang

ABC def

def ABC : Affine.Triangle ℝ (EuclideanSpace ℝ (Fin 2)) · Imo2001P1.Imo2001q1Cfg.ABC

ABC def

def ABC : Affine.Triangle ℝ (EuclideanSpace ℝ (Fin 2)) · Imo2014P4.Imo2014q4Cfg.ABC

ABC def

def ABC : Affine.Triangle ℝ Pt · Imo2023P2.Imo2023q2Cfg.ABC

ACanWin def

A can win the game with parameter k in finitely many moves. · Usa2014P4.ACanWin

aceSets def

The sample space: the 3-element subsets of the positions {1, ..., n}; each such subset records the positions of the three aces in the pack. · Usa1975P5.aceSets

aChoice def

We define $a_{choice}(b) := 4*(2+b)^4$, so that we can take $m = 2+b$ in polynomial_not_prime. · Imo1969P1.aChoice

AcuteSet def

The predicate from the problem statement: the 3-element subset w of indices spans an acute-angled triangle. · Imo1970P6.AcuteSet

add def

Addition of two forms of the same degree. · Imo2017P6.HForm.add

addColoring def

def addColoring (f g : coloring) : coloring · Usa1998P4.addColoring

Adj def

Two cells are adjacent if their squares share a vertex (Chebyshev distance at most 1). · Usa2004P4.Adj

Adj def

Two lattice points are adjacent when their (Manhattan) distance is 1. · Usa2008P3.Adj

Adj def

Two cells are adjacent when their difference is one of the six unit steps. · Usa2014P4.Adj

Adjacent def

Definition of adjacency: Two squares are adjacent if they share a common side. · Imo1999P3.Adjacent

Adjacent def

Whether two cells are adjacent. · Imo2022P6.Adjacent

Adjacent def

Whether two cells are adjacent. · Imo2024P5.Adjacent

adjacent def

def adjacent {n : ℕ} : checkerboard n → checkerboard n → Prop · Usa1999P1.adjacent

AdjDistinct abbrev

Adjacent columns are distinct. · Usa2013P2.AdjDistinct

Admissible def

A configuration is admissible if it can be obtained from the initial configuration by a finite number of operations. Since the operations commute and are involutions, every sequence of operations is described by a Moves. · Usa2013P3.Admissible

AdmissibleMark def

The set of admissible markings for a player: a finite subset of (0,1) of size at most n. We encode it as a Finset ℝ subject to the side conditions. · Imo2026P3.AdmissibleMark

aE def

the "a" side representative: if the negative loop (-k,-k) appears, we take -k as the representative (making all loops "positive"); otherwise k. · Usa2010P6.aE

AffSubOfPlane abbrev

Affine subspaces of the plane (i.e. ∅, point, line, plane) · Imo2025P1.AffSubOfPlane

AForce inductive

AForce k s means that from the board s, with A to move, A can force a win in finitely many moves regardless of how B plays. Since the witness is an inductive tree covering all of B's responses, every play following the strategy … · Usa2014P4.AForce

Agree abbrev

The proposition that the judges in an ordered pair agree about a contestant's rating. · Imo1998P2.JudgePair.Agree

agreedContestants def

The set of contestants on which two judges agree. · Imo1998P2.agreedContestants

AgreedTriple abbrev

A triple consisting of contestant together with an ordered pair of judges. · Imo1998P2.AgreedTriple

ainvCount def

The number of A-inversions of the permutation σ. · Usa2017P2.ainvCount

aliceAns def

The t-th answer of A's counterplay. · Imo2012P3.aliceAns

aliceHist def

The answer history of A's counterplay after t steps. · Imo2012P3.aliceHist

alicePlay def

A's counterplay against σ: after each answer she records, for every candidate, the length of its current run of consecutive lies. Given a question, she chooses the side with smaller total weight as the "bad set" and answers that x lies … · Imo2012P3.alicePlay

aliceStreak def

The streak (length of the current run of consecutive lies) of each candidate after t answers of A's counterplay. · Imo2012P3.aliceStreak

aliceWeight def

The total weight after t answers. · Imo2012P3.aliceWeight

AliceWins def

Alice wins a finished board: there is a chain of black cells, consecutive cells sharing a vertex, from the top row to the bottom row. · Usa2004P4.AliceWins

all_black_k def

def all_black_k : Finset (Point n) · Imo2025P6.all_black_k

all_colorings_are_good abbrev

abbrev all_colorings_are_good (m : ℕ) : Prop · Bulgaria1998P1.all_colorings_are_good

all_one_or_two abbrev

abbrev all_one_or_two (l : List ℕ) : Prop · ZerosOnesAndTwos.all_one_or_two

all_prefixes def

def all_prefixes (p : List α → Prop) (a : Stream' α) : Prop · KolmogorovStreams.all_prefixes

all_same_class def

def all_same_class (is_decent : List α → Prop) (b : Stream' (List α)) : Prop · KolmogorovStreams.all_same_class

all_same_color def

def all_same_color (f : coloring) : Prop · Usa1998P4.all_same_color

AllCutsDistinct def

The property from the problem statement: no matter how the necklace is cut into m blocks of n consecutive beads (the cut is determined by the starting position s of the first block), the numbers of red beads in the m blocks are … · Usa2024P4.AllCutsDistinct

allImoUrls def

def allImoUrls (year : Nat) (idx : Nat) : List WriteupLink · allImoUrls

AllRightOf def

The property of lam in the problem: starting from any initial configuration in which the fleas are not all at the same point, for every point M on the line there is a finite sequence of moves taking all the fleas strictly to the right … · Imo2000P3.AllRightOf

allUsamoUrls def

def allUsamoUrls (year : Nat) (idx : Nat) : List WriteupLink · allUsamoUrls

alternateSum def

def List.alternateSum {α : Type u} [Add α] [Zero α] (l : List α) (head : Bool) : α · Imo2022P1.List.alternateSum

Alternating abbrev

abbrev Alternating (n : Nat) : Prop · Imo2004P6.Alternating

altFormula def

The key to solving this problem simply is that we can rewrite the equation as a product of terms, shown in `alt_formula`, being equal to zero. · Imo1962P4.altFormula

AltPath structure

An alternating path in S: a list of at least two distinct points of S such that the step from position i to position i + 1 is horizontal (the two points agree on their second coordinate) when i is even and vertical (the two … · Imo1986P6.AltPath

altSeq def

The alternating sequence 0, 1, 0, 1, .... · Usa1987P5.altSeq

altSum def

The alternating sum ∑_{U ⊆ s} (-1)^{|U|} (m - σ(U)).choose k, viewed as an integer. · Usa1994P5.altSum

AMove def

A legal move of player A: from the number n just chosen by B (or the initial number n₀), A may choose any m with n ≤ m ≤ n ^ 2 (A wins by choosing 1990). · Imo1990P5.AMove

AMove def

A move of player A: place counters on two empty adjacent cells. · Usa2014P4.AMove

AmyEnsures def

Amy can ensure that she places at least K stones. (400 rounds of fuel exceeds any possible length of play, since every round occupies two new sites of the 400.) · Imo2018P4.AmyEnsures

amyMoves def

The sites on which Amy may place a stone: the unoccupied sites at distance different from √5 from every red stone. · Imo2018P4.amyMoves

ang def

The angle of the j-th vertex of a regular 4027-gon. · Imo2013P2.ang

answers def

The number of answers given so far in the current round. · Imo2012P3.BobPhase.answers

antipascal_triangle structure

antipascal triangle with n rows · Imo2018P3.antipascal_triangle

antipode def

def Sphere.antipode (s : Sphere Pt) (p : Pt) : Pt · Imo2023P2.Sphere.antipode

aopsImoUrl def

def aopsImoUrl (year : Nat) (idx : Nat) : String · aopsImoUrl

aopsUsamoUrl def

def aopsUsamoUrl (year : Nat) (idx : Nat) : String · aopsUsamoUrl

apCount def

The number of three-term arithmetic progressions among the first n terms of a, counted by their middle index. · Usa1980P2.apCount

apeb def

The lighter pebble of pair k. · Imo2020P3.apeb

apPairs def

For a sequence a : ℕ → ℝ and an index j, the finset of pairs (i, k) with i < j < k < n such that a i, a j, a k forms a three-term arithmetic progression. Every three-term arithmetic progression with indices below n corresponds … · Usa1980P2.apPairs

append def

Append two closed trails that both start at the same vertex v. · Imo2020P3.CTrail.append

appendToLast def

def appendToLast {n : ℕ} (b : Fin (n + 1) → List ℝ) (extra : List ℝ) : Fin (n + 1) → List ℝ · Imo2026P3.appendToLast

appleTouchIconPng def

def appleTouchIconPng : Asset · Assets.appleTouchIconPng

apply def

Evaluate a trigonometric map at a real number. · Usa1995P2.TrigMap.apply

applyMoves def

The configuration reached from the initial (all-white) configuration by performing the moves v: token (a, b) ends up black iff an odd number of the three lines through it were flipped. · Usa2013P3.applyMoves

apPoly def

The polynomial P(x) = ∏_{i=1}^{k} (x + i·d) attached to an arithmetic progression with common difference d. · Imo2023P3.apPoly

Aquaesulian def

def Aquaesulian (f : ℚ → ℚ) : Prop · Imo2024P6.Aquaesulian

Aquaesulian def

The condition on functions in the problem (for a general AddCommGroup and in symmetric form). · Imo2024P6.General.Aquaesulian

arcDist def

The arc distance between two of the 432 points: the number of unit arcs in the shorter of the two arcs joining them. The chord through x and y has length 2R sin(π·d/432) with d = arcDist x y, which is strictly increasing in `d ∈ … · Usa2012P2.arcDist

arcOf def

The i-th arc as a finset. · Usa2025P6.CirclePartition.arcOf

arcSet def

An arc of length l starting at c on the circle ZMod m. · Usa2025P6.arcSet

arith_mean def

def arith_mean (ms : Multiset ℕ) : ℚ · Imo1981P2.arith_mean

Arrangement abbrev

An arrangement of the 2n cards: the label shown at each position. · Usa2016P6.Arrangement

Asleep def

Each professor p : Fin 5 takes two naps, and nap k : Fin 2 of professor p is the closed interval [s p k, e p k]. Professor p is asleep at time t if t belongs to one of these two nap intervals. · Usa1986P2.Asleep

assembleSelectedBlocks def

def assembleSelectedBlocks (p : List ℝ) (I : Finset (Fin p.length)) (b : Fin (selectedList p I).length → List ℝ) : Fin p.length → List ℝ · Imo2026P3.assembleSelectedBlocks

assembleTwoSelectedBlocks def

def assembleTwoSelectedBlocks (p : List ℝ) (I J : Finset (Fin p.length)) (bI : Fin (selectedList p I).length → List ℝ) (bJ : Fin (selectedList p J).length → List ℝ) : Fin p.length → List ℝ · Imo2026P3.assembleTwoSelectedBlocks

Asset inductive

A static asset to be copied · Asset

assocB def

The association map from red lines to blue points, for a choice of witnesses. · Imo2014P6.assocB

Attr abbrev

A single HTML attribute · Attr

auxColor def

The extremal coloring on 32 edges (Wöginger's construction): vertices 0,…,3 form the red square, 4,…,7 the blue square, and 8 is the apex. The diagonals of the two squares are the four uncolored edges. · Imo1992P3.auxColor

auxColoring def

The extremal coloring, packaged as an EdgeColoring. · Imo1992P3.auxColoring

auxPoly def

The polynomial 1 + X^k + (-1 - X)^k over ℝ. It arises from substituting x = 1, y = t, z = -1 - t into x^k + y^k + z^k (note 1 + t + (-1 - t) = 0). · Usa1982P2.auxPoly

avail def

The set of blue points that have not been used yet. · Usa2017P4.avail

AWins inductive

AWins n: it is A's turn and the current number is n (the initial position has n = n₀), and A has a winning strategy. A either wins immediately by choosing 1990 (a legal move from n), or chooses a legal move m from which B cannot … · Imo1990P5.AWins

A₂ def

A₂ is the second point of intersection of the ray AA₁ with the circumcircle of ABC. · Imo2019P2.Imo2019q2Cfg.A₂

B

B def

def B : ℕ · Imo1975P4.B

B def

def B · Imo1989P6.B

B def

def B (n : ℕ) [NeZero n] : Prop · Imo1993P6.B

B def

The elements i outside X c such that X c ∪ {i} is blue. · Usa2015P3.B

b def

def b (attrs : List Attr · Html.b

b def

def b (n : ℕ) · Imo1979P6.b

b def

The blue point associated to ℓ: the next vertex of the region after r in clockwise order. · Imo2014P6.Witness.b

b def

def b : ℕ → ℕ · Usa1973P2.b

b def

b n: the smallest number of blocks one can tear out of an n×n sheet of stamps (tearing out whole blocks of three adjacent stamps in a single row or column) making it impossible to tear out any more blocks. · Usa2002P6.b

b def

The average b n k = (a n 0 + ... + a n k) / (k + 1), a nonnegative integer. · Usa2007P1.b

b0 def

The number of blue points on the axis y = 0 in a list. · Usa2008P3.b0

b1a def

Second circle when 13 ∤ n and n ≢ 2 [MOD 17]. · Usa1990P3.b1a

b1b def

Second circle when 13 ∤ n and n ≡ 2 [MOD 17]. · Usa1990P3.b1b

b2a def

Second circle when 13 ∣ n and n ≢ 16 [MOD 17]. · Usa1990P3.b2a

b2b def

Second circle when 13 ∣ n and n ≡ 16 [MOD 17]. · Usa1990P3.b2b

b_avg def

b_avg x n is the average of the terms x 1, x 2, ..., x n. · Usa1993P5.b_avg

b_seq def

The b_n sequence defined in terms of the a sequence · Imo1970P3.b_seq

b_st_coords def

def b_st_coords (s t : Int) : Int × Int · Imo2025P6.b_st_coords

Bad def

The triple of points X, Y, Z has an angle of at least π / 2 (at X, at Y, or at Z respectively). · Imo1970P6.Bad

badPair def

The "bad" vertices for a pair p: the remaining vertices that are joined to exactly one of the two endpoints of p. · Usa1985P4.badPair

badSet def

The elements of {1, ..., 280} divisible by 2, 3, 5 or 7. Among any five of them, two share a common prime factor. · Imo1991P3.badSet

Balance def

The imbalance (left pan minus right pan) after a sequence of placements. A pair (i, b) denotes one placement of the weight 2^i; the boolean is true if the weight is placed on the left pan and false if it is placed on the right pan. · Imo2011P4.Balance

Balanced def

A signing of a set of points of the plane: ε p = 1 means that p is colored white and ε p = -1 means that p is colored red. The difference between the numbers of white and red points of S lying on a line then equals the sum of … · Imo1986P6.Balanced

Balanced def

A finite set of cells is balanced under the coloring f if each of the three letters occurs on exactly one third of its cells. · Imo2016P2.Balanced

base def

def base (title : String) (config : SConfig) (currentPage : NavbarState) (includeHljs : Bool · base

base def

A distinguished point on the line: the foot of the perpendicular from the origin. · Imo2014P6.Line.base

base_two_to_base_three def

def base_two_to_base_three (n : ℕ) · Imo1983P5.base_two_to_base_three

baseMonsterData def

An arbitrary choice of monster positions, which is modified to put selected monsters in desired places. · Imo2024P5.baseMonsterData

BaseSetup structure

structure BaseSetup (n : ℕ) [NeZero n] · Imo2025P6.BaseSetup

bazzaStrategy def

Bazza's greedy strategy: spend the entire quadratic budget. · Imo2025P5.bazzaStrategy

BddCond def

The condition that the sequence p(f(n²)) − 2n is bounded above (and defined for every n). · Usa2006P3.BddCond

Beam inductive

A beam in an n × n × n cube, given by its orientation and the two coordinates of its cross-section: * xBeam j k occupies y = j, z = k and spans the x-direction; * yBeam i k occupies x = i, z = k and spans the y-direction; … · Usa2020P2.Beam

BenInv def

Ben's invariant: every 4-cycle contains at most one red stone, and the blue stones are exactly the opposite sites of the red stones. · Imo2018P4.BenInv

benMoves def

The sites on which Ben may place a stone: all unoccupied sites. · Imo2018P4.benMoves

Big def

Big numbers are those greater than l (thus, appear at most k times). · Imo2024P3.Condition.Big

BigBound def

BigBound m c x ss holds when every jump of ss (performed starting from position x) that ends at a position greater than c has length at most 2 ^ m. · Usa2006P5.BigBound

bigUnion def

The union of the six pairwise coprime families, all inside {1, ..., 280}. · Imo1991P3.bigUnion

BinaryPalindrome def

Binary palindromes. · Imo1988P3.BinaryPalindrome

binaryReverse def

Reverse the base-two digits, dropping leading zeroes. · Imo1988P3.binaryReverse

bisectLengths def

def bisectLengths (l : List ℝ) : List ℝ · Imo2026P3.bisectLengths

bitQuestion def

The set of candidates whose i-th bit is 1. · Imo2012P3.bitQuestion

Blackboard abbrev

abbrev Blackboard (n : ℕ) · Usa2023P4.Blackboard

blackCount def

The number of black squares of a rectangle. · Imo1974P4.Rect.blackCount

blackPairs def

The number (mod 2) of adjacent pairs of holes that are both black. · Imo2021P5.blackPairs

blackPerm def

def blackPerm [NeZero n] : Fin n → Fin n · Imo2025P6.blackPerm

BlackPointProps structure

structure BlackPointProps (s t : Int) (p : Point n) : Prop · Imo2025P6.BlackPointProps

blacks def

The black squares of the checkerboard coloring. · Imo2018P4.blacks

blockCount def

The number of red beads in the block of n consecutive beads starting at position s + i * n (positions are taken modulo m * n). · Usa2024P4.blockCount

blockIndex def

def List.blockIndex {α : Type u} [DecidableEq α] (l : List α) (k : Fin l.length) · Imo2022P1.List.blockIndex

blockIndices def

def blockIndices (f : ℕ → ℕ) (N : ℕ) : List ℕ · Imo2026P3.blockIndices

blockMatrix def

def blockMatrix {n : ℕ} (A B C D : Fin n → Fin n → ℕ) : Fin (n + n) → Fin (n + n) → ℕ · Imo1997P4.blockMatrix

blocks def

def List.blocks {α : Type u} [DecidableEq α] : List α → List ℕ · Imo2022P1.List.blocks

blocks def

def Row.blocks {n : ℕ} (c : Row n) : List ℕ · Imo2022P1.Row.blocks

blue def

The blue predicate. · Usa2008P3.blue

blueCard def

blueCard c T is the number of subsets of T that are colored blue by c; this is the function f of the problem statement. · Usa2015P3.blueCard

blueCol def

The blue points in column x. · Imo2002P1.blueCol

bluePts def

The blue points: vertices with even indices. · Imo2013P2.bluePts

bluePts def

The blue points: the intersection points of pairs of distinct blue lines. · Imo2014P6.bluePts

BMove def

A legal move of player B: from the number m just chosen by A, B may choose any m' such that m / m' is a prime power p ^ r with r ≥ 1 (B wins by choosing 1). · Imo1990P5.BMove

BMove def

A move of player B: remove one counter from the board. · Usa2014P4.BMove

Bnd def

A constant dominating all values and all consecutive differences of xe. · Usa2022P5.Bnd

Board abbrev

A board is a finite multiset of natural numbers. The full board discipline (entries ≥ 1, cardinality 2026) is captured by the predicate IsInitial. · Imo2026P1.Board

Board abbrev

The board: square i contains b i for i < 2000; anything outside is irrelevant. · Usa1999P5.Board

Board abbrev

A board state: the set of cells that currently hold a stone. · Usa2021P3.Board

board def

The 8 × 8 chessboard. · Imo1974P4.board

BobCanForceEnd inductive

inductive BobCanForceEnd (a : ℕ+) (n : ℕ) : State n → Prop · Usa2023P4.BobCanForceEnd

bobCell2 def

The cell Bob plays in when Alice plays in rows 3 to 6: some empty cell of rows 3 to 6 (one always exists at that point by a parity argument, see inv_prefBoard). · Usa2004P4.bobCell2

bobEmbedding def

An embedding of the 2 ^ k bit patterns into the pool. · Imo2012P3.bobEmbedding

bobFreshValue def

A rational number not appearing on the board. · Usa2004P4.bobFreshValue

bobMateValue def

The number Bob writes in the mate of Alice's cell when he answers in the first two rows. · Usa2004P4.bobMateValue

bobMove def

Bob's strategy: if Alice just played in the first two rows, answer in the mate of her cell with a number preserving the order-isomorphism; otherwise play in any empty cell of rows 3 to 6 with a fresh number. · Usa2004P4.bobMove

BobPhase inductive

Bob's phase within the current elimination round: either probing with the singleton question (j consecutive "no" answers so far), or asking the bit questions after a "yes" (the probe phase took j answers, and bs are the bit answers … · Imo2012P3.BobPhase

bobQuestion def

Bob's question in a given phase: the singleton {special} when probing, the |bs|-th bit question in the bit phase. · Imo2012P3.bobQuestion

bobSpecial def

The distinguished candidate asked about in the probe phase: an element of the pool outside the image of the bit patterns. · Imo2012P3.bobSpecial

BobState structure

Bob's state: his current candidate pool together with the progress in the current elimination round. · Imo2012P3.BobState

bobStateOf def

Bob's state after processing the first t answers. · Imo2012P3.bobStateOf

bobStep def

One step of Bob's state machine. If the pool is already small enough, the state is frozen. · Imo2012P3.bobStep

bobStepPhase def

One round-step of Bob's state machine, in the case 2 ^ k < P.card. · Imo2012P3.bobStepPhase

bobStrategy def

Bob's winning strategy for part (a). · Imo2012P3.bobStrategy

BobWins def

Player B can guarantee a win with parameters k, n when player A's bound is N. · Imo2012P3.BobWins

body def

def body (attrs : List Attr · Html.body

BOK def

Well-formed board: nothing written outside the 2000 squares. · Usa1999P5.BOK

Bonza def

def Bonza (f : ℕ+ → ℕ+) : Prop · Bonza

boundaryNeighbors def

def boundaryNeighbors {n : ℕ} (c : Finset (checkerboard n)) (x : c) : Finset (checkerboard n) · Usa1999P1.boundaryNeighbors

boundaryPoints def

def boundaryPoints (S : Finset ℝ) : List ℝ · Imo2026P3.boundaryPoints

Bounded abbrev

abbrev Bounded (x : ℕ → ℝ) : Prop · Imo1991P6.Bounded

bpeb def

The heavier pebble of pair k. · Imo2020P3.bpeb

br def

def br · Html.br

break_into_words def

def break_into_words : (Stream' ℕ) → -- word lengths (Stream' α) → -- original sequence (Stream' (List α)) -- sequence of words · KolmogorovStreams.break_into_words

bResponses def

The legal responses available to B after A chooses m. Keeping only divisors whose complementary factor is a prime power avoids reasoning about impossible moves. · Imo1990P5.bResponses

bSeq def

bSeq p n is the number obtained by writing n in base p - 1 and reading the result in base p. · Usa1995P1.bSeq

bT def

The parameter of the blue point b in the parametrization of g₁: the other endpoint of the g₁-edge. · Imo2014P6.Witness.bT

build def

The sequence of length n + 1 with first term c whose successive differences are given by x. · Usa1996P4.build

build def

Runs the extraction algorithm for at most fuel steps, returning the list of extracted digits if the pair (0, 0) is reached in time. · Usa1997P3.build

build def

def build : ℕ → solution_set · Usa2017P1.build

buildAux def

Auxiliary for build: the k-th term of the sequence with first term c and successive differences given by x. · Usa1996P4.buildAux

buildSite def

Build the entire site · buildSite

bv def

The contribution of one direction to the weight of v ^^ sp ε: the number of flipped lines of that direction, as a function of the "full flip" bit δ and the "theta flip" bit τ. · Usa2013P3.bv

BWins inductive

BWins m: it is B's turn and the current number is m, and B has a winning strategy. B either wins immediately by choosing 1, or chooses a legal move m' ≠ 1 from which A cannot win (A wins by choosing 1990) and such that every legal … · Imo1990P5.BWins

BWinsStart def

BWinsStart n: B has a winning strategy from the initial position with n₀ = n (it is A's turn): whatever legal first move m A makes, it is not 1990 and B wins from m. · Imo1990P5.BWinsStart

B₂ def

B₂ is the second point of intersection of the ray BB₁ with the circumcircle of ABC. · Imo2019P2.Imo2019q2Cfg.B₂

C

C abbrev

abbrev C : Fin 8 · Imo1979P6.C

C def

def C (n : ℕ) [NeZero n] : Prop · Imo1993P6.C

c abbrev

The first index i (0-based) such that n ≤ a i. This exists because a is unbounded. The problem's bₙ is c a hu n + 1 (the 1-based index). · Usa1985P5.c

C' def

The reflection of C in line AB. · Imo2012P5.Imo2012P5Cfg.C'

C_G_symm def

def C_G_symm (n : ℕ) : {w : Octagon.Walk C E // isTerminalWalk w ∧ w.length = n} ≃ {w : Octagon.Walk G E // isTerminalWalk w ∧ w.length = n} · Imo1979P6.C_G_symm

c_seq def

Helper: c_k = √(a_k) · Imo1970P3.c_seq

calc_s def

def calc_s (p : Point n) : Int · Imo2025P6.calc_s

calc_t def

def calc_t (p : Point n) : Int · Imo2025P6.calc_t

CanAdd structure

A new friendship may be formed between u and v: they are distinct, not yet friends, and have at least two common friends. · Usa2022P6.CanAdd

cands def

Candidate "first moments" for a set A of professors: nap-start times of members of A at which every member of A is asleep. · Usa1986P2.cands

cands def

The candidate move sequences used to reach a configuration with exactly one odd entry. Which one applies depends on the parity pattern of the starting configuration. · Usa2003P6.cands

CanEnsure inductive

With fuel rounds left to play, Amy can ensure from the position (red, blue) (with Amy to move) that she places at least K stones in total. (An inductive predicate so that definitions and proofs do not have to unfold a recursion on … · Imo2018P4.CanEnsure

canon def

Canonical orientation of a nonzero lattice point: exactly one of s, -s satisfies canon s. · Imo2017P6.canon

canonicalHighCount def

Canonical high-rank counts used by the construction. · Usa2024P2.canonicalHighCount

canonicalPlay def

The canonical play: all blue cards, then all red cards, then all white cards. Every play with the same card counts is a permutation of this one. · Usa2000P3.canonicalPlay

cap def

The capacity bound: any collection of total value at most cap k can be split into k or fewer groups each of value at most 1. · Imo2014P5.cap

Car structure

A cable car's starting and finishing points. · Imo2020P4.Car

Card inductive

The three colors of cards. · Usa2000P3.Card

cast def

Reindexing a circular partition along an equality of the number of arcs. · Usa2025P6.CirclePartition.cast

cat def

Concatenation of two lamp vectors. · Imo1993P6.cat

cdist def

The cyclic (counterclockwise) distance from a to b; it is 0 iff a = b. · Usa2017P4.cdist

Cell def

The cell of a sign vector σ: the set of points lying on the prescribed side of every line of L. The nonempty cells are exactly the regions into which the lines of L cut the plane, and the bounded nonempty cells are its finite … · Imo2014P6.Cell

Cell abbrev

A cell of the board. · Imo2022P6.Cell

Cell abbrev

A cell on the board for the game. · Imo2024P5.Cell

Cell abbrev

A cell of the 6×6 grid: (row, column), both in Fin 6. Row 0 is the top row of the grid and row 5 the bottom row. · Usa2004P4.Cell

Cell abbrev

A cell of the hexagonal grid, given in axial coordinates. · Usa2014P4.Cell

Cell abbrev

The grid cells indexing the sets Sᵢⱼ. · Usa2019P4.Cell

Cell abbrev

abbrev Cell (N : ℕ) · Usa2022P1.Cell

cellDegree def

The degree of a cell: the number of cells adjacent to it. · Imo2022P6.cellDegree

cellOrder def

The linear order on cells induced by the key function. · Imo2022P6.cellOrder

cells def

The unit squares making up a rectangle. · Imo1974P4.Rect.cells

cellValue def

Extend a coloring by zero outside the board. · Usa1998P4.cellValue

centerCells def

def centerCells (k : ℕ) : Finset (Fin (3 * k) × Fin (3 * k)) · Imo2016P2.centerCells

cfun def

The coefficient function assigning x to p, y to q, and 1 to everything else. · Usa2012P3.cfun

chain def

The greedy "always go to the larger child" path starting at the apex. · Imo2018P3.chain

chainInv def

The chain arctan, sin, arccos, tan of trigonometric maps. We show in run_chainInv that it sends any positive x to 1 / x. · Usa1995P2.chainInv

chainLeft def

def List.chainLeft {α : Type u} [DecidableEq α] (l : List α) (k : Fin l.length) : Fin l.length · Imo2022P1.List.chainLeft

chainLeft def

The first coin in the chain containing coin k (zero-based). · Imo2022P1.Row.chainLeft

chainRight def

def List.chainRight {α : Type u} [DecidableEq α] (l : List α) (k : Fin l.length) : Fin l.length · Imo2022P1.List.chainRight

chainRight def

The last coin in the chain containing coin k (zero-based). · Imo2022P1.Row.chainRight

chainSqrt def

The chain arctan, cos, arctan, sin, arccos, tan of trigonometric maps. We show in run_chainSqrt that it sends any real x to √(1 + x²). · Usa1995P2.chainSqrt

check9 def

def check9 (f : Fin 9 → Fin 2) : Bool · Bulgaria1998P1.check9

checkerboard def

def checkerboard (n : ℕ) · Usa1999P1.checkerboard

checkerGraph def

def checkerGraph {n : ℕ} (c : Finset (checkerboard n)) : SimpleGraph c · Usa1999P1.checkerGraph

chenImoUrl def

def chenImoUrl (year : Nat) (_idx : Nat) : String · chenImoUrl

chenUsamoUrl def

def chenUsamoUrl (year : Nat) (_idx : Nat) : String · chenUsamoUrl

chessboard def

def chessboard : Type · Usa1998P4.chessboard

chi def

The additive character ZMod p → ℂ given by j ↦ ζ ^ j.val. · Usa1999P3.chi

chi def

The colour of a point as ±1 (+1 for blue, -1 for red). · Usa2008P3.chi

children def

The children of v: cells of D whose parent is v. · Usa2007P4.children

ChinesePair structure

structure ChinesePair · Imo1989P5.ChinesePair

ChoiceCount def

The sets of n blue points in T whose coordinates are distinct in the dimension selected by coord. · Imo2002P1.ChoiceCount

Circle abbrev

abbrev Circle · Usa2000P5.Circle

circleCenter abbrev

abbrev circleCenter (ω : Fin 7 → Circle) (i : Fin 7) : Point · Usa2000P5.circleCenter

CircleEmb structure

A circular embedding: an enumeration of the complement of D that respects the successor structure of the circle. · Usa2025P6.CirclePartition.CircleEmb

CirclePartition structure

A partition of the circle ZMod m into k consecutive nonempty arcs, described by a basepoint and the list of arc lengths. · Usa2025P6.CirclePartition

Classification def

The classification: f is a nonzero constant times a (possibly empty) product of factors 4X − a² with a an odd integer. · Usa2006P3.Classification

clearCoeff def

The (integer) coefficients of denomProd q N • q. · Usa1995P4.clearCoeff

clearPoly def

The integer polynomial obtained from q : ℚ[X] by clearing denominators: its coefficients are clearCoeff q N, so it agrees with denomProd q N • q on all evaluations. · Usa1995P4.clearPoly

clip def

def clip (n : ℕ) : Fin 99 · Usa1998P4.clip

clipped_rect def

def clipped_rect [NeZero k] (hk : 2 ≤ k) (s t : Int) : Option (Matilda (k * k) (all_black_k k)) · Imo2025P6.clipped_rect

clippedEmbedding def

def clippedEmbedding {N M : ℕ} (e : Fin (N + 1) ↪o Fin (M + 1)) (j : ℕ) : ℕ · Imo2026P3.clippedEmbedding

cls def

def cls (c : String) : Attr · Html.cls

cmax def

The maximum entry of a configuration. · Usa2003P6.cmax

cmul def

Scalar multiplication of a form by an integer. · Imo2017P6.HForm.cmul

cnt def

The number of entries of a having residue x modulo 3. · Usa1979P3.cnt

cntP def

The number of entries satisfying p. · Usa2017P2.cntP

code def

def code (attrs : List Attr · Html.code

codexDenom def

def codexDenom (n : ℕ) : ℝ · Imo2026P3.codexDenom

codexDyadicWeights def

def codexDyadicWeights (n : ℕ) : List ℝ · Imo2026P3.codexDyadicWeights

codexLowerCuts def

def codexLowerCuts (n : ℕ) : Finset ℝ · Imo2026P3.codexLowerCuts

coef def

The choice of integer coefficients: take the differences bᵢ - b'ᵢ, flipping the sign wherever x i < 0. · Imo1987P3.coef

coeFunctionInt2Real def

def coeFunctionInt2Real {α : Type*} (f : α → ℤ) : (α → ℝ) · Imo1977P2.coeFunctionInt2Real

Coin inductive

The two types of coins. · Imo2022P1.Coin

col def

def col {n : ℕ} (i : Fin n) : Finset (Fin n × Fin n) · Imo1997P4.col

col def

The cells of column k. · Imo2016P2.col

col_valid def

def col_valid {n : ℕ} (hn : 0 < n) (a : Fin n → Fin n → Fin (n ^ 2)) (ha : a.Injective2) : Prop · Usa2023P5.col_valid

colFiber def

The squares of S lying in column c. · Usa2000P4.colFiber

collectProblemMeta def

def collectProblemMeta (env : Lean.Environment) (problems : Lean.NameMap String) (solutions : Lean.NameMap String) (metadatas : Lean.NameMap ProblemExtraction.ProblemFileMetadata) : Lean.Core.CoreM … · collectProblemMeta

colMate def

The pairing of columns: each column is paired with the column three places away. · Usa2004P4.colMate

ColombianConfiguration structure

A configuration of 2013 red points and 2014 blue points in the plane, all distinct, such that no three points of the configuration are collinear. · Imo2013P2.ColombianConfiguration

Color inductive

inductive Color : Type · Imo2002P1.Color

Color inductive

inductive Color : Type · Usa2002P1.Color

colorCount def

def colorCount {n : ℕ} (f : Fin n → Fin n → Letter) (cells : Finset (Fin n × Fin n)) (c : Letter) : ℕ · Imo2016P2.colorCount

colorCount def

def colorCount (color : Cell N → Fin 2) (c : Fin 2) (p : Equiv.Perm (Fin N)) : ℕ · Usa2022P1.colorCount

coloredEdges def

The colored edges of an edge coloring, represented as the set of edges that received a color. (Diagonal "edges" s(i, i) are never colored, so this is exactly the set of colored segments joining two distinct points.) · Imo1992P3.EdgeColoring.coloredEdges

Coloring abbrev

A coloring of the subsets of Fin n; true means blue, false means red. · Usa2015P3.Coloring

coloring def

After j moves, color hole x red iff the walnut in it has number < j; otherwise the hole is black. · Imo2021P5.coloring

coloring def

def coloring · Usa1998P4.coloring

coloring_is_good abbrev

abbrev coloring_is_good {m : ℕ} (color : Set.Icc 1 m → Fin 2) : Prop · Bulgaria1998P1.coloring_is_good

coloring_of_eight def

def coloring_of_eight {n : ℕ} : Set.Icc 1 n → Fin 2 · Bulgaria1998P1.coloring_of_eight

colorOf def

The coloring whose blue sets are exactly the sets T with X₀ ⊆ T ⊆ X₀ ∪ B₀. · Usa2015P3.colorOf

colorsAt abbrev

The set of link types that town v has to other towns. · Usa1981P2.colorsAt

colour def

Colour an edge e = {p, q} of the complete graph on Fin (K + 1) with 0 iff the difference of its endpoints, in one of the two directions, lies in [1, m]. · Imo1988P2.colour

colPart def

The interior cells of column k in rows n - r .. n - 1. · Usa2019P4.colPart

colRect def

def colRect (k : ℕ) : Rectangle · Usa1998P4.colRect

ColSeq abbrev

A sequence of n+1 columns, each column one of the three symbols of Fin 3 (0 = u, 1 = v, 2 = w). · Usa2013P2.ColSeq

colSum def

def colSum (j : Fin n) : ℕ · Imo1971P6.colSum

colZero def

The cells of column 0 in rows ≤ j. · Usa2019P4.colZero

commonAtoms def

def commonAtoms : List ℝ → List ℝ → List ℝ · Imo2026P3.commonAtoms

compAnchor def

def compAnchor (config : SConfig) (text : String) (rel : List String) : Html · compAnchor

Company structure

The cable cars of a company. · Imo2020P4.Company

Completable def

The graph G can be completed so that every user becomes friends with every other user. · Usa2022P6.Completable

complete def

def complete (n : ℕ+) : Prop · Imo1992P6.complete

completeOn def

The complete graph on the finite set S of vertices, seen as a graph on V. · Usa2022P6.completeOn

compRow def

def compRow {idxType subIdxType : Type} [Ord idxType] [Ord subIdxType] (config : SConfig) (contest : Contest idxType subIdxType) (filePath : List String) (mds : Lean.NameMap ProblemMeta) : Html · Contest.compRow

compTable def

def compTable (rows : List <| Html) : Html · compTable

compute_k def

def compute_k (n: ℕ) : ℕ · Imo1978P6.compute_k

Condition def

The conditions on a in the problem. We reindex a to start from 0 rather than 1; N then only has to be nonnegative rather than positive, and the sum in the problem statement is over Ico m n rather than Ioc m n. · Condition

Condition def

The conditions on the problem's coloring C. Although its domain is all of ℕ, we only care about its values in Set.Ico 1 n. · Imo1985P2.Condition

Condition def

The condition of the problem on a placement of numbers round a circle. · Imo2022P3.Condition

Condition def

def Condition (α : ℝ) : Prop · Imo2024P1.Condition

Condition def

The condition of the problem. · Imo2024P2.Condition

Condition def

def Condition (a : ℕ → ℕ) (N : ℕ) : Prop · Imo2024P3.Condition

condition def

def condition (a b : ℕ) : Prop · Usa2017P1.condition

Conditions def

def Conditions (x : Fin 4 → ℝ) : Prop · Usa2014P1.Conditions

Conditions def

def Conditions (x : Fin 4 → ℝ) : Prop · Usa2017P6.Conditions

Conf abbrev

A configuration of six integers at the vertices of a hexagon. · Usa2003P6.Conf

Config structure

structure Config · Config

Config abbrev

A configuration of the sequence, indexed by ZMod 99 (indices are interpreted modulo 99, as in the problem statement). Index i corresponds to the problem's aᵢ₊₁. · Usa1994P2.Config

Config abbrev

A configuration of the game: an integer at each vertex of the pentagon. The vertices are indexed by ZMod 5, so that the neighbors of vertex i are i - 1 and i + 1. · Usa2011P2.Config

conjPerm def

The conjugating permutation: the product of the swaps (σ x, φ x) over the representatives. · Usa2018P6.conjPerm

conn def

In a pseudograph with endpoint functions a b : E → V, the edge e connects v and w. · Imo2020P3.conn

ConnectedP def

Connectivity of a permutation of S: it is a single cycle. · Imo2022P3.ConnectedP

ConsecutiveFactors abbrev

abbrev ConsecutiveFactors (n a b : ℕ) · Imo2023P1.ConsecutiveFactors

ConsistentUpTo def

The play is consistent with the secret x up to time T: among any k + 1 consecutive answers within the first T, at least one is truthful. · Imo2012P3.ConsistentUpTo

const def

The constant form. · Imo2017P6.HForm.const

constAddStart def

def constAddStart (c : ZMod 2) : coloring · Usa1998P4.constAddStart

constr def

The extremal sequence (zero-based): at index 2k the value is (4k+3) / (2 * √(k+1)), and at index 2k+1 it is 2 * √(k+1). · Usa2010P3.constr

constr def

The necklace constructed for the m ≤ n + 1 direction: writing p = q * n + j with j < n, bead p is red iff n + 1 - m ≤ j < n - q. · Usa2024P4.constr

constr_b' def

The flipped choice function: keep b i exactly when the i-th prime divides d. · Usa2021P4.constr_b'

constr_r def

The 2k primes used in the construction: in slot i, the "true" choice is the (2 * i)-th prime and the "false" choice is the (2 * i + 1)-th prime. · Usa2021P4.constr_r

constrEdges def

The edge set of the construction: the edge 0-1 together with, for each i < 1010, the three further edges 1-xᵢ, xᵢ-yᵢ, yᵢ-0 of a 4-cycle 0-1-xᵢ-yᵢ-0 sharing the edge 0-1. · Usa2022P6.constrEdges

constrGraph def

The graph of the construction. · Usa2022P6.constrGraph

constrSet def

The extremal construction: the points (1, 1) and (i, 2) for 2 ≤ i ≤ n. · Usa2020P5.constrSet

construct_partition def

def construct_partition (k : ℕ) (hk : 2 ≤ k) [NeZero k] [DecidableEq (Matilda (k * k) (all_black_k k))] : Finset (Matilda (k * k) (all_black_k k)) · Imo2025P6.construct_partition

constructCompanyA def

def constructCompanyA (n : Set.Ioi 1) : Company ↑n (↑n * ↑n - ↑n) · Imo2020P4.constructCompanyA

constructCompanyB def

def constructCompanyB (n : Set.Ioi 1) : Company ↑n (↑n * ↑n - ↑n) · Imo2020P4.constructCompanyB

construction def

The extremal configuration: every square of row 0 or of column 0, except the corner square (0, 0). · Usa2000P4.construction

Contest structure

structure Contest (idxType subIdxType : Type · Contest

contestant abbrev

The contestant from the triple consisting of a contestant and an ordered pair of judges. · Imo1998P2.AgreedTriple.contestant

ContestIndex abbrev

Index for identifying individual problems within a contest. Currently Nat × Nat covers (year, problemNum) and (day, problemNum). · ContestIndex

Coords structure

structure Coords · Imo2018P3.Coords

coordSet def

def coordSet (n : ℕ) : Finset ℝ · Imo2007P6.coordSet

coprimeSet def

The set of integers in [0, n) that are coprime to n. For n ≥ 2 this is the set {a₁, ..., aₘ} of the problem statement. · Usa2018P3.coprimeSet

coprimeSet1 def

1 together with all primes in {1, ..., 280}; pairwise coprime. · Imo1991P3.coprimeSet1

coprimeSet2 def

{2·41, 3·37, 5·31, 7·29, 11·23, 13·19}; pairwise coprime. · Imo1991P3.coprimeSet2

coprimeSet3 def

{2·37, 3·31, 5·29, 7·23, 11·19, 13·17}; pairwise coprime. · Imo1991P3.coprimeSet3

coprimeSet4 def

{2·31, 3·29, 5·23, 7·19, 11·17, 13·13}; pairwise coprime. · Imo1991P3.coprimeSet4

coprimeSet5 def

{2·29, 3·23, 5·19, 7·17, 11·13}; pairwise coprime. · Imo1991P3.coprimeSet5

coprimeSet6 def

{2·23, 3·19, 5·17, 7·13, 11·11}; pairwise coprime. · Imo1991P3.coprimeSet6

copyAsset def

Copy a single asset · copyAsset

Corner abbrev

abbrev Corner : Type · Usa1998P4.Corner

corner_set def

The image set of findLineCorner. · Imo2025P1.coverGridNoEdgeConfig.corner_set

cornerCell def

The second cell used in the corner propagation argument for the 5 × n case: it is the cell just next to a tile placed in the corner which cannot be covered by any other tile. · Imo2004P3.cornerCell

cornerDelta def

The sum of the values of the four cells touching a grid-line corner. · Usa1998P4.cornerDelta

cornerMax def

cornerMax h k r s n is the maximum, over all ways of choosing each of n further variables to be either h or k, of (r + sum of the choices) * (s + sum of the reciprocals of the choices). It is defined recursively; the leaves of … · Usa1977P5.cornerMax

cornerPoint def

The points on the three corners of grid n · Imo2025P1.coverGridNoEdgeConfig.cornerPoint

cornerSupport def

def cornerSupport (f : coloring) : Finset Corner · Usa1998P4.cornerSupport

correction abbrev

abbrev correction (m k : ℕ) · Usa2026P4.correction

countCol def

The number of column sequences of length n+1 with distinct adjacent columns starting with s and ending with t. · Usa2013P2.countCol

counterexSeq def

The counterexample for n ≤ 12: the numbers √F₁, √F₂, ... where F is the Fibonacci sequence. · Usa2012P1.counterexSeq

cov def

cov n i j means that cell (i, j) is torn out by the efficient pattern. · Usa2002P6.cov

Cover structure

A cover of G' relative to the original graph G: a finite collection C of cliques of G' together with a labeling ℓ assigning to every edge of G' a clique containing its endpoints, such that every clique K "owns" at least … · Usa2022P6.Cover

coverConfig structure

The configuration of a finise set of lines going through a set of points in the plane. · Imo2025P1.coverConfig

coverGridConfig structure

A coverConfig with the additional requirement that the set of points to be covered is grid n · Imo2025P1.coverGridConfig

coverGridNoEdgeConfig structure

A coverGridConfig with the additional requirements that n > 1 and lines doesn't contain an edge. Note: we need n > 1 to have three corners in the grid. · Imo2025P1.coverGridNoEdgeConfig

covers def

def covers (m : Matilda n all_black) (l : Label n) : Prop · Imo2025P6.covers

covers def

covers b x y z means that beam b contains the unit cube at coordinates (x, y, z). · Usa2020P2.Beam.covers

cross def

def cross {n : ℕ} (i : Fin n) : Finset (Fin n × Fin n) · Imo1997P4.cross

cross def

The cross with center (0,0) and four arms of length 2006. · Usa2007P4.cross

crossAux def

The body of cross, kept reducible so that membership and cardinality can be unfolded in the auxiliary lemmas mem_aux and card_aux. (In this environment, Finset.Icc on ℤ records a Preorder ℤ instance whose term contains the … · Usa2007P4.crossAux

CrossingPoints structure

structure CrossingPoints · Imo2025P6.DisjointSetup.CrossingPoints

crossT def

The parameter value where the standard parametrization of ℓ crosses m. · Imo2014P6.Line.crossT

cspos def

The position of column-in-strip cs within its row in the strip order. · Imo2022P6.cspos

cStateVec def

State of the n'+1-lamp process of "shifted" form: lamp 0 off, lamp 1 on, and lamps 2..n' given by the vector x on Fin n'. · Imo1993P6.cStateVec

Csum def

Csum P k = Σ_{j<k} P.coeff j, the total mass of the lower coefficients. · Imo2023P3.Csum

CTrail structure

A closed trail in a pseudograph: a closed walk with no repeated edges. · Imo2020P3.CTrail

cubeCode def

The code of a cube position: the integer parts of its coordinates divided by k. Two positions sharing all three codes have left faces strictly within k of each other along every axis, so their interiors overlap; hence the code is … · Imo1976P3.cubeCode

CubeInBox abbrev

A placement of a cube of side k in the a × b × c box: the cube is the closed box [p.1, p.1 + k] × [p.2.1, p.2.1 + k] × [p.2.2, p.2.2 + k], and it must be contained in [0, a] × [0, b] × [0, c]. · Imo1976P3.CubeInBox

cutsOfLengths def

def cutsOfLengths (l : List ℝ) : Finset ℝ · Imo2026P3.cutsOfLengths

cval def

The complement of n inside its level. · Usa2022P5.cval

cyc def

The 4-cycle (one of 100) that a site belongs to: its 4×4 block together with its label within the block. · Imo2018P4.cyc

cycSign def

The sign function attached to an even-length cycle: `+1` at even positions, `-1` at odd positions. · Imo1986P6.cycSign

D

D def

Lamp n-2 is off at every positive round m ≤ n-1. · Imo1993P6.D

d def

def d : ℕ → ℕ · CIIM2022P6.d

d def

Define d(n), the function counting the number of positive divisors of n. · Imo1998P3.d

d abbrev

abbrev d {n : ℕ} (a : Fin n → ℝ) (i : Fin n) · Imo2007P1.d

D_set def

def D_set · Imo2014P4.Imo2014q4Cfg.D_set

decomp₁ def

A decomposition realising the white-square counts {1, 2, 3, 4, 5, 7, 10} (rectangle sizes 2, 4, 6, 8, 10, 14, 20). · Imo1974P4.decomp₁

decomp₂ def

A decomposition realising the white-square counts {1, 2, 3, 4, 5, 8, 9} (rectangle sizes 2, 4, 6, 8, 10, 16, 18). · Imo1974P4.decomp₂

decomp₃ def

A decomposition realising the white-square counts {1, 2, 3, 4, 6, 7, 9} (rectangle sizes 2, 4, 6, 8, 12, 14, 18). · Imo1974P4.decomp₃

decomp₄ def

A decomposition realising the white-square counts {1, 2, 3, 5, 6, 7, 8} (rectangle sizes 2, 4, 6, 10, 12, 14, 16). · Imo1974P4.decomp₄

decPairEquivGaps def

The decreasing-adjacent-pairs are equivalent to the gaps. · Imo2022P6.decPairEquivGaps

decPairOfGap def

The decreasing orientation of the cells of a gap. · Imo2022P6.decPairOfGap

decSequencesTo def

def decSequencesTo (f : α → β) (i : α) : Finset ℕ · Imo2025P6.decSequencesTo

decSubsets def

def decSubsets (f : Fin n → Fin n) : Finset (Finset (Fin n)) · Imo2025P6.decSubsets

degVec def

The degree vector, modulo 2. · Usa2008P6.degVec

delPerm def

Deleting M from a permutation: the short-circuited permutation on S.erase M, sending the predecessor of M to the successor of M. · Imo2022P3.delPerm

denomProd def

The product of the denominators of the coefficients of q of degree at most N. Scaling q by this natural number clears the denominators. · Usa1995P4.denomProd

denoms def

def denoms (x : ℝ) (n : ℕ) : Finset ℕ · Usa1983P5.denoms

descend def

The decreasing list b, b-1, ..., 1, 0. · Usa1990P4.descend

det def

The determinant of the two normals; nonzero iff the lines are not parallel. · Imo2014P6.Line.det

det def

The determinant aᵢ bⱼ − aⱼ bᵢ of two ordered pairs of nonnegative integers, viewed as an integer. · Usa2020P4.det

DetermineDeclsExtension abbrev

abbrev DetermineDeclsExtension · ProblemExtraction.DetermineDeclsExtension

diag_inter_set def

def diag_inter_set (P₁ P₂ P₃ P₄ : Pt) · Imo2023P2.diag_inter_set

diagDiff def

A diagonal of the second type: the cells (i, j) with i - j = d. · Imo2016P2.diagDiff

diagSum def

A diagonal of the first type: the cells (i, j) with i + j = s. · Imo2016P2.diagSum

Dif def

The consecutive difference Dif A j = A (j+1) - A j as an integer. · Imo2023P3.Dif

diff def

The sequence of successive differences (XORs) of y. · Usa1996P4.diff

DiffByOne def

Condition (2) of the problem, phrased for the list of base-n digits of a number as produced by Nat.digits (least significant digit first, so the "first" digit of the number is the last entry of the list): every digit except the most … · Usa1990P4.DiffByOne

Digit abbrev

abbrev Digit · Usa1972P3.Digit

digit def

The unique digit in {0, …, 9} congruent to u modulo 2 and to v modulo 5 (which exist and are unique by the Chinese remainder theorem). · Usa1997P3.digit

digitCount def

digitCount t x d counts the occurrences of the digit d among the first t decimal digits of x (least significant first), i.e. the digits of x padded with leading zeros to length t. · Usa2013P5.digitCount

DigitFree def

A natural number is (p)-digit-free if no digit of its base-p expansion equals p - 1. · Usa1995P1.DigitFree

DigitSeq abbrev

abbrev DigitSeq (n : ℕ) · Usa1972P3.DigitSeq

digitsPadded def

def digitsPadded (b m n : ℕ) : List ℕ · Usa1992P1.digitsPadded

Dir inductive

The three possible orientations of a beam. · Usa2020P2.Dir

dir def

A direction vector of the line: the normal (a, b) rotated by 90 degrees. · Imo2014P6.Line.dir

dir def

The orientation of a beam. · Usa2020P2.Beam.dir

Dirs def

The three (undirected) line directions of the grid. · Usa2014P4.Dirs

dirs abbrev

The four unit directions in which a jump is allowed. · Imo1993P3.dirs

DisjointBeams def

The non-intersection condition: two distinct beams do not share a unit cube. · Usa2020P2.DisjointBeams

disjointPairEquiv def

Disjoint pairs of finsets of Fin n correspond to ternary functions: each element is in X₀, in B₀, or in neither. · Usa2015P3.disjointPairEquiv

DisjointPairs def

The type of disjoint pairs (X₀, B₀) of finsets of Fin n; these parametrize the nontrivial valid colorings. · Usa2015P3.DisjointPairs

DisjointSetup structure

structure DisjointSetup (n : ℕ) [NeZero n] extends BaseSetup n · Imo2025P6.DisjointSetup

dist def

def dist : ℤ × ℤ → ℤ × ℤ → ℝ · Usa2017P5.dist

Distinct abbrev

The proposition that the judges in an ordered pair are distinct. · Imo1998P2.JudgePair.Distinct

Distinguished def

The condition that x is the "distinguished" coordinate of a solution (the coordinate at which the minimum of the left-hand side is attained): the other two shifted coordinates y - 1, z - 1 multiply to 1, and x - 1 is the … · Usa2013P4.Distinguished

div def

def div (attrs : List Attr · Html.div

Dividable abbrev

abbrev Dividable (n : ℕ) · Imo2023P1.Dividable

doccoCss def

def doccoCss : Asset · Assets.doccoCss

dropLast def

The dropLast of an uphill path of length at least 2 is an uphill path. · Imo2022P6.NordicSquare.UphillPath.dropLast

dropLastEquiv def

Deleting the last column: sequences of length n+2 ending in t correspond to sequences of length n+1 ending in some r ≠ t. · Usa2013P2.dropLastEquiv

dropTrailingZeros def

Remove the trailing (i.e. most significant) zeros of a digit list. · Usa2019P3.dropTrailingZeros

dst def

def dst (asset : Asset) : String · Asset.dst

dummyCols def

The dummy columns used to turn "at least k real matches" into a full matching. · Usa2022P1.dummyCols

dw def

The depth of a cell: length of a shortest walk from the root r inside D (defined to be 0 outside D). · Usa2007P4.dw

dynamic def

Helper: create a page from IO action · Page.dynamic

E

E def

def E {n : ℕ} (a : Fin n → ℝ) : ℝ · Imo1971P1.E

E abbrev

abbrev E : Fin 8 · Imo1979P6.E

e def

The "even-length line" indicator: the i-th line of any direction contains n - i tokens, which is even iff i ≡ n (mod 2). · Usa2013P3.e

Easy def

A problem is easy for a cohort (boys or girls) if at least three of its members solved it. · Imo2001P3.Easy

Ecard def

Number of even-length lines in one direction. · Usa2013P3.Ecard

eCnt def

The multiplicity of the value v among the entries. · Usa2017P2.eCnt

ectx def

The edge context of the red line ℓ. · Imo2014P6.Witness.ectx

edgeCoeffs def

def edgeCoeffs (n : ℕ) (d : Fin 3) : LineCoeffs · Imo2025P1.edgeCoeffs

EdgeColoring structure

An edge coloring of the complete graph on 9 vertices by two colors (encoded as Fin 2), where some edges may be left uncolored (none). The vertices are indexed by Fin 9 and the edges by unordered pairs Sym2 (Fin 9); the geometric … · Imo1992P3.EdgeColoring

EdgeCtx structure

A bounded cell of an arrangement in general position, together with a distinguished boundary line ℓ. · Imo2014P6.EdgeCtx

edgeEndpointCornerId def

def edgeEndpointCornerId (d : Fin 3) (r : Fin 2) : Fin 3 · Imo2025P1.edgeEndpointCornerId

edgeEndpointIndex def

def coverGridNoEdgeConfig.edgeEndpointIndex (C : coverGridNoEdgeConfig) (r : Fin 2) : Fin C.n · Imo2025P1.coverGridNoEdgeConfig.edgeEndpointIndex

edgeIdx def

The position of the unordered pair {i, j} in the list pair. · Usa1981P2.edgeIdx

edgeLine def

The three edge lines of a the grid point to be covered in a coverGridConfig · Imo2025P1.coverGridConfig.edgeLine

edgeLine def

The three lines on the edges of the triangular integer grid, each side having n points: x - 1 = 0; y - 1 = 0; x + y - (n + 1) = 0. These lines are named edgeLine n 0, edgeLine n 1, edgeLine n 2, resp. · Imo2025P1.edgeLine

edgePoint def

The points on the three edges of a coverGridConfig · Imo2025P1.coverGridConfig.edgePoint

Edges abbrev

The edges of the complete graph on Fin N: two-element subsets. · Imo1988P2.Edges

edgeSets def

The set of edges incident to the vertex i. · Imo1988P2.edgeSets

eFn def

The vector with only the last lamp on. · Imo1993P6.eFn

elabProblemFile def

def elabProblemFile (tk : Syntax) (md : Option (TSyntax `term)) : Command.CommandElabM Unit · ProblemExtraction.elabProblemFile

emb def

def Label.emb (t : LabelType) : Point n ↪ Label n · Imo2025P6.Label.emb

embed_B def

def embed_B : (B n) ↪ {x | T n x} · Imo1989P6.embed_B

embedFinLE def

def embedFinLE {m n : ℕ} (hmn : m ≤ n) : Fin m ↪ Fin n · Imo2009P6.embedFinLE

empties def

The empty squares of the board. · Usa1999P5.empties

emptySquares def

def emptySquares {n : ℕ} (c : Finset (checkerboard n)) : Finset (checkerboard n) · Usa1999P1.emptySquares

encodePoint def

def encodePoint (f : Signature → ℕ) : RealizedPoint f ↪ ℤ · Usa2024P2.encodePoint

EndInevitable inductive

inductive EndInevitable (a : ℕ+) (n : ℕ) : State n → Prop · Usa2023P4.EndInevitable

EndInevitableIn inductive

end is inevitable in M moves · Usa2023P4.EndInevitableIn

Ends def

The "ends" placements: cards 1 and n are alone in two boxes and all cards 2, ..., n - 1 are in the third box. · Imo2000P4.Ends

endsfun def

The "ends" placements of the 100 cards. · Imo2000P4.endsfun

entries def

The number of times the visitor enters junction v during her walk, from the initial state σ₀ until she gets back to the starting junction (the final re-entry into the starting junction counts, the departure from it does not). · Usa2021P2.Park.entries

Entry structure

An entry in the state of the Problem Extraction environment extension · ProblemExtraction.Entry

EntryVariant inductive

inductive EntryVariant · ProblemExtraction.EntryVariant

eqAffSubOfPlane def

The decidable equality predicate L = L' for (L L' : AffSubOfPlane). · Imo2025P1.eqAffSubOfPlane

eqBefore def

The set of positions j < i with a j = a i. · Usa1987P5.eqBefore

EquivPilings inductive

Two pilings are equivalent if they are related by a sequence of stone moves. · Usa2015P4.EquivPilings

eraseMin def

def eraseMin (s : Finset ℕ) · Imo1981P2.eraseMin

escPath def

The rabbit's path during an escape phase when it chooses the point a + t • u + w. · Imo2017P3.escPath

escPathY def

The rabbit's path during an escape phase when it chooses the point a + t • u - w. · Imo2017P3.escPathY

escReps def

The reports made during an escape phase: the device reports the point on the line through the previous positions, at the same fractional distance as the rabbit. · Imo2017P3.escReps

escStep def

One escape phase with frame {u, w}: the rabbit runs to one of the two points a + t • u ± w (choosing the one farther from where the hunter ends up), while the device reports points on the line. · Imo2017P3.escStep

EssentiallyIncreasing def

A function f : ℝ → ℝ is essentially increasing if f s ≤ f t whenever s ≤ t are real numbers such that f s ≠ 0 and f t ≠ 0. · Usa2022P5.EssentiallyIncreasing

eval def

Evaluation of a homogeneous form at a point. · Imo2017P6.HForm.eval

evasiveHist def

The history after j rounds against the evasive wizard. · Usa2016P6.evasiveHist

evasiveWizard def

The wizard that evades the player forever when k = n. · Usa2016P6.evasiveWizard

evenSum def

The sum of entries at even (0-indexed) positions. · Imo2026P3.evenSum

EventuallyPeriodic def

def EventuallyPeriodic (b : ℕ → ℕ) : Prop · Imo2024P3.EventuallyPeriodic

evPairs def

The sequence of pairs of students that switch places: each entry is (student in front, student behind), with front rank < behind rank. · Usa2010P2.evPairs

example_16 def

def example_16 : Fin 16 → ℝ · Imo1977P2.example_16

example_16_int def

def example_16_int : Fin 16 → ℤ · Imo1977P2.example_16_int

examplePlanes def

def examplePlanes (n : ℕ) : Finset Plane · Imo2007P6.examplePlanes

exists_desired_triangle def

def exists_desired_triangle : Prop · Imo2018P3.exists_desired_triangle

ExistsDecreaseOn def

def ExistsDecreaseOn (s : Finset ℝ) (f : ℝ → ℝ) · Imo2021P2.ExistsDecreaseOn

Expressible def

A natural number n is expressible if it can be written as a sum of positive integers whose reciprocals sum to 1. · Usa1978P3.Expressible

extend def

Add a diagonal line x + y = n + 2 to a countAndStrongCover · Imo2025P1.strongCoverGridConfig.extend

extend def

The checksum construction: given five digits f : Fin 5 → ZMod 10, build a six-digit plate whose last digit makes the total digit sum congruent to zero modulo ten. · Usa1990P1.extend

extendPerm abbrev

abbrev extendPerm {m n : ℕ} (f : Equiv.Perm (Fin m)) (h : m ≤ n) : Equiv.Perm (Fin n) · Imo2009P6.extendPerm

extendPerm def

Extension of a permutation of Fin n to Fin (n + 1) fixing j, via the identification Fin n ≃ {x // x ≠ j}. · Usa2018P6.usa2018p6_aux.extendPerm

ExternallyTangent def

def ExternallyTangent (c1 c2 : Circle) : Prop · Usa2000P5.ExternallyTangent

extractFromExt def

def extractFromExt {m : Type → Type} [Monad m] [MonadEnv m] [MonadError m] (ext : ExtractionExtension) : m (NameMap String) · ProblemExtraction.extractFromExt

ExtractionExtension abbrev

abbrev ExtractionExtension · ProblemExtraction.ExtractionExtension

extractMetadata def

Using the data in the solution extraction environment extension, constructs a map from module name to problem metadata · ProblemExtraction.extractMetadata

extractModuleDoc def

def extractModuleDoc (env : Lean.Environment) (m : Lean.Name) : String · extractModuleDoc

extractProblems def

Using the data in the problem extraction environment extension, constructs a map from module name to problem source code. · ProblemExtraction.extractProblems

extractSolutions def

Using the data in the solution extraction environment extension, constructs a map from module name to solution source code. · ProblemExtraction.extractSolutions

extremal def

The extremal triangle: red dot of row i at position 2 ^ (clog₂ (i+1)) - 1 - i. · Imo2023P5.extremal

extremalAdj def

Adjacency in the extremal graph: all pairs of distinct vertices except 0—1 and 0—2. · Usa1982P1.extremalAdj

extremalGraph def

The extremal graph: the complete graph on Fin 1982 with the two edges 0—1 and 0—2 removed. · Usa1982P1.extremalGraph

e₁ def

The first standard basis vector. · Imo2013P2.e₁

F

F def

def F : ℚ · Imo1981P2.F

F def

def F · Imo2023P2.Imo2023q2Cfg.F

F def

The first moment when both members of a pair A are asleep. · Usa1986P2.F

F def

Ordered pairs of distinct indices whose values collide for the shift k. · Usa2018P4.F

f def

def f (x y z A B C : ℝ) : Fin 3 → ℂ · f

f def

def f (a b c : ℝ) : ℝ → ℝ · Imo1968P3.f

f abbrev

abbrev f (x: ℝ) · Imo1988P4.f

f def

def f (n : ℕ) : ℤ[X] · Imo1993P1.f

f def

The function f of the problem: the number of elements of {k+1, ..., 2k} whose binary representation has exactly three 1s. · Imo1994P3.f

f def

f n is the number of ways of representing n as a sum of powers of two with non-negative integer exponents, where representations that differ only in the order of their summands are considered the same. Rather than defining f as a … · Imo1997P6.f

f def

f j i p is the maximum number of red dots on a ninja path from the top row to position p of row i (and 0 if the position is invalid). · Imo2023P5.f

f def

def f (p : Point (k * k)) : ℤ × ℤ · Imo2025P6.f

f def

def f (g : Equiv.Perm (Fin (k + 2))) (hg : g ∈ (S' k m)) · UK2024R1P1.f

f def

The function whose zeros are the real roots of the quartic. · Usa1985P2.f

f def

The first moment at which all members of A are simultaneously asleep. · Usa1986P2.f

f def

The quantity f(i) from the problem statement. · Usa1987P5.f

f def

def f : ℕ → ℝ → ℝ · Usa1990P2.f

f def

The tower-of-exponents function of the problem, with the index shifted by one: f 0 = 2 and f (n + 1) = 2 ^ f n, so that the problem's f n is our f (n - 1). · Usa1991P3.f

f def

def f (a b c : ℝ) : ℝ · Usa2001P3.f

f def

f n is the minimal k for which there exists a k-stable set with n integers. (That the defining set is nonempty is proved in stable_exists. · Usa2005P6.f

f def

The auxiliary potential: blue points are those with f p ≡ 2n - 1 (mod 4). · Usa2008P3.f

f def

f C is the smallest number of operations required to obtain C. · Usa2013P3.f

f def

Our construction (valid for x ∈ ℝ) is P_x := (x-2014/3, (x-2014/3)^3). · Usa2014P3.f

f def

def f (x : Fin 4 → ℝ) : ℝ · Usa2017P6.f

f def

The values aᵢ + ik (computed in ZMod p) produced by the shift k. · Usa2018P4.f

f def

def f (n : ℕ) (x : ℝ) : ℝ · Usa2026P1.f

f' def

def f' (m : Fin (k + 2)) (g : Equiv.Perm (Fin (k + 1))) · UK2024R1P1.f'

f'_invFun def

def f'_invFun (g : Equiv.Perm (Fin (k + 1))) (m : Fin (k + 2)) (n : Fin (k + 2)) : Fin (k + 2) · UK2024R1P1.f'_invFun

f'_toFun def

def f'_toFun (g : Equiv.Perm (Fin (k + 1))) (m : Fin (k + 2)) (n : Fin (k + 2)) : Fin (k + 2) · UK2024R1P1.f'_toFun

f_good def

def f_good (f : ℝ → ℝ) : Prop · Usa2016P4.f_good

f_invFun def

def f_invFun (g : Equiv.Perm (Fin (k + 2))) (hg : g ∈ (S' k m)) (n : Fin (k + 1)) : Fin (k + 1) · UK2024R1P1.f_invFun

f_toFun def

def f_toFun (g : Equiv.Perm (Fin (k + 2))) (hg : g ∈ (S' k m)) (n : Fin (k + 1)) : Fin (k + 1) · UK2024R1P1.f_toFun

Fantastic def

An involution is fantastic if its edges have pairwise distinct labels. · Usa2018P6.Fantastic

faq def

def faq (config : SConfig) : List Html · faq

faviconIco def

def faviconIco : Asset · Assets.faviconIco

Favorable def

The event that the triangle formed by the first three points is disjoint from the triangle formed by the last three points. With six points on a circle, the two triangles are disjoint iff the two vertex sets do not interleave around the … · Usa1983P1.Favorable

fcard def

The number of fixed-point-free involutions of Fin n. · Usa2018P6.usa2018p6_aux.fcard

fdef def

The defect f x - x of a function on the positive reals. · Imo2026P5.fdef

FE def

def FE (f : ℝ → ℝ) : Prop · Usa2002P4.FE

fExample def

An example of a function achieving the maximum number of values of f(r)+f(-r). · Imo2024P6.fExample

ffun def

The j-th constructed function on the real line; it is nonzero only at the integers 1, …, 2047. · Usa2022P5.ffun

fib def

The fiber over v of the value map of the shift k. · Usa2018P4.fib

Fiber abbrev

The possible values of a filling at a fresh cell s, given the values A f and C f forced by the neighbors of s. · Usa2019P4.Fiber

fiber def

Given α : Type* and k : ℕ, fiber α k is the set of permutations of α with exactly k fixed points. · Imo1987P1.fiber

FibPair def

The classification of solutions of a^2 + b^2 + 1 = 3 * a * b: either a = b = 1, or {a, b} = {F_{2k-1}, F_{2k+1}} for some k ≥ 1. · Usa2026P6.FibPair

filled def

The set of cells filled after the first n moves of a play. · Usa2004P4.filled

Fillings def

Partial configurations on a set D of cells: the cardinality and monotonicity conditions hold on D, and the value is ∅ off D (the latter condition keeps the ambient function type finite). · Usa2019P4.Fillings

fillRank def

Fill one rank with the least residue making divisibility hold. · Usa2024P2.fillRank

filt def

filt e c y ss processes the list of jumps ss starting at position y, deleting every jump whose length is divisible by 2 ^ (e + 1) and which lands at a position greater than c. This is the deletion operation of the official … · Usa2006P5.filt

filterProblemCount def

def filterProblemCount (c : Contest idx subIdx) (f : idx → subIdx → Bool) : Nat · Contest.filterProblemCount

fin_equiv def

def fin_equiv : Finset.Icc 1 (2*n) ≃ Fin (2*n) · Imo1989P6.fin_equiv

finalBoard def

The final board of a play: after 36 moves every cell is filled (see prefBoard_finalBoard), and this is the number written in each cell. · Usa2004P4.finalBoard

finBlocks def

def finBlocks (b : Fin m → List ℝ) : List (List ℝ) · Imo2026P3.finBlocks

findFstEq def

The first path element whose row is at least r. Since rows change by at most one on each move and the path starts in row 0, this is in fact on row r: see Path.findFstEq_fst. · Imo2024P5.Path.findFstEq

findLine def

coverGridConfig.findLine chooses a line in lines that goes through x · Imo2025P1.coverGridConfig.findLine

findLineCorner def

coverGridNoEdgeConfig.findLineCorner C c chooses a line in lines that goes through C.cornerPoint c using the function findLine. · Imo2025P1.coverGridNoEdgeConfig.findLineCorner

findLineEdge def

coverGridConfig.findLineEdge chooses a line in lines that goes through C.edgePoint d i using the function coverGridConfig.findLine. · Imo2025P1.coverGridConfig.findLineEdge

findModuleImports def

Helper function for extractFromExt. · ProblemExtraction.findModuleImports

finish def

The last station in a linkage. · Imo2020P4.Company.linkage.finish

firstMonster def

The first monster on a path, or none. · Imo2024P5.Path.firstMonster

firstPlayerShare def

The sum of the entries of a list L at the (0-indexed) even positions, after sorting L in non-increasing order. These are the entries in the 1st, 3rd, 5th, … positions of the sorted (decreasing) list, i.e. the pieces claimed by … · Imo2026P3.firstPlayerShare

fixedDecompEquiv def

The fixed points of the conjugation involution decompose as a choice on {a, b} (identity or swap) times a switching involution of the reduced vertex. · Usa2018P6.fixedDecompEquiv

fixedPointsEquiv def

The set of pairs (x : α, σ : Perm α) such that σ x = x is equivalent to the set of pairs (x : α, σ : Perm {x}ᶜ). · Imo1987P1.fixedPointsEquiv

fixedPointsEquiv' def

The set of triples (k ≤ card α, σ ∈ fiber α k, x ∈ fixedPoints σ) is equivalent to the set of pairs (x : α, σ : Perm α) such that σ x = x. The equivalence sends (k, σ, x) to (x, σ) and (x, σ) to (card (fixedPoints σ), σ, x). · Imo1987P1.fixedPointsEquiv'

flattenFinBlocks def

def flattenFinBlocks (b : Fin m → List ℝ) : List ℝ · Imo2026P3.flattenFinBlocks

flip def

def Coin.flip : Coin → Coin · Imo2022P1.Coin.flip

flip abbrev

abbrev flip (n : ℕ) {c : ℝ} (l : labelling c) : labelling c · Usa2017P5.flip

flipIx def

The index of the coin that Harry flips in configuration c: the k-th coin from the left, where k is the number of heads. · Imo2019P5.flipIx

flipPair def

The flip on pairs (σ, φ). · Usa2018P6.flipPair

fn0 def

The first attempt in a winning strategy, as a function: first pass along the second row to locate the monster there. · Imo2024P5.fn0

fn1OfEdge0 def

The second attempt in a winning strategy, as a function, if the monster in the second row is at the left edge: zigzag across the board so that, if we encounter a monster, we have a third path we know will not encounter a monster. · Imo2024P5.fn1OfEdge0

fn1OfNotEdge def

The second attempt in a winning strategy, as a function, if the monster in the second row is not at an edge: pass to the left of that monster then along its column. · Imo2024P5.fn1OfNotEdge

fn2OfEdge0 def

The third attempt in a winning strategy, as a function, if the monster in the second row is at the left edge and the second (zigzag) attempt encountered a monster: on the row before the monster was encountered, move to the following row … · Imo2024P5.fn2OfEdge0

fn2OfNotEdge def

The third attempt in a winning strategy, as a function, if the monster in the second row is not at an edge: pass to the right of that monster then along its column. · Imo2024P5.fn2OfNotEdge

FollowsStrategy def

A play follows Bob's strategy σ if each of Bob's moves (the odd-numbered moves) is the move prescribed by σ on the current board. · Usa2004P4.FollowsStrategy

footer def

def footer (attrs : List Attr · Html.footer

footerComp def

def footerComp (config : SConfig) : List Html · footerComp

ForcesWinIn def

Whether a strategy forces a win within the given number of attempts. · Imo2024P5.Strategy.ForcesWinIn

formalizedCount def

def formalizedCount (c : Contest idxType subIdxType) (mds : Lean.NameMap ProblemMeta) : Nat · Contest.formalizedCount

formedQuadraticEval def

The formed quadratic evaluated at t, i.e. the quadratic with coefficients formedQuadratic a b c applied to t. · Imo1959P3.formedQuadraticEval

FourPointProperty def

The hypothesis of the problem: among any four vertices of the graph, some vertex is adjacent to the other three. · Usa1982P1.FourPointProperty

fpfDecomposeEquiv def

Fixed-point-free involutions of Fin (n + 2) are in bijection with pairs of an element j : Fin (n + 1) (the partner of 0) and a fixed-point-free involution of Fin n. · Usa2018P6.usa2018p6_aux.fpfDecomposeEquiv

fpfSubtype def

Fixed-point-free involutions of Fin n. · Usa2018P6.usa2018p6_aux.fpfSubtype

Fpoly def

Fpoly P A k m := ∏_{i=1}^{k} (X + C (A (m+i) - A m)) - P; it vanishes at A m. · Imo2023P3.Fpoly

fracs def

Rationals in the interval with reduced denominator at most `n`. · Usa1983P5.fracs

Fragrant abbrev

abbrev Fragrant (s : Set ℕ+) : Prop · Imo2016P4.Fragrant

fromColoring def

The map from a valid coloring to its parametrizing data: none for the all-red coloring, and the disjoint pair (X c, B c) otherwise. · Usa2015P3.fromColoring

fromCounts def

def fromCounts (counts : List (Nat × Nat)) : List (Nat × Nat) · fromCounts

frontContrib def

The number of inversions contributed by the first position when it has entry x and threshold c, over the remaining entries w. · Usa2017P2.frontContrib

Fs def

The integer-valued function Fs f t = 4^d · f(t²/4), where d = f.natDegree; the powers of 4 clear the denominators. · Usa2006P3.Fs

fsucc def

The student of rank one higher than a (well-defined when a is not the tallest student). Defined as a literal so that (fsucc a h).val is definitionally a.val + 1. · Usa2010P2.fsucc

fwdDiff def

The forward difference operator on real sequences. · Usa1984P5.fwdDiff

G

G abbrev

abbrev G : Fin 8 · Imo1979P6.G

G def

def G : SimpleGraph (V n r) · Imo1981P2.G

g def

Cumulative count: the number of elements of {1, ..., n} with exactly three 1s. · Imo1994P3.g

g def

def g (n : ℕ) : ℕ · Imo1998P6.g

g def

The value of g in the problem (determined by a and b). · Imo2024P2.Condition.g

g def

def g (a b c : ℝ) : ℝ · Usa2001P3.g

g def

The residue of 1 + k * t modulo p. · Usa2006P1.g

g def

The normalized function $g(s) = f(1/s - 1)$, mapping $(0, 1)$ to $(0, 1)$. · Usa2018P2.g

g1 def

Weight functions on the exponents: cells with (i + j) % 3 = r get weight 1 for the two classes in question and 0 for the remaining one. · Imo1993P3.g1

g1 def

The other line through r (a blue line). · Imo2014P6.Witness.g1

g1ctx def

The edge context of the blue line g₁. · Imo2014P6.Witness.g1ctx

g2 def

def g2 (k : ℤ) : ZMod 2 · Imo1993P3.g2

g2 def

The other line through b (another blue line). · Imo2014P6.Witness.g2

g2ctx def

The edge context of the blue line g₂. · Imo2014P6.Witness.g2ctx

gains def

gains a n r c counts how many times cell (r, c) receives a stone, given that a tromino was placed with anchor (i, j) exactly a i j times. The cell (r, c) is covered by the trominoes anchored at (r, c), (r - 1, c) and `(r - 1, … · Usa2021P3.gains

gapCells def

Cells of a gap on an n × n board (ordered by position). · Imo2022P6.gapCells

GapDir inductive

A direction for a gap between two adjacent cells. · Imo2022P6.GapDir

gapDirEquivFin2 def

GapDir is equivalent to Fin 2. · Imo2022P6.gapDirEquivFin2

gapOfPair def

The gap determined by an ordered pair of adjacent cells. · Imo2022P6.gapOfPair

gapPair def

The ordered pair of cells of a gap: for horiz, (i, j), (i, j+1); for vert, (j, i), (j+1, i). · Imo2022P6.gapPair

gapPath def

Given adjacent cells a, b, the uphill path ending with the edge {a,b} (obtained by extending the path to the smaller-valued cell by the larger one). · Imo2022P6.NordicSquare.gapPath

gapPathInj def

The injection from gaps (plus a point for the trivial path) to uphill paths. · Imo2022P6.gapPathInj

gapSize def

The distance to the next point outside D (a positive number of steps). · Usa2025P6.CirclePartition.gapSize

gc def

The contribution of the first position, as a function of its value. · Usa2017P2.gc

GeneralPosition def

A set of lines is in general position if no two are parallel and no three pass through the same point. · Imo2014P6.GeneralPosition

generate def

def All.generate (config : SConfig) (numProved : Nat) (mdsArray : Array <| Lean.Name × ProblemMeta) : IO Page · All.generate

generate def

def generate (c : Contest idxType subIdxType) (config : SConfig) (filePath : String) (navbarState : NavbarState) (mds : Lean.NameMap ProblemMeta) (fmtIdx : idxType → String) (fmtSubIdx : subIdxType → … · Contest.generate

generate def

def Index.generate (config : SConfig) (tagFormalizedCounts : Array Nat) (tagSolvedCounts : Array Nat) (numProved : Nat) (mds : Lean.NameMap ProblemMeta) : IO Page · Index.generate

generate def

def Problem.generate (config : SConfig) (p : ProblemInfo C) : IO (List Page) · Problem.generate

generateAll def

TODO: split this into collect ⇒ Data ⇒ generate maybe serialize and reuse when no content change · generateAll

generateFormalized def

def Problem.generateFormalized (config : SConfig) (name : Lean.Name) (detail : ProblemMeta) (writeupLinks : List WriteupLink) : IO (List Page) · Problem.generateFormalized

generateProblems def

def generateProblems {idxType subIdxType : Type} [Ord idxType] [Ord subIdxType] (c : Contest idxType subIdxType) (config : SConfig) (mds : Lean.NameMap ProblemMeta) : IO <| List Page · Contest.generateProblems

generateStub def

def Problem.generateStub (p : ProblemInfo C) : List Html · Problem.generateStub

genFun def

The generating function ∑ σ, X ^ (ainvCount m A σ) of the A-inversion statistic. · Usa2017P2.genFun

geometric_mean def

def geometric_mean {n : ℕ} (f : Fin n → ℕ+) (s : Finset (Fin n)) : ℝ · Imo2020P5.geometric_mean

geomSum def

def geomSum (m : ℕ+) : ℤ[X] · Usa1977P1.geomSum

geomSumStep def

def geomSumStep (m n : ℕ+) : ℤ[X] · Usa1977P1.geomSumStep

getCrossingPoints def

def getCrossingPoints (ha_pos : 0 < c.a) (hb_pos : 0 < c.b) : CrossingPoints c · Imo2025P6.DisjointSetup.getCrossingPoints

getDeclsInPackage def

Gets the declarations that originate in modules beneath package. · ProblemExtraction.getDeclsInPackage

gExp def

The exponent g_p for a prime p and board B: the gcd of the p-adic valuations of the entries of B. Since gcd(a, 0) = a, valuations equal to 0 (entries not divisible by p) do not affect this gcd, so gExp p B is the gcd of … · Imo2026P1.gExp

gf def

def gf (n : ℕ+) : ℕ · Imo1998P6.gf

Gform def

The local form used modulo the prime p: x² + xy + y² for p = 2 and x^(p-1) + y^(p-1) for odd p. · Imo2017P6.Gform

GH def

The "good head" condition on a list: either the head is red, or it lies in B₀ (blue, y = 0) and the second point (if any) is red. For such lists the colour sum is at most the number of B₀-points. · Usa2008P3.GH

Good abbrev

abbrev Good (f : ℕ → ℕ) : Prop · Imo1993P5.Good

Good def

A placement of the cards 1, ..., n into three boxes (labeled by ZMod 3) is good if every box is nonempty and whenever two pairs of cards from two different pairs of boxes have the same sum, the pairs of boxes coincide. · Imo2000P4.Good

Good structure

The properties of a Nordic square implying the minimal number of uphill paths. · Imo2022P6.NordicSquare.Good

Good def

Good p c m expresses p = 1 + c * X + O(X^(m+1)). · Usa1988P5.Good

Good def

Formalization of "a set of 11 distinct positive integers such that every integer between 1 and 1500 is the sum of a subset", with the elements listed in increasing order as a 0 < a 1 < … < a 10. · Usa1992P3.Good

Good def

The specification of the problem: Q has coefficients in {0, …, 9} and takes the values u at -2 and v at -5. · Usa1997P3.Good

Good def

A set S of squares on an m × n board contains no forbidden triangle: one cannot find three (distinct) chosen squares whose centers form a right triangle with sides parallel to the edges of the board, that is, with two of them in the … · Usa2000P4.Good

Good def

The property of the natural number k occurring in the problem: every 2022-tuple (x₁, …, x₂₀₂₂) of real numbers is the pointwise sum of k essentially increasing functions at the points 1, …, 2022. · Usa2022P5.Good

Good def

The property required of n: writing the divisors of n ! in increasing order as 1 = d₁ < d₂ < ⋯ < dₖ = n !, the consecutive gaps are non-decreasing. We phrase this using consecutive triples: whenever a < b < c are divisors of n ! … · Usa2024P1.Good

Good structure

structure Good (S : Fin 100 → Set ℤ) : Prop · Usa2024P2.Good

good def

def good [Ring R] (f : R → R) · Imo2017P2.good

good def

Auxiliary condition: m * n is of the form x ^ 2 + x + k for a nonnegative integer x. The problem uses positive x, but uniqueness of placements for the weaker (nonnegative) condition implies uniqueness for the stronger one. · Imo2022P3.good

good_seqs def

def good_seqs {n : ℕ} · Usa1972P3.good_seqs

GoodA abbrev

A binary sequence of length n (encoded as x : Fin n → Bool, with false standing for 0 and true for 1) is A-good if it contains no three consecutive terms equal to 0, 1, 0 in that order. · Usa1996P4.GoodA

GoodArrangement def

An arrangement of lines (one-dimensional affine subspaces of the plane) is good for a configuration if no line passes through a point of the configuration and every red point is strictly separated from every blue point by at least one of … · Imo2013P2.GoodArrangement

GoodB abbrev

A binary sequence of length n is B-good if it contains no four consecutive terms equal to 0, 0, 1, 1 or 1, 1, 0, 0 in that order. · Usa1996P4.GoodB

GoodCircle def

GoodCircle n says that all divisors of n that are greater than 1 can be arranged in a circle so that no two adjacent divisors are relatively prime. The circle is represented by a list l containing each such divisor exactly once; … · Usa2005P1.GoodCircle

GoodMateValue def

GoodMateValue b x vx w says that the number w is a legal and good answer for Bob in the mate of the cell x (which contains vx): it does not yet appear on the board, and it occupies the same position relative to the entries of the … · Usa2004P4.GoodMateValue

goodNats def

goodNats is the set of natural numbers satisfying the condition in the problem statement, namely the a : ℕ such that n^4 + a is not prime for any n : ℕ. · Imo1969P1.goodNats

goodPairs def

The good index pairs of a choice v of 100 points. · Usa2020P4.goodPairs

GoodPlacement def

Combinatorial form of validity: whenever two pairs of cards from two different pairs of boxes have the same sum of indices, the pairs of boxes coincide. Equivalent to ValidPlacement (valid_iff_good); this is the form used in the … · Imo2000P4.GoodPlacement

GoodRect def

The predicate characterising the rectangles that can be tiled by hooks. · Imo2004P3.GoodRect

goodSets def

The good two-element subsets of a set of points: those {P, Q} with |det P Q| = 1. · Usa2020P4.goodSets

gpd def

The greatest prime divisor of an integer m, with the convention gpd (±1) = 1. (The value at 0 is irrelevant for the problem, which requires f(n²) ≠ 0 anyway.) · Usa2006P3.gpd

gPNat def

def gPNat (n : ℕ+) : ℕ+ · Imo1998P6.gPNat

graph def

def Company.graph {n k : ℕ} (c : Company n k) : SimpleGraph (Fin (n ^ 2)) · Imo2020P4.Company.graph

grid def

The integer grid consisting of (a, b), where a, b are positive integers and a + b ≤ n + 1. · Imo2025P1.grid

gridAdj def

Two cells of the integer lattice are adjacent when they share an edge, i.e. their Manhattan distance is 1. · Usa2007P4.gridAdj

gridGraph def

Use the full grid graph and the subgraph induced by the checkers. · Usa1999P1.gridGraph

gridGraph def

The infinite grid graph on ℤ × ℤ: vertices are cells, edges join edge-adjacent cells. · Usa2007P4.gridGraph

gridPos abbrev

The grid arrangement of cube positions: cubes at (i * k, j * k, l * k) for i < ⌊a / k⌋₊, j < ⌊b / k⌋₊, l < ⌊c / k⌋₊. · Imo1976P3.gridPos

gridShift def

def gridShift (d : Fin 3) : Plane · Imo2025P1.gridShift

groupedIndices def

def groupedIndices (I J : Finset (Fin m)) : List (Fin m) · Imo2026P3.groupedIndices

GuaranteesWin def

Player B's strategy σ guarantees a win if 1. against any answer sequence that stays consistent with x forever, B eventually stops and guesses, and 2. whenever B guesses X at time T and the answers given so far are consistent with … · Imo2012P3.GuaranteesWin

gval def

The value of the j-th constructed function at the integer point n: zero outside [1, 2047]; on its own level (j = lvl n - 1) it is the corrector xe x n - cval n * Bnd x, and on higher levels it is the bit contribution `2^j * Bnd … · Usa2022P5.gval

H

H def

def H : Pt · Imo2023P2.Imo2023q2Cfg.H

h1 def

def h1 (attrs : List Attr · Html.h1

h2 def

def h2 (attrs : List Attr · Html.h2

h3 def

def h3 (attrs : List Attr · Html.h3

h4 def

def h4 (attrs : List Attr · Html.h4

halfBeams def

The construction: 3030 beams forming a staircase. · Usa2020P2.halfBeams

halfBlockAt def

def halfBlockAt (p : List ℝ) (i : Fin p.length) : List ℝ · Imo2026P3.halfBlockAt

hallTargets def

Hall targets for row r: good real columns, plus all dummy columns. · Usa2022P1.hallTargets

has_digit_one def

def has_digit_one (n : ℕ) : Prop · Usa2026P4.has_digit_one

HasAngle def

A triangle s has an interior angle equal to θ. · Imo2026P4.HasAngle

HasAp def

HasAp a p n m means that the first n + 1 terms a 0, a 1, …, a (n-1), m (where the candidate m is the n-th term) contain an arithmetic progression of length p: there are strictly increasing indices v 0 < v 1 < … < v (p-1), all … · Usa1995P1.HasAp

HasChain def

HasChain n means that an n-element set (which we may take to be Fin n) admits a sequence of 100 mutually distinct nonempty subsets in which any two consecutive sets are disjoint and do not cover the whole set. · Usa2016P1.HasChain

HasEmptySquare def

A peaceful configuration of n rooks is a permutation σ: the rook in row i sits in column σ i. Such a configuration has a rook-free k × k square if there is a block of k consecutive rows and k consecutive columns (fitting on … · Imo2014P2.HasEmptySquare

HasEven abbrev

abbrev HasEven {n : ℕ} (s : DigitSeq n) : Prop · Usa1972P3.HasEven

HasFive abbrev

abbrev HasFive {n : ℕ} (s : DigitSeq n) : Prop · Usa1972P3.HasFive

HasMonoRectangle def

A coloring (true = red, false = blue) of an m × n board has a monochromatic rectangle if there are two distinct rows and two distinct columns whose four intersection squares all have the same color. · Usa1976P1.HasMonoRectangle

HasMonoTriangle def

A coloring has a monochromatic triangle if there are three distinct vertices whose three connecting edges all have the same color. · Imo1992P3.EdgeColoring.HasMonoTriangle

hasProblemName def

def hasProblemName (c : Contest idx subIdx) (name : Lean.Name) : Bool · Contest.hasProblemName

HasRook def

σ places a rook in every axis-aligned K × K square — exactly the negation of HasEmptySquare. · Imo2014P2.HasRook

HasSOS def

The board contains three consecutive squares spelling S O S. · Usa1999P5.HasSOS

HasThreat def

The player to move can win immediately: some legal move produces SOS. · Usa1999P5.HasThreat

HasTrap def

The board contains a trap. · Usa1999P5.HasTrap

HasUniqueLarge def

A board has a unique large entry when exactly one entry is > 1. · Imo2026P1.HasUniqueLarge

hblock def

A horizontal block: three adjacent stamps in a single row. · Usa2002P6.hblock

head def

def head (c : List Html) · Html.head

headBit def

def headBit : List (Fin 2) → Fin 2 · Usa1996P6.headBit

header def

def header (attrs : List Attr · Html.header

hfn def

The discrepancy between g and its linear interpolant on [1/8, 3/8], rescaled to parameters in [0, 1]. · Usa2018P2.hfn

HForm structure

A homogeneous polynomial in two variables with integer coefficients, represented by its degree and coefficient function. Evaluation is ∑ i ∈ range (deg + 1), coeff i * x^i * y^(deg - i). · Imo2017P6.HForm

highBit def

def highBit (d : Fin 4) : Fin 2 · Usa1996P6.highBit

highlightMinJs def

def highlightMinJs : Asset · Assets.highlightMinJs

Hill def

A "hill" in a Nordic square: a cell adjacent only to cells with smaller values. · Imo2022P6.NordicSquare.Hill

hillFiberEquiv def

The fiber of uphill paths ending at a hill is equivalent to its set of neighbors. · Imo2022P6.NordicSquare.hillFiberEquiv

hist def

The answer history after t questions, when player A answers according to ans. · Imo2012P3.hist

hole def

The "hole" (notch) of a hook: the centre cell of its bounding box. · Imo2004P3.hole

hookShapes def

The eight orientations of the hook (rotations and reflections of the figure in the problem statement). Each orientation is a 3 × 3 square with three cells removed: the centre cell, the middle cell of one side, and a corner cell adjacent … · Imo2004P3.hookShapes

hr def

def hr · Html.hr

Html inductive

HTML document tree. Structural correctness by construction. · Html

html def

def html (attrs : List Attr · Html.html

htmlEscape def

Escape for HTML text content · htmlEscape

htmlEscapeAttr def

Escape for HTML attribute values (superset of text escaping) · htmlEscapeAttr

hunterPos def

The hunter's position after round n when using strategy σ against the reported points p 1, ..., p n. · Imo2017P3.hunterPos

I

I def

the endpoints don't matter in the volume, so we don't need to know if they are in the solution or not · Imo1988P4.I

I abbrev

abbrev I (A B C : P) (hABC : AffineIndependent ℝ ![A, B, C]) : P · Usa1988P4.I

id_ def

def id_ (i : String) : Attr · Html.id_

IData abbrev

The insertion data: where and on which pan the weight 2^0 is inserted. Sum.inl k (with k : Fin (n + 1)) inserts it on the left pan at position k; Sum.inr k (with k : Fin n) inserts it on the right pan at position k + 1 (the … · Imo2011P4.IData

im def

The set of values attained by the shift k. · Usa2018P4.im

img def

def img (src : String) (alt : String) (attrs : List Attr · Html.img

Imo2001q1Cfg structure

structure Imo2001q1Cfg · Imo2001P1.Imo2001q1Cfg

Imo2012P5Cfg structure

A configuration satisfying the conditions of the problem. · Imo2012P5.Imo2012P5Cfg

Imo2014q4Cfg structure

structure Imo2014q4Cfg · Imo2014P4.Imo2014q4Cfg

Imo2019q2Cfg structure

A configuration satisfying the conditions of the problem. We define this structure to avoid passing many hypotheses around as we build up information about the configuration; the final result for a statement of the problem not using this … · Imo2019P2.Imo2019q2Cfg

Imo2023q2Cfg structure

structure Imo2023q2Cfg · Imo2023P2.Imo2023q2Cfg

imoProblemCounts def

def imoProblemCounts · imoProblemCounts

in_white_rect def

def in_white_rect (s t : Int) (p : Point n) : Prop · Imo2025P6.in_white_rect

InAtLeastKSubsets abbrev

z is in at least k of the sets S. · Usa2024P2.InAtLeastKSubsets

incidence def

def incidence {V E : Type*} [Fintype V] [Fintype E] (src dst : E → V) : (V → ZMod 3) →ₗ[ZMod 3] (E → ZMod 3) · Imo2026P3.CodexMod3.incidence

incidence_count def

def incidence_count (u v all_black : Finset (Point n)) (p : Point n) : ℕ · Imo2025P6.incidence_count

incidenceCoeff def

def incidenceCoeff (B : Fin m → Finset ℤ) (a : ℤ) (k : Fin m) : ℤ · Imo2021P6.incidenceCoeff

IncreasingSequenceFromOne structure

A sequence of real numbers satisfying the given conditions · Imo1970P3.IncreasingSequenceFromOne

incSequencesTo def

def incSequencesTo (f : α → β) (i : α) : Finset ℕ · Imo2025P6.incSequencesTo

incSubsets def

def incSubsets (f : Fin n → Fin n) : Finset (Finset (Fin n)) · Imo2025P6.incSubsets

Indecomposable def

m is indecomposable in Vₙ if it belongs to Vₙ but cannot be written as a product of two members of Vₙ. · Imo1977P3.Indecomposable

indexedDiffs def

def indexedDiffs (q : List ℝ) : List ℝ · Imo2026P3.indexedDiffs

indexInBlock def

def indexInBlock (l : List ℕ) (k : ℕ) · Imo2022P1.indexInBlock

initArr def

The wizard's initial arrangement: a bijection of each of σ [] and its complement onto the labels. · Usa2016P6.initArr

initEquiv₁ def

The equivalence between the first query and the labels. · Usa2016P6.initEquiv₁

initEquiv₂ def

The equivalence between the complement of the first query and the labels. · Usa2016P6.initEquiv₂

initial abbrev

The initial state: all lamps on, and the next step happens at lamp 0. · Imo1993P6.initial

initial def

The initial configuration: 1, 2, 1, 2, ..., 1, 2, 3. · Usa1994P2.initial

initialCover def

The initial cover of G: one K₂ per edge. · Usa2022P6.initialCover

initPos def

The initial position: an n × n block of occupied squares. · Imo1993P3.initPos

inner def

def inner : Finset (Fin 99) · Usa1998P4.inner

innerSum def

For l = [b₁, ..., bₘ], innerSum l is 4 * b₁ + 4 * b₂ + ... + 4 * b_{m-1} + 2 * bₘ (and 0 for the empty list): the "tail" of S after the first entry. · Usa2026P2.innerSum

InSameArm def

b lies in the same arm of the cross as a (meaningful when a is not the center). · Usa2007P4.InSameArm

insertList abbrev

Inserting a fresh 2^0 weight at position k on pan b into a list of placements whose weights are all doubled. · Imo2011P4.insertList

insertZeroWays def

The valid sequence obtained by inserting the weight 2^0 according to the given insertion data. · Imo2011P4.insertZeroWays

inSub def

Membership in the downward sub-triangle with apex (p, q). · Imo2018P3.inSub

intCols def

The interior cells (rows < n) in columns 1..i. · Usa2019P4.intCols

interiorPartialSums def

def interiorPartialSums (l : List ℝ) : List ℝ · Imo2026P3.interiorPartialSums

InteriorRow abbrev

A row that is neither the first nor the last (and thus contains a monster). · Imo2024P5.InteriorRow

interiorVerts def

The vertices that a walk visits at an interior position: all w.getVert (i + 1) with i + 1 < w.length. At each such vertex two consecutive edges of the walk meet. · Imo1991P4.interiorVerts

interPt def

The intersection point of two non-parallel lines. · Imo2014P6.Line.interPt

IntersectionSetup structure

structure IntersectionSetup (n : ℕ) [NeZero n] extends BaseSetup n · Imo2025P6.IntersectionSetup

intervalBlock def

def intervalBlock {N : ℕ} (r : ℕ → ℝ) (f : ℕ → ℕ) (i : Fin N) : List ℝ · Imo2026P3.intervalBlock

Inv def

The invariant maintained after each move of the second player: a threat-free board with a trap and no SOS, with the right parity of empty squares (t = true: first player to move). · Usa1999P5.Inv

Inv def

The invariant Bob maintains after each of his moves. · Usa2004P4.Inv

invariant def

The invariant of the game: the weighted sum of the values, where the value at vertex i has weight i. A turn changes it by a multiple of 5. · Usa2011P2.invariant

invPair def

The A-inversion relation on a pair of entries: x is the left entry (at position i, with threshold c = a_i) and y is the right entry. · Usa2017P2.invPair

InX inductive

The set X of the problem, as an inductive predicate: it is the smallest set of polynomials that contains the identity polynomial X and is closed under the two operations r ↦ X * r and r ↦ X + (1 - X) * r. · Usa1987P3.InX

is_good_seq def

def is_good_seq {n : ℕ} (s : DigitSeq n) · Usa1972P3.is_good_seq

is_power_of_two def

def is_power_of_two (n : ℤ) : Prop · Imo2015P2.is_power_of_two

is_solitary def

def is_solitary (n : ℕ) : Prop · Usa2026P4.is_solitary

is_sum_of_pos_squares def

$z$ can be written as the sum of $k$ positive squares. · Imo1992P6.is_sum_of_pos_squares

is_valid abbrev

abbrev is_valid (x : ℕ → ℤ) (y z : ℤ) : Prop · Usa1985P1.is_valid

is_valid_c def

def is_valid_c (c : ℝ) : Prop · is_valid_c

IsAcuteTriple def

Three real numbers are the side lengths of an acute triangle iff the strict triangle inequalities hold and the sum of the squares of any two of them is strictly greater than the square of the third one. · Usa2012P1.IsAcuteTriple

IsAdmissible def

def IsAdmissible (n : ℕ) (T : Finset Plane) : Prop · Imo2007P6.IsAdmissible

IsAdmissible def

The two-sided inequality defining admissible functions on positive real numbers. · Imo2026P5.IsAdmissible

IsAnimal structure

An animal is a nonempty finite set of cells whose induced subgraph of the grid graph is connected. · Usa2007P4.IsAnimal

IsAntiChain def

def IsAntiChain (s : Finset (Point n)) : Prop · Imo2025P6.IsAntiChain

IsArithProg def

A sequence f : ℕ → ℕ is an arithmetic progression. · Imo2009P3.IsArithProg

IsBlack def

A cell is black if it contains the greatest number in its row. · Usa2004P4.IsBlack

IsBlock def

A block that can be torn out of the n×n sheet. · Usa2002P6.IsBlock

IsChain def

def IsChain (s : Finset (Point n)) : Prop · Imo2025P6.IsChain

isConstant def

def isConstant {R : Type*} [Semiring R] (p : R[X]) : Prop · Imo1993P1.isConstant

IsCut def

One admissible cut of the triangle s, producing children L and R. · Imo2026P4.IsCut

IsDinoPartition def

parts is a partition of the animal d into two or more dinosaurs: at least two pairwise disjoint dinosaurs whose union is d. · Usa2007P4.IsDinoPartition

IsDinosaur def

A dinosaur is an animal with at least 2007 cells. · Usa2007P4.IsDinosaur

IsGood def

def IsGood (x A : ℝ) : Prop · Imo1959P2.IsGood

IsGood structure

The predicate says that x satisfies the inequality · Imo1960Q2.IsGood

IsGood structure

structure IsGood (f : ℝ≥0 → ℝ≥0) : Prop · Imo1986P5.IsGood

IsGood def

Label the points by ZMod (2 * n - 1). A set B of black points is good if it contains two points x and y with y - x = n + 1 or x - y = n + 1, which is exactly the condition that one of the two arcs between them contains n … · Imo1990P2.IsGood

IsGood abbrev

abbrev IsGood (a b c d e : ℝ) : Prop · Usa1978P1.IsGood

IsGood abbrev

A set of integers is called good if it does not contain three elements a, b, c (not necessarily distinct) satisfying a + b + c = 0. · Usa2009P2.IsGood

IsGood def

The property of n that the problem asks to characterize: among any n positive real numbers whose maximum is at most n times their minimum (here expressed as a i ≤ n * a j for all indices i j), some three are the side lengths of … · Usa2012P1.IsGood

IsHook def

A hook is a translate of one of the eight orientations. · Imo2004P3.IsHook

IsIndependentPoint def

Condition for a set of points to be "independent" (pairwise distance > 2). This matches the sw condition. · Imo1999P3.IsIndependentPoint

IsInitial def

An initial board: exactly 2026 entries, each strictly greater than 1. · Imo2026P1.IsInitial

IsInt def

The predicate that a rational number is an integer. · Usa2009P6.IsInt

IsLosing def

A losing square: an empty square such that playing either letter there allows the opponent to win on the following move. · Usa1999P5.IsLosing

IsMaximalTearing def

A tearing-out of pairwise disjoint blocks from the n×n sheet which makes it impossible to tear out any more blocks. · Usa2002P6.IsMaximalTearing

IsMaxProd def

def IsMaxProd (n₀ : ℕ) · Imo1976P4.IsMaxProd

IsMaxProdSet def

def IsMaxProdSet (s : Multiset ℕ) · Imo1976P4.IsMaxProdSet

IsMinMatildaCount def

def IsMinMatildaCount (n : ℕ) [NeZero n] (m : ℕ) : Prop · Imo2025P6.IsMinMatildaCount

IsMove def

A single move: the piece at c jumps over the adjacent piece at c + d onto the empty square c + d + d; the jumped-over piece is removed. · Imo1993P3.IsMove

IsPacking structure

A packing of the a × b × c box by cubes of volume 2 (side k = ∛2), with edges parallel to the edges of the box: a finite set of cube positions inside the box, pairwise non-overlapping. · Imo1976P3.IsPacking

IsPow2 def

A positive integer which is a power of two (in particular 1 = 2 ^ 0 counts). · Usa2026P2.IsPow2

IsPrimitive def

A dinosaur is primitive if its cells cannot be partitioned into two or more dinosaurs. · Usa2007P4.IsPrimitive

IsProductOfkDistinctMembers def

def IsProductOfkDistinctMembers (x : ℕ) (k : ℕ) (S : Set ℕ) : Prop · Imo1994P6.IsProductOfkDistinctMembers

IsSolution abbrev

abbrev IsSolution (a b x y z : ℝ) : Prop · Imo1961P1.IsSolution

IsSolution def

def IsSolution (n : ℕ) : Prop · Imo2012P6.IsSolution

IsSolution abbrev

The property that the integers A, B, C, a, b, c solve the problem for the real cube root k of 2: the rational function (Ax² + Bx + C)/(ax² + bx + c) approximates k strictly better than x does, for every non-negative rational … · Usa1972P4.IsSolution

IsSolution def

The conditions of the problem on a function f : ℕ → ℕ. Since the problem is about functions on the positive integers, we require positivity of f on positive inputs explicitly; the value f 0 is irrelevant. · Usa2012P4.IsSolution

IsStable def

A set S of positive integers is k-stable if the sum of the elements of any nonempty subset X ⊆ S has digit sum equal to k. · Usa2005P6.IsStable

isSw def

Helper predicate for the internal logic of the construction. We divide the grid based on parity and modulo 4 conditions. · Imo1999P3.isSw

IsSwitch def

A switching involution on a vertex σ: an involution φ supported on the numerators of σ which preserves labels. · Usa2018P6.IsSwitch

IsTerminal def

A board is terminal when at most one entry is > 1, so no move is possible. · Imo2026P1.IsTerminal

isTerminalWalk def

def isTerminalWalk {V : Type} {G : SimpleGraph V} {u v : V} (w : G.Walk u v) · Imo1979P6.isTerminalWalk

isTerminalWalk_length_cons_equiv def

def isTerminalWalk_length_cons_equiv {V : Type} {G : SimpleGraph V} {u t : V} (m n : ℕ) (npos : 0 < n) : {w : G.Walk u t // isTerminalWalk w ∧ w.length = m+n} ≃ Σ (v:V), {w : G.Walk u v // t ∉ … · Imo1979P6.isTerminalWalk_length_cons_equiv

IsTile def

A tile is a translate of one of the six tile shapes. · Imo2004P3.IsTile

isTree def

Whether a cell of the board is a tree cell of the construction. · Imo2022P6.isTree

isTreeJ def

Whether a cell with pattern-column residue jm6 = j % 6 and row r is a tree cell of the construction (its complement are the hills). · Imo2022P6.isTreeJ

IsTriangle def

A triangle, viewed as the multiset of its three interior angles (in degrees): positive reals summing to 180. · Imo2026P4.IsTriangle

IsUniversal def

A vertex is universal if it is joined to all 1981 other vertices. · Usa1982P1.IsUniversal

IsValid def

A collection of plates is valid if any two distinct plates in it differ in at least two places. · Usa1990P1.IsValid

IsValid def

A coloring is valid if it satisfies the multiplicative condition of the problem. · Usa2015P3.IsValid

IsValid def

The property from the problem statement: S is a finite set of positive integers such that for every s ∈ S and every positive divisor d of s there exists a unique t ∈ S with Nat.gcd s t = d. · Usa2021P4.IsValid

IsValidConfiguration def

def IsValidConfiguration (n : ℕ) [NeZero n] (all_black : Finset (Point n)) (partition : Finset (Matilda n all_black)) : Prop · Imo2025P6.IsValidConfiguration

IsValidMarking def

A set s is a valid marking if every square in the grid is adjacent to some square in s. · Imo1999P3.IsValidMarking

isValidRow def

def isValidRow (l : List Coin) · Imo2022P1.isValidRow

IsValidSeq def

The predicate stating that a : ℕ → ℕ (0-indexed) is a sequence satisfying Definition 1: each term exceeds 1, and each subsequent term is the smallest integer strictly larger than the previous one that shares a common factor with every … · Imo2026P6.IsValidSeq

IsVertex def

A vertex is an involution with at most one fixed point (equivalently, a maximal matching of the complete graph). · Usa2018P6.IsVertex

IsWalk inductive

A walk in a pseudograph: the vertex list has one more entry than the edge list. · Imo2020P3.IsWalk

isWhite def

The white squares of the chessboard are those whose coordinates have even sum. · Imo1974P4.isWhite

iterFac def

Iterated factorials starting at 3: iterFac 0 = 3 and iterFac (r + 1) = (iterFac r)!. These are used to produce arbitrarily large fixed points of f (Shankar Padmanabhan's argument). · Usa2012P4.iterFac

IV inductive

IV a b l holds when l is a list of natural numbers whose set of entries is exactly the interval [a, b], built by starting from a single digit and repeatedly prepending a new minimum or a new maximum. These are essentially the valid … · Usa1990P4.IV

IVSet def

Lists whose digits form exactly the interval [a, b]. · Usa1990P4.IVSet

J

JapaneseTriangle structure

structure JapaneseTriangle (n : ℕ) · Imo2023P5.JapaneseTriangle

JudgePair abbrev

An ordered pair of judges. · Imo1998P2.JudgePair

judgePair abbrev

The ordered pair of judges from the triple consisting of a contestant and an ordered pair of judges. · Imo1998P2.AgreedTriple.judgePair

judge₁ abbrev

The first judge from an ordered pair of judges. · Imo1998P2.JudgePair.judge₁

judge₂ abbrev

The second judge from an ordered pair of judges. · Imo1998P2.JudgePair.judge₂

K

K def

The set of positive integers whose decimal representation does not contain the digit 7. · Usa2019P3.K

k def

The side length of a cube of volume 2: the real cube root of 2. · Imo1976P3.k

k def

The largest number to appear infinitely often. · Imo2024P3.Condition.k

K' def

The second point on line AX with BC = BK'. · Imo2012P5.Imo2012P5Cfg.K'

K'_set def

def K'_set · Imo2023P2.Imo2023q2Cfg.K'_set

K_set def

def K_set · Imo2023P2.Imo2023q2Cfg.K_set

kE def

enumeration of the absolute values · Usa2010P6.kE

keyFn def

The key function of the construction: tree cells come first (in strip order), then the hills (in column-major order). · Imo2022P6.keyFn

KnightAdj def

Two sites are at distance √5 iff they are a knight's move apart, i.e. their coordinate differences are (±1, ±2) or (±2, ±1). · Imo2018P4.KnightAdj

kseq def

Define the two main sequences · Usa2008P1.kseq

L

L def

One full round of the process: L x p = x last + ∑_{i ≤ p} x i in ZMod 2. · Imo1993P6.L

L def

def L · Imo2014P4.Imo2014q4Cfg.L

L def

L(A,B): Liu Bang's total length, given Liu Bang's marks A and Xiang Yu's marks B. · Imo2026P3.L

l def

The largest number to appear more than k times. · Imo2024P3.Condition.l

L' def

The second point on line BX with AC = AL'. · Imo2012P5.Imo2012P5Cfg.L'

L0 def

The extremal board: five loops (i,i) for each i ∈ {1,…,8} and one negative edge (-i,-j) for each 1 ≤ j < i ≤ 8 (a K₈ on the negative side). · Usa2010P6.L0

lab def

The label (0–3) of a cell within its 4×4 block, from the pattern 1 2 3 4 3 4 1 2 2 1 4 3 4 3 2 1 (read with 1-indexed labels in the official solution). · Imo2018P4.lab

Label structure

structure Label (n : ℕ) · Imo2025P6.Label

label def

def label : ℕ → ℤ × ℤ → ℕ · Usa2017P5.label

label def

The label of the edge {k, σ k} as seen from its smaller endpoint k: the rational (k+1)/(σ k + 1). · Usa2018P6.label

label_pos def

def label_pos (l : Label n) : Point n × Point n · Imo2025P6.label_pos

labelAt def

The label the player can deduce at position i, computed from observations i and i + 1 (junk value 0 when those observations are not available). · Usa2016P6.labelAt

labelling def

def labelling (c : ℝ) · Usa2017P5.labelling

LabelType inductive

inductive LabelType · Imo2025P6.LabelType

labelWeight def

def labelWeight [DecidableEq ι] (l : List (ℝ × ι)) (v : ι) : ℝ · Imo2026P3.labelWeight

lampsAfter abbrev

The lamp states after t steps of the process. · Imo1993P6.lampsAfter

lap def

The Laplacian of the friendship graph as a ZMod 2-linear map: (lap G x) v = deg(v) * x v + ∑_{u ∼ v} x u. · Usa2008P6.lap

large_n def

A sufficiently large value of n, congruent to -1 mod φ (a * b + 1). · Imo2024P2.Condition.large_n

large_n_0 def

A sufficiently large value of n, congruent to 0 mod φ (a * b + 1). · Imo2024P2.Condition.large_n_0

last abbrev

abbrev last : singularities · Imo1988P4.last

last_divides_lcm_remaining def

def last_divides_lcm_remaining (n k : ℕ) : Prop · Imo1981P4.last_divides_lcm_remaining

lasti def

The last index of Fin n. · Imo1993P6.lasti

lastTwo def

The last two cells of an uphill path, as a pair (second-to-last, last), with junk value for the second-to-last cell if the path has length 1. · Imo2022P6.UphillPath.lastTwo

latinSquare def

def latinSquare {n : ℕ} (v : Fin n → ℕ) : Fin n → Fin n → ℕ · Imo1997P4.latinSquare

ldsLength def

def ldsLength (f : Fin n → Fin n) : ℕ · Imo2025P6.ldsLength

leanJs def

def leanJs : Asset · Assets.leanJs

leanName def

def leanName (p : ProblemInfo C) : Lean.Name · ProblemInfo.leanName

left_child def

def left_child (c : Coords) : Coords · Imo2018P3.left_child

leftmost def

The position of the leftmost flea. · Imo2000P3.leftmost

leftmostNSame def

The property of a row having leftmost n coin with the same type. · Imo2022P1.Row.leftmostNSame

leftVertex abbrev

abbrev leftVertex (A : ZMod 3 → Point) (i : Fin 7) : Point · Usa2000P5.leftVertex

Legal def

A sequence of permitted switches starting from configuration e. · Usa2010P2.Legal

Letter abbrev

The three letters I, M, O. · Imo2016P2.Letter

letters def

The occupied squares of the board. · Usa1999P5.letters

lhs def

The tuple of left-hand sides of the equations, as a function of the tuple of unknowns. · Imo1976P5.lhs

lhsFinset def

The possible values of the tuple of left-hand sides: each coordinate is an integer between -2n² and 2n². · Imo1976P5.lhsFinset

li def

def li (attrs : List Attr · Html.li

lift def

Extend a placement g : Fin 100 → ZMod 3 to all of ℕ (by 0 outside [1, 100]); card a corresponds to index a - 1. · Imo2000P4.lift

Line structure

A line in the plane ℝ × ℝ, given by the equation a * x + b * y + c = 0 with (a, b) ≠ (0, 0). · Imo2014P6.Line

line def

The "line" ax + by + c = 0. ("line" means except for the degenerate case a = 0 ∧ b = 0) Note: We don't enforce a ≠ 0 ∨ b ≠ 0. · Imo2025P1.line

line' def

Build a line from a LineCoeffs · Imo2025P1.line'

linear def

The linear form α * x + β * y. · Imo2017P6.HForm.linear

LineCoeffs structure

The coeffecients of a line a * x + b * y + c = 0 · Imo2025P1.LineCoeffs

linexy0 def

The line `x+y=0`, as an affine subspace. · Imo2025P1.linexy0

Link inductive

The three possible link types between two towns. · Usa1981P2.Link

link def

def link (attrs : List Attr) · Html.link

linkage structure

A linkage between two stations. · Imo2020P4.Company.linkage

Linked inductive

Linked a b means that a can be connected to b by a finite chain of positive integers in which any two consecutive terms x, y satisfy x + y ∣ x * y. · Usa2002P5.Linked

linked def

The property of two stations being linked (in the given order). · Imo2020P4.Company.linked

lisLength def

def lisLength (f : Fin n → Fin n) : ℕ · Imo2025P6.lisLength

listOfBlocks def

def listOfBlocks (l : List ℕ) (head : Coin) : List Coin · Imo2022P1.listOfBlocks

liveLean def

def liveLean (config : SConfig) (p : ProblemInfo C) (proved : Bool) : List Html · liveLean

liveLeanForName def

def liveLeanForName (config : SConfig) (name : Lean.Name) (proved : Bool) : List Html · liveLeanForName

lo def

The lower-left corner of the bounding box of a set of cells. · Imo2004P3.lo

loser def

The child of x holding the smaller value. · Imo2018P3.loser

losers def

The smaller children dropped along the apex path (the "losers"). · Imo2018P3.losers

losing def

The losing squares of the board. · Usa1999P5.losing

lowBit def

def lowBit (d : Fin 4) : Fin 2 · Usa1996P6.lowBit

lower_intervals def

def lower_intervals : Set (Set ℝ) · UpperLowerContinuous.lower_intervals

lowerCfg def

The Colombian configuration witnessing the lower bound: the vertices of a regular 4027-gon, colored red at odd indices and blue at even indices. · Imo2013P2.lowerCfg

lowerFill def

def lowerFill : ℕ → Signature → ℕ · Usa2024P2.lowerFill

lows def

The lines whose constraint is a lower bound on the parameter along ℓ. · Imo2014P6.lows

lvl def

The level of n: for n ≥ 1 this is the unique ℓ ≥ 1 with 2^(ℓ-1) ≤ n < 2^ℓ. · Usa2022P5.lvl

M

M abbrev

abbrev M : Polynomial ℝ · Imo1988P4.M

M def

def M · Imo2023P2.Imo2023q2Cfg.M

M def

A number greater than any of the initial terms a 0 through a N (otherwise arbitrary). · Imo2024P3.M

m def

def m (_:ℕ) : ℕ → ℕ · Imo1973P6.m

M' abbrev

abbrev M' (n : singularities) : Polynomial ℝ · Imo1988P4.M'

M_st def

def M_st (s t : Int) : Finset (Point n) · Imo2025P6.M_st

main_ def

def main_ (attrs : List Attr · Html.main_

mainCss def

def mainCss : Asset · Assets.mainCss

mainEquiv def

The valid colorings are in bijection with the parameters. · Usa2015P3.mainEquiv

maintSeq def

Running one maintenance round: the rabbit runs directly away from the hunter and the device reports the rabbit's position honestly. · Imo2017P3.maintSeq

make_b_point def

def make_b_point (s t : Int) (h_bounds : let b · Imo2025P6.make_b_point

makePlot def

def makePlot (n : ℕ) (npos : 0 < n) : NicePlotOfP n npos · Imo1976P2.makePlot

map_mod def

def map_mod (n : ℕ) (hn : 0 < n) (f : ℕ → ℕ) : ℕ → Fin n · ZerosOnesAndTwos.map_mod

maskedCell def

def maskedCell (p : Prop) [Decidable p] (f : coloring) (x y : ℕ) : ZMod 2 · Usa1998P4.maskedCell

mate def

The pairing of the cells of the first two rows: the cell (0, j) is paired with (1, colMate j) and vice versa; all other cells are paired with themselves. Paired cells are in different rows and three columns apart, so they do not even … · Usa2004P4.mate

Matilda structure

structure Matilda (n : ℕ) [NeZero n] (all_black : Finset (Point n)) · Imo2025P6.Matilda

maxCliqueCard def

The largest size of a clique of the graph G all of whose vertices lie in A. · Imo2007P3.maxCliqueCard

maxD def

The maximum of a set of naturals, defaulting to 0 for the empty set. · Usa1975P5.maxD

maxDecSequencesTo def

def maxDecSequencesTo (f : α → β) (i : α) : ℕ · Imo2025P6.maxDecSequencesTo

maxIncSequencesTo def

def maxIncSequencesTo (f : α → β) (i : α) : ℕ · Imo2025P6.maxIncSequencesTo

maxNumCubes def

The maximal number of cubes of volume 2 that can be placed in the a × b × c box with edges parallel to the edges of the box: along an edge of integer length n exactly ⌊n / k⌋₊ cubes fit. That this is indeed the maximum is proved in … · Imo1976P3.maxNumCubes

Mc def

def Mc (A H C : EuclideanSpace ℝ (Fin 2)) : EuclideanSpace ℝ (Fin 2) · Usamo2025P4.Mc

meas def

The measure of a configuration: twice the sum of the 1-based positions of the heads minus the square of the number of heads. We will show that this is a nonnegative integer (see meas_nonneg) which drops by exactly one at each step (see … · Imo2019P5.meas

MedalsProcess abbrev

The process described in the problem, from the point of view of the medals remaining: r k is the number of medals left at the start of day k + 1 (so r 0 = m). On day k (for 1 ≤ k ≤ n - 1), k medals and one seventh of the rest … · Imo1967P6.MedalsProcess

Medium def

Medium numbers are those that are more than k but at most l (and include all numbers appearing finitely often but more than k times). · Imo2024P3.Condition.Medium

mem def

def Matilda.mem (m : Matilda n all_black) (p : Point n) : Prop · Imo2025P6.Matilda.mem

members_of abbrev

abbrev members_of (i : Fin N) : Finset (@Name M) · Imo1978P6.members_of

mergeNeighbors def

def mergeNeighbors (c : Contest idx subIdx) : List <| idx × List subIdx · Contest.mergeNeighbors

meta_ def

def meta_ (attrs : List Attr) · Html.meta_

mid def

The middle element of a 3-element set of natural numbers, computed as the sum minus the minimum minus the maximum. When S is the set of ace positions, this is the number of cards turned over to reach the second ace. · Usa1975P5.mid

midWindow def

The k - 1 positions strictly between i and i + k (the empty set if they do not fit). · Usa2016P6.midWindow

minCell def

The cell with value 1. · Imo2022P6.NordicSquare.minCell

minD def

The minimum of a set of naturals, defaulting to 0 for the empty set. · Usa1975P5.minD

minEndpoint def

The smaller endpoint of an edge, well-defined since min is symmetric. · Imo1992P3.minEndpoint

minJumps def

The minimum number of jumps the frog needs to reach position m. · Usa2006P5.minJumps

mirror def

def Octagon.mirror : Octagon ≃g Octagon · Imo1979P6.Octagon.mirror

mirror def

The point reflection swapping the two distinguished cells x₀ = (1, 0) and y₀ = (4, 0) of the strategy below. · Usa2014P4.mirror

mixedRel def

mixedRel n G X p says that the vertex X is distinct from the two endpoints of the pair p and is adjacent to exactly one of them. · Usa1985P4.mixedRel

mk def

def msos.mk (L : List (ℕ × ℕ+)) : Multiset ℕ+ · Imo1992P6.msos.mk

mk_mul_hom_fun def

def PNat.mk_mul_hom_fun {R : Type} [CommMonoid R] (g : ℕ → R) : ℕ+ →ₙ* R · Imo1990P4.PNat.mk_mul_hom_fun

mk_mul_hom_fun def

def PRat.mk_mul_hom_fun (g : ℕ → ℚ+) : ℚ+ →* ℚ+ · Imo1990P4.PRat.mk_mul_hom_fun

mkColor def

A symmetric link assignment on five towns, reconstructed from its restriction to the ten unordered pairs. · Usa1981P2.mkColor

mkU def

Bundle ten link types into a function Fin 10 → Link. · Usa1981P2.mkU

Mod3 def

The mod-3 placements: the box of card a depends only on a % 3. · Imo2000P4.Mod3

mod3fun def

The mod-3 placements of the 100 cards. · Imo2000P4.mod3fun

mod4_cycle def

def mod4_cycle : Set (ℤ → ℤ) · Imo2012P4.mod4_cycle

mod_base abbrev

abbrev mod_base : ℤ · Imo2025P6.mod_base

MODTable def

The coloring f of the n × n table satisfies all the required conditions: every row and column is balanced, and every diagonal whose length is a multiple of three is balanced. · Imo2016P2.MODTable

monoE def

Boolean check: is the triangle with these three link types monochromatic? · Usa1981P2.monoE

monoTriples def

The monochromatic pairs of rows in column j, tagged with their color: (r1, r2, b) means r1 < r2 and both squares (r1, j) and (r2, j) have color b. · Usa1976P1.monoTriples

monsterCells def

The cells with monsters as a Set, given an injection from rows to columns. · Imo2024P5.MonsterData.monsterCells

MonsterData abbrev

Data for valid positions of the monsters. · Imo2024P5.MonsterData

monsterData12 def

Positions for monsters with specified columns in the second and third rows (rows 1 and 2). · Imo2024P5.monsterData12

motive def

def motive (Cdone : Finset (Fin N)) (k : ℕ) : Prop · Imo1978P6.motive

motive' def

def motive' (n : ℕ) (k : ℕ) : Prop · Imo1978P6.motive'

Move abbrev

A permitted move between two squares: both lie on the board and the squared distance between their centers equals r. · Imo1996P1.Move

Move def

A single move with jump ratio lam: flea i, sitting at some point A = x i, jumps over flea j at B = x j (with A to the left of B) and lands at the point C = B + lam * (B - A), so that BC / AB = lam. All other fleas stay … · Imo2000P3.Move

Move inductive

A move of player B: either stop and guess a set X, or ask whether x ∈ S. · Imo2012P3.Move

Move def

A single move: pick two entries m, n (from two distinct positions, modelled as two separate elements of the multiset) both > 1, remove them and insert gcd(m, n) and lcm(m, n) / gcd(m, n). Using m ::ₘ n ::ₘ s for the source … · Imo2026P1.Move

Move def

An allowed move: change the value at some index n to another value v that differs from both neighbors. · Usa1994P2.Move

Move inductive

One legal turn of the game: the two adjacent entries x and y are erased and replaced by a power of two z which is strictly larger than both of them. · Usa2026P2.Move

move def

The operation performed at vertex i when s i < 0. · Imo1986P3.move

move def

A single move, on a pair of position and move number. · Imo2021P5.move

move def

def List.move {α : Type u} (a b : ℕ): List α → List α · Imo2022P1.List.move

move def

Move coins a through b to the left of the row. · Imo2022P1.Row.move

Moves def

Moves f g means that configuration g can be reached from f by a sequence of moves. · Usa2003P6.Moves

Moves structure

A choice of lines to flip: for each of the three directions and each i < n, whether the i-th line in that direction is flipped. The three lines through the token (a, b, c) are the a-th, b-th and c-th lines of the three … · Usa2013P3.Moves

MSequence abbrev

abbrev MSequence (n k : ℕ) (f : Sequence n k) : Prop · Imo2008P5.MSequence

mul def

Multiplication of homogeneous forms (degrees add). · Imo2017P6.HForm.mul

MulanCanGuarantee def

Mulan can guarantee victory for the value θ: from every valid starting triangle she wins in finitely many steps regardless of Shan-Yu's play. · Imo2026P4.MulanCanGuarantee

MulanWins inductive

The set of triangles from which Mulan can force, in finitely many steps, a triangle with an interior angle equal to θ, no matter how Shan-Yu discards. · Imo2026P4.MulanWins

mulSeq def

A completely multiplicative sequence built from values assigned on a finite set of primes: mulSeq P c j = ∏ r ∈ P, c r ^ (Nat.factorization j r). · Usa2012P3.mulSeq

mult def

The multiplicity of vertex x as an endpoint of edge e. · Imo2020P3.mult

MultisetNatOfLen14 structure

A type representing assignments to the variables $n_1$, $n_2$, ..., $n_{14}$, quotiented by permutations of indices. · Usa1979P1.MultisetNatOfLen14

Mval def

The claimed invariant terminal value M = ∏_{p ∣ ∏ B} p ^ gExp p B, the product over all primes dividing some entry of B of p raised to the gcd of the p-adic valuations. · Imo2026P1.Mval

N

N def

The value of N in the problem (any sufficiently large value). · Imo2024P2.Condition.N

n def

def n : ℕ · Imo1989P1.n

N' def

N' is such that, by position N', every medium number has made all its appearances and every small number has appeared more than max(k, N+1) times; furthermore, a N' is small (which means that every subsequent big number is preceded … · Imo2024P3.Condition.N'

N'aux def

N'aux is such that, by position N'aux, every medium number has made all its appearances and every small number has appeared more than max(k, N+1) times. · Imo2024P3.Condition.N'aux

Name abbrev

abbrev Name : Type · Imo1978P6.Name

NatPredicate def

It will be convenient to have the lemmas above in their natural number form. Most of these can be proved with the `norm_cast` family of tactics. · Imo1981P3.NatPredicate

nav def

def nav (attrs : List Attr · Html.nav

navbar def

def navbar (config : SConfig) (currentPage : NavbarState) : List Html · navbar

NavbarState inductive

inductive NavbarState · NavbarState

nb def

The nearest available blue point to r, going counterclockwise from r (if one exists; otherwise, arbitrarily, r itself). · Usa2017P4.nb

NC def

Abbreviation for the noncollinearity hypothesis on a triple of points. · Imo1970P6.NC

Necklace abbrev

A circular necklace with m * n beads, each red (true) or blue (false). The beads are indexed by their position on the circle, i.e. by ZMod (m * n). · Usa2024P4.Necklace

neg def

Negation of a form. · Imo2017P6.HForm.neg

negFourValue def

def negFourValue {b : ℕ} (digits : List (Fin b)) : ℤ · Usa1996P6.negFourValue

neighborCols def

Columns containing a good cell in one of the rows in R. · Usa2022P1.neighborCols

neighbors4 def

The explicit four-element finset of neighbours of a cell. · Usa2007P4.neighbors4

neqAfter def

The set of positions j > i with a j ≠ a i. · Usa1987P5.neqAfter

newSwitch def

The new switching involution: the product of the swaps (x, σ x) over the representatives. · Usa2018P6.newSwitch

next_row def

def next_row {n} (i : Finset.Icc 1 n) (h : i.val + 1 ≤ n) : Finset.Icc 1 n · Imo2023P5.next_row

nextA def

The effect of one doubling step p(x) ↦ p(x) p(-x) on the exponents: if p = ∏ (1 - X^i) ^ (a i) then p(x) p(-x) = q(x²) where q = ∏ (1 - X^i) ^ (nextA a i). · Usa1988P5.nextA

nextD def

The successor of x in the circle with D deleted. · Usa2025P6.CirclePartition.nextD

Nice def

Digit lists (little-endian) whose entry at each position has the parity of the position, so that consecutive digits have different parity. · Imo2004P6.Nice

NicePlotOfP structure

structure NicePlotOfP (n : ℕ) (npos : 0 < n) · Imo1976P2.NicePlotOfP

NinjaPath structure

structure NinjaPath (n : ℕ) · Imo2023P5.NinjaPath

No3Col def

def No3Col (S : Finset Pt) : Prop · Imo2013P2.No3Col

no_eval def

Wrapper to prevent the Lean kernel from eagerly trying to normalize the solution value, which happens to be way too large to normalize. · Imo1981P6.no_eval

NoEven abbrev

abbrev NoEven {n : ℕ} (s : DigitSeq n) : Prop · Usa1972P3.NoEven

NoFive abbrev

abbrev NoFive {n : ℕ} (s : DigitSeq n) : Prop · Usa1972P3.NoFive

NonOverlapping abbrev

Two cubes of side k placed at p and q do not overlap: their interiors are disjoint, i.e. they are separated along at least one axis. · Imo1976P3.NonOverlapping

NordicSquare abbrev

A Nordic square. · Imo2022P6.NordicSquare

normalizeSignature def

Push v down to its canonical high-rank residue. · Usa2024P2.normalizeSignature

NR def

Number of rows. · Imo2018P3.NR

NSequence abbrev

abbrev NSequence (n k : ℕ) (f : Sequence n k) : Prop · Imo2008P5.NSequence

nsOf def

The constructed Nordic square: values are positions in the key order plus one. · Imo2022P6.nsOf

nsOfIso def

The order isomorphism between all cells (with the key order) and Fin (m ^ 2). · Imo2022P6.nsOfIso

nth def

The position after n moves. · Imo2021P5.Position.nth

nth_smallest def

def nth_smallest {n : ℕ} {a : Fin n → ℝ} (ha : Function.Injective a) : Fin n → ℝ · Imo1966P5.nth_smallest

nth_smallest_index def

def nth_smallest_index {n : ℕ} {a : Fin n → ℝ} (ha : Function.Injective a) : Fin n → Fin n · Imo1966P5.nth_smallest_index

nthDiv def

The i-th smallest positive divisor of n (meaningful for i < n.divisors.card). · Imo2002P4.nthDiv

nu def

The exponent of the largest power of 2 dividing the integer x (the 2-adic valuation of x). · Usa2006P5.nu

numberOfEntries def

The set of all possible numbers of times the visitor could have entered a junction during her walk, over all parks and all choices of starting junction and first trail. · Usa2021P2.numberOfEntries

numGoodTriples def

The quantity T from the problem statement: the number of triples of indices i < j < k whose values are not (0, 1, 0) or (1, 0, 1). · Usa1987P5.numGoodTriples

numHeads def

The number of coins showing heads in a configuration of n coins. A configuration is a function Fin n → Bool, where c i = true means that the i-th coin from the left (starting the count at 0) shows heads. · Imo2019P5.numHeads

numPartitions abbrev

The number of partitions of n. · Usa1986P5.numPartitions

nums def

The numerators of an involution: positions sent to a strictly larger value. · Usa2018P6.nums

nV def

number of distinct absolute values · Usa2010P6.nV

O

O def

def O :EuclideanSpace ℝ (Fin 2) · Imo2001P1.Imo2001q1Cfg.O

O abbrev

abbrev O (A B C : P) (hABC : AffineIndependent ℝ ![A, B, C]) : P · Usa1988P4.O

o def

o P is the number of nonzero coefficients of a polynomial P over ZMod 2. · Imo1985P3.o

Objective def

def Objective (x : Fin 4 → ℝ) : ℝ · Usa2014P1.Objective

Observation abbrev

An observation made by the player: the set of queried positions, together with the labels that were revealed (none outside the queried set). · Usa2016P6.Observation

obsValues def

The labels revealed in an observation on a given set of positions. · Usa2016P6.obsValues

Ocard def

Number of odd-length lines in one direction. · Usa2013P3.Ocard

OccursDen def

def OccursDen (x : ℝ) (n d : ℕ) : Prop · Usa1983P5.OccursDen

Octagon abbrev

abbrev Octagon · Imo1979P6.Octagon

odd_const def

def odd_const : Set (ℤ → ℤ) · Imo2012P4.odd_const

oddCount def

The number of odd coefficients of a polynomial with integer coefficients. · Imo1985P3.oddCount

oddPart def

def oddPart (a : ℕ) : ℕ · Usa1983P5.oddPart

of def

The identity map from cells to ordered cells. · Imo2022P6.OrderedCell.of

ofBlocks def

def Row.ofBlocks {n : ℕ} (l : List ℕ) (head : Coin) (hl : l.sum = 2 * n) : Row n · Imo2022P1.Row.ofBlocks

off def

The offset of arc i: total length of the preceding arcs. · Usa2025P6.CirclePartition.off

offA1 def

Offsets of the first circle when 13 ∤ n: [n, n+1, …, n+13]. · Usa1990P3.offA1

offA2 def

Offsets of the first circle when 13 ∣ n: [n+19, n+20, …, n+32]. · Usa1990P3.offA2

offB1a def

Offsets of the second circle when 13 ∤ n and n ≢ 2 [MOD 17]: [n+15, n+14, n+16, n+17, …, n+32]. · Usa1990P3.offB1a

offB1b def

Offsets of the second circle when 13 ∤ n and n ≡ 2 [MOD 17]: [n+14, n+15, …, n+30, n+32, n+31]. · Usa1990P3.offB1b

offB2a def

Offsets of the second circle when 13 ∣ n and n ≢ 16 [MOD 17]: [n+1, n, n+2, n+3, …, n+18]. · Usa1990P3.offB2a

offB2b def

Offsets of the second circle when 13 ∣ n and n ≡ 16 [MOD 17]: [n, n+1, …, n+16, n+18, n+17]. · Usa1990P3.offB2b

offExt def

Periodic extension of the offsets: the total length of the first a arcs (going around the circle repeatedly). · Usa2025P6.CirclePartition.offExt

officialImoUrl def

def officialImoUrl (year : Nat) (_idx : Nat) : String · officialImoUrl

ofFn def

Convert a function giving the cells of a path to a Path. · Imo2024P5.Path.ofFn

offsets def

The six unit steps between adjacent cells of the grid. · Usa2014P4.offsets

ogPreviewPng def

def ogPreviewPng : Asset · Assets.ogPreviewPng

OnBoard abbrev

The predicate that p is a square of the 20 × 12 board. · Imo1996P1.OnBoard

ones def

The number of 1s in the binary representation of n. · Imo1994P3.ones

ones def

def ones (b : ℕ) : ℕ → ℕ · ZerosOnesAndTwos.ones

oneSunny def

A strongCoverGridConfig with n = 1 and nS = 1 · Imo2025P1.oneSunny

op abbrev

abbrev op (f : S → S) (a b : S) : S · Imo1994P5.op

open_intervals def

def open_intervals : Set (Set ℝ) · UpperLowerContinuous.open_intervals

operation def

def List.operation {α : Type u} [DecidableEq α] (l : List α) (k : Fin l.length) : List α · Imo2022P1.List.operation

operation def

The operation moving the chain containing coin k (zero-based). · Imo2022P1.Row.operation

operationOneBased def

def List.operationOneBased {α : Type u} [DecidableEq α] (l : List α) {k : ℕ} (hk1 : 1 ≤ k) (hkn : k ≤ l.length): List α · Imo2022P1.List.operationOneBased

operationOneBased def

The operation moving the chain containing coin k (one-based). · Imo2022P1.Row.operationOneBased

opp def

The opposite site of a site in its 4-cycle: the two sites of the cycle that are not a knight's move apart. · Imo2018P4.opp

oppCoord def

The opposite coordinate within a 4×4 block: i ↦ 3 − i within the block. · Imo2018P4.oppCoord

optPlays def

The set of plays that achieve the lowest score. · Usa2000P3.optPlays

order def

def order {n : ℕ} (a : Fin n → ℝ) : Fin n → Fin n · Imo1966P5.order

OrderedCell def

The cell type equipped with the key order (a synonym to avoid instance clashes). · Imo2022P6.OrderedCell

Ordering abbrev

The cyclic order in which the six chosen points appear around the circle: σ i is the position of the i-th chosen point among the six positions 0, …, 5 listed in clockwise order. Only the cyclic order of the six points matters for … · Usa1983P1.Ordering

Others def

def Others · Imo2025P6.IntersectionSetup.Others

Outcome inductive

The outcome of a game: first player wins, second player wins, or draw. · Usa1999P5.Outcome

outsideIndices def

def outsideIndices (I J : Finset (Fin m)) : Finset (Fin m) · Imo2026P3.outsideIndices

Overdetermined def

A finite set of points in the coordinate plane is overdetermined if it has at least two elements and some nonzero real polynomial of degree at most |S| - 2 passes through every point of S. · Usa2020P5.Overdetermined