Winning Gold at IMO 2025 with a Model-Agnostic Verification-and-Refinement Pipeline

Benchmark context

• The IMO’s status is reinforced by its selectivity: gold medals go to only the top twelfth of contestants, and 11 of 34 Fields Medalists awarded since 1990 were prior IMO gold medalists.The competition includes over 100 countries and tests algebra, combinatorics, geometry, and number theory across two 4.5-hour sessions.Source: §1 · pp. 1–2

Motivation

• IMO problems combine extreme difficulty, complete proof requirements, and systematic novelty, making them a grand challenge for genuine mathematical reasoning rather than retrieval or pattern recognition.Unlike AIME’s final-answer format, IMO solutions must provide logically sound proofs, and recent evaluations found that leading models often commit fallacies or rely on superficial heuristics.Source: §1 · pp. 2–3

Positioning

• The natural-language approach produces human-readable proofs, complementing formal systems such as AlphaProof whose Lean-verified proofs guarantee correctness but can be verbose, cumbersome, and inaccessible to most mathematicians.The stated goal is to support human-AI collaboration by making AI reasoning understandable, critiqueable, and reusable.Source: §1 · p. 3

Main contribution and results

• 5 of 6 IMO 2025 problems were solved (approximately 85.7%), versus 31.6% for Gemini 2.5 Pro, 21.4% for Grok-4, and 38.1% for GPT-5 under best-of-32 baselines.The comparison indicates that verification and refinement convert existing models’ capabilities into rigorous mathematical proofs, with the IMO 2025 setting also mitigating contamination concerns.Source: §1 · p. 3

External validation

• 94.5% accuracy ranked the Gemini-based pipeline #3 among 434 IMC participants, compared with 57.7% and rank #92 for Gemini 2.5 Pro alone.This independent evaluation used the more knowledge-intensive 2025 International Mathematics Competition for University Students on a pristine dataset.Source: §1 · p. 4

Approach

• The pipeline is model-agnostic and inference-time, using carefully designed prompts and robust verification to iteratively refine natural-language solutions for Olympiad-level rigor and novelty.It builds on iterative refinement and mathematical verification research while addressing the known bottleneck of generating high-quality feedback.Source: §1 · p. 4

2.1 Pipeline

• The pipeline generates an initial solution, self-improves it, verifies it with a bug report, optionally reviews that report, corrects the solution, and accepts or rejects it.The procedure is run independently in parallel or serial until a correct solution is obtained or the model reports failure.Source: §2.1 · p. 4

2.2 Solver

• Step 2 adds another reasoning budget for review and continuation because models often exhaust their single-query budgets on difficult IMO problems, noticeably improving outputs.Gemini 2.5 Pro’s maximum of 32,768 thinking tokens is described as insufficient for a typical IMO problem, while Grok-4 and GPT-5 face similar constraints.Source: §2.2 · p. 5

2.3 Verifier

• The verifier classifies critical errors and major or minor justification gaps, then iterates bug-report review and correction until solutions robustly pass or are declined.Critical errors are seldom missed, but reported critical errors may be noncritical and some reported gaps may be trivial; repeated verification and review mitigate these mistakes, with acceptance requiring five successful verifier passes.Source: §2.3 · p. 6

3 Experiment Setup

• The setup uses low temperature for Gemini 2.5 Pro and Grok-4, maximum thinking for Gemini, high reasoning effort for GPT-5, and disables tools.GPT-5 temperature and Grok-4 reasoning effort cannot be adjusted; web search, code, and other tools are disabled.Source: §3 · p. 7

3.1 Solver Prompt

• The solver prompt requires complete, logically justified proofs, honest partial results when necessary, structured outputs, and final self-correction.Its detailed-solution section must contain only a step-by-step proof sufficient for expert verification, without commentary, alternatives, or failed attempts.Source: §3.1 · pp. 7–8

3.2 Verifier Prompt

• The verifier independently checks every solution step, classifies issues as Critical Errors or Justification Gaps, and reports verdicts with findings and a detailed log.Critical Errors invalidate dependent reasoning, whereas Justification Gaps are provisionally assumed while subsequent steps are still checked.Source: §3.2 · pp. 9–11

4.1 Performance on IMO 2025

• Hint-free solutions for IMO Problems 1 and 2 were obtained by removing only the hints, but at higher computational cost, indicating that hints mainly improve efficiency.The initial hints were mathematical induction for Problem 1 and analytic geometry for Problem 2.Source: §4.1 · p. 12
• Problem 6 defeated all three base models because a flawed claim that every tile lies entirely left or right of uncovered squares invalidated the lower-bound proof.The models correctly identified the trivial upper bound of 4048, but failed on the matching lower bound; this exposes a persistent hurdle in complex combinatorial reasoning.Source: §4.1 · p. 12
• 5 out of 6 IMO 2025 problems were solved rigorously with Gemini 2.5 Pro, Grok-4, or GPT-5, compared with best-of-32 baselines of 31.6%, 21.4%, and 38.1%, respectively.The full verbatim proofs supporting the 5 out of 6 result are provided in Appendix A.Source: §4.1 · p. 12
• The verifier-guided iterative refinement loop overcame finite reasoning budgets and gaps in initial drafts, converting latent model capabilities into more reliable mathematical proofs.The contrast with single-pass generation supports the pipeline’s central role in eliciting rigorous and trustworthy arguments.Source: §4.1 · pp. 12–13

4.2 Generalization to Undergraduate Mathematics

• The IMC evaluates complete proofs across algebra, analysis, geometry, and combinatorics, making its more advanced undergraduate scope a test of broader applicability.The competition has been held annually since 1994 and requires a more extensive knowledge base than the pre-university IMO.Source: §4.2 · p. 13
• 94.5% accuracy placed the Gemini agent at rank #3 among 434 IMC 2025 participants, versus 57.7% and rank #92 for base Gemini 2.5 Pro.This independent evaluation used the publicly released code and mitigated data-contamination concerns because the competition occurred afterward.Source: §4.2 · p. 13

Stronger base models

• Future integration of Gemini 2.5 Pro Deep Think, Grok-4 Heavy, and GPT-5 Pro requires API access and controllable web search for fair evaluation.These variants were excluded because none was available through an API and their interfaces could not disable web search, which could compromise evaluation on Internet-solvable problems.Source: §5 · pp. 13–14

Multi-model collaboration

• A multi-model framework could have models independently generate and verify outputs, then collectively critique them to synthesize each pipeline step [14].The proposed collaboration would combine diverse solution strategies and help detect errors or logical gaps missed by one model.Source: §5 · p. 14

Archival Note

• The archival progression began with Gemini 2.5 Pro solutions without hints for Problems 3–5 and general-hint solutions for Problems 1–2.The initial experiments appeared in arXiv versions 1 and 2.Source: Archival Note · p. 14
• Version 3 obtained hint-free Gemini solutions for Problems 1 and 2 by removing the hints alone, though at higher computational cost.The result confirmed that the pipeline could solve these problems from first principles without code changes.Source: Archival Note · p. 14
• Version 4 extends the pipeline to Grok-4 and GPT-5, generating hint-free solutions for Problems 1 through 5 across all three models.This expansion demonstrates the pipeline’s model-agnostic scope and motivated a corresponding title change.Source: Archival Note · p. 14
• Appendix A contains complete hint-free outputs from all three models, whereas Appendix B archives Gemini’s original hint-based solutions for Problems 1 and 2.The appendices preserve the evolution of the experiments in separate records.Source: Archival Note · p. 14

A Verbatim Model Outputs for IMO 2025 Problems (Hint-Free)

• The model outputs are reproduced verbatim, except for minor formatting corrections needed for TeX compilation; wording, mathematical steps, and logic remain unchanged.Corrections include adding missing TeX delimiters or replacing Unicode symbols with LaTeX equivalents.Source: A Verbatim Model Outputs for IMO 2025… · p. 18

A.1 Problem 1

• Problem 1 asks for all k for which n distinct lines cover the positive lattice triangle while exactly k lines are sunny.A sunny line is nonparallel to the x-axis, y-axis, and x + y = 0, with n ≥ 3.Source: §A.1 · p. 18

A.1.1 Solution by Gemini 2.5 Pro

• The proof establishes K_3 = {0, 1, 3}, proves a key structural lemma for n ≥ 4, and derives K_n = K_{n−1} by removing or adding a nonsunny boundary line.The preliminary covering lemma ensures the reverse construction yields distinct lines.Source: §A.1.1 · pp. 19, 21
• For every n ≥ 3, the solution concludes that the possible numbers of sunny lines are exactly K_n = {0, 1, 3}.This follows from establishing K_3 = {0, 1, 3} and proving K_n = K_{n−1} for n ≥ 4.Source: §A.1.1 · p. 21

A.1.2 Solution by Grok-4

• For n = 3, explicit coverings realize k = 0, k = 1, and k = 3, while exhaustive checks rule out k = 2.The k = 3 construction uses three sunny lines with slopes 1, −1/2, and −2.Source: §A.1.2 · pp. 21–22
• For n > 3, every n-line covering must contain a full boundary side, because each other line covers at most two boundary points while the boundary has 3n −3 points.Removing that non-sunny side leaves a covering of S_n−1, so induction preserves the number of sunny lines.Source: §A.1.2 · pp. 22–23
• The three values remain achievable recursively by removing full sides until reaching S_1 for k = 1 or S_3 for k = 3, while k = 0 uses only non-sunny lines.The recursive constructions use n −1 non-sunny lines for k = 0, n −1 full sides before S_1 for k = 1, and n −3 full sides before S_3 for k = 3.Source: §A.1.2 · p. 23
• For every n ≥ 3, the possible numbers of sunny lines are exactly k = 0, 1, and 3.The induction proves necessity and achievability of all three values.Source: §A.1.2 · pp. 21, 23

A.1.3 Solution by GPT-5

• The boundary lemma shows that any m ≥4 distinct lines covering Sm include one of the three boundary sides.Otherwise, the lines cover at most 2m boundary points, fewer than the 3m −3 boundary points when m ≥4.Source: §A.1.3 · p. 23
• Peeling boundary sides from any n-line cover leaves three lines covering a translate of S3 and guarantees at least n −3 non-sunny lines.Each removed boundary side is non-sunny, and translations preserve slopes and the sunny/non-sunny classification.Source: §A.1.3 · pp. 23–24
• On S3, no three-line cover has exactly two sunny lines, whereas covers exist with exactly 0, 1, and 3 sunny lines.Sunny lines through S3 contain at most two points, while the listed configurations realize the other three counts.Source: §A.1.3 · pp. 24–25
• For every n ≥3, the admissible numbers of sunny lines are exactly {0, 1, 3}, so k = 2 is impossible.The reduction to three lines and explicit constructions establish both impossibility and achievability.Source: §A.1.3 · p. 25
• The general constructions explicitly realize k = 0, 1, and 3 using n −3 vertical lines together with three final covering lines.The three cases cover the remaining columns and use respectively zero, one, or three sunny lines.Source: §A.1.3 · p. 25

A.2 Problem 2

• Problem 2 defines two intersecting circles Ω and Γ, points C, D, A, B, E, F, a circumcenter P, and the orthocenter H of triangle PMN.The centers M and N lie on the line through C and D, with C, M, N, D ordered consecutively.Source: §A.2 · p. 25
• The required conclusion in Problem 2 is that the line through H parallel to AP is tangent to the circumcircle of triangle BEF.This is the stated geometric claim to be proved.Source: §A.2 · p. 25

• The proof sets the line of centers MN as the x-axis and the radical axis AB as the perpendicular y-axis, with O at their intersection.It represents M and N as (m, 0) and (n, 0), while A and B are (0, a) and (0, −a).Source: §A.2.1 · p. 26
• The coordinate setup yields a^2 = r^2 − m^2 = R^2 − n^2 and places C and D at (m − r, 0) and (n + R, 0).These relations encode the two circle equations and the stated order C, M, N, D on the x-axis.Source: §A.2.1 · p. 26
• The proof computes P and H using perpendicular-bisector and altitude conditions, then proves PN ⟂ AD so the altitude from M is parallel to AD.This produces the coordinate relations needed to compare the line through H parallel to AP with the target circumcircle.Source: §A.2.1 · p. 26
• For the circumcircle of BEF, the proof derives coordinates for E and F and establishes identities for its center Oω, including xc + kAPyc = m + n − akAP.The center relations follow from perpendicular bisectors and equal distances to B and E.Source: §A.2.1 · pp. 26–27
• The final algebra gives T1 = rR/a and T1^2 = T2, so the line through H parallel to AP is tangent to the circumcircle of triangle BEF.The conclusion explicitly states that the tangency condition is satisfied.Source: §A.2.1 · pp. 27–28

Coordinate setup

• The coordinate setup places M and N on the x-axis, with intersections A and B symmetric about MN and points C and D ordered as C, M, N, D.The circles are centered at (0, 0) and (d, 0), with radii r and R satisfying |R − r| < d < R + r.Source: §A.2.2 · p. 28

Circumcenter and intersections

• The circumcenter P of △ACD has p = (d + R − r)/2 and y_p = −p(m + r)/h, yielding the slope s of AP.The proof then parameterizes the second intersections E and F of AP with the two circles.Source: §A.2.2 · p. 28

Algebraic lemmas

• The first lemma proves h(u + v) + suv = 0 by reducing its condition to E(p) = λQ(p) and showing Q(p) = 0 after substituting p.The cancellation verifies the algebraic relation needed for the subsequent perpendicular-bisector arguments.Source: §A.2.2 · p. 28
• Lemmas 2 and 3 show that the circumcenter of △BEF has x = d/2 and y-coordinate c_y = (d/2 − m)/s − h.Both conclusions follow by substituting the formulas for u and v into the perpendicular-bisector conditions.Source: §A.2.2 · pp. 28–29

Tangency conclusion

• The circumradius of △BEF equals the distance from O = (d/2, c_y) to the line through H parallel to AP, so that line is tangent to the circumcircle.Lemma 4 establishes the needed relation, while the final equalities give both quantities as |d/2 − m|(1 + s^2)/|s|.Source: §A.2.2 · p. 29

A.2.3 Proof by GPT-5

• The line through H parallel to AP is tangent to the circumcircle of triangle BEF, completing GPT-5’s proof.The proof establishes the circumcircle’s existence under the necessary and sufficient condition ax ≠ 0 before applying the tangency criterion.Source: §A.2.3 · pp. 30, 33

A.3.1 Solution by Gemini 2.5 Pro

• Gemini classifies the possible prime-support sets Sf as ∅, {2}, or the set of all primes.The classification yields f(n) = 1, f(n) = n, or the bound f(n) ≤ 2min(n, v2(n) + 2) for even n.Source: §A.3.1 · pp. 34–35
• For Problem 3, the smallest constant satisfying f(n) ≤ cn for every bonza function is c = 4.Gemini constructs a bonza function attaining f0(4)/4 = 4, proving sharpness.Source: §A.3.1 · p. 36

A.3.2 Solution by Grok-4

• Grok-4 derives f(n) ≤ 4n by bounding odd-prime valuations by vp(n) and the 2-adic valuation by v2(n) + 2.It then proposes a power-of-two-valued construction for the lower bound and begins verifying its bonza property.Source: §A.3.2 · pp. 37–38
• For odd b, LTE and separate treatment of b = 1 show v_2(b^(2d) − f(1)f(a)) meets the required bound.For odd b > 1, the minimum valuation is at least d + 2 when d ≥ 2 and at least 2 when d = 1.Source: §A.3.2 · p. 38
• For even b, comparing the valuations of b^(2d) and 2f(a) proves the bound when b is a power of 2 or is even but not a power of 2.In the mixed even case, the valuation is determined by the smaller exponent unless the exponents coincide, where the valuation is larger; all cases satisfy the target inequality.Source: §A.3.2 · p. 38
• c = 4 is the smallest constant, because f is bonza and achieves f(2^d)/2^d = 4 for d ≥ 2.The result follows after checking all cases for b.Source: §A.3.2 · p. 38

A.3.3 Solution by GPT-5

• The GPT-5 argument begins with f(1)=1, shows every prime divisor of f(n) divides n, and propagates divisibility from f(a) to f(b).These lemmas establish the prime-divisibility structure used in the later rigidity and dichotomy arguments.Source: §A.3.3 · pp. 38–39
• If an odd-prime value exists, then f is the identity; otherwise f(n)=1 for odd n, every f(n) is a power of 2, and f(n)≤2v2(n)+2.The dichotomy follows from infinitely many odd-prime values in the first branch and 2-adic restrictions in the complementary branch.Source: §A.3.3 · p. 40
• f(n) ≤4n for every bonza function, and the constant 4 is best possible.The construction F attains equality at n=2^s for every s≥2.Source: §A.3.3 · p. 41

A.4 Problem 4

• Problem 4 asks for all a1 in an infinite sequence where each term has at least three proper divisors and the next term sums its three largest proper divisors.For N with divisor count d(N)≥4, the three largest proper divisors correspond to N/d2, N/d3, and N/d4.Source: §A.4 · p. 41, §A.4.1 · pp. 41–42

A.4.1 Solution by Gemini 2.5 Pro

• Every term in an infinite valid sequence must be divisible by both 2 and 3; if a term is odd or not divisible by 3, the sequence eventually fails.Source: §A.4.1 · pp. 42–43
• When v2(N)=1, f(N)=N, so N is fixed; when v2(N)≥2, iteration follows as+1=(13/12)as, reaching v2=1 exactly when v2(a1) is odd.The cited proof verifies d(a1)≥4 in the fixed-point case and d(as+1)≥12≥4 for the transition term.Source: §A.4.1 · pp. 43–44
• The possible initial values are N=2^a3^bM with a,b≥1 and all prime factors of M at least 7, subject to one of two valuation conditions.Either a=1 and b≥1, or a is odd with a≥3 and b≥(a+1)/2, producing a fixed point after finitely many steps.Source: §A.4.1 · p. 44

A.4.2 Solution by Grok-4

• f(m) = m exactly for integers divisible by 6 but not by 4 or 5; f(m) > m only for integers divisible by 12 or divisible by 15 with v2(m) = 1, and f(m) < m otherwise.The fixed-point set is S, while the two increasing cases generate the possible backward chains into S.Source: §A.4.2 · pp. 44–45
• Every valid infinite sequence eventually reaches a fixed point in S and then remains there, because nontrivial cycles are impossible.Inputs whose orbit reaches numbers with fewer than three proper divisors are invalid, including 1, primes, and prime powers with exponent at most 2.Source: §A.4.2 · p. 46
• The valid chains are obtained by backward steps from f ∈ S: n = 2^(1+2j) · 3^(b+j) · 13^(c−j) · h for 0 ≤ j ≤ c, with b ≥ 1 and h having only prime factors at least 7.These chains remain divisible by 6, have at least three proper divisors, and increase forward to f.Source: §A.4.2 · pp. 46–47
• All possible a1 are positive integers divisible by 6 but not by 5, with odd positive v2(a1), positive v3(a1), and v2(a1) - 2v3(a1) a negative odd integer.All other prime factors are at least 7.Source: §A.4.2 · pp. 46–47

A.4.3 Solution by GPT-5

• For 6 divides N, f(N) equals 13N/12 when 4 divides N, 31N/30 when 4 does not divide N and 5 divides N, and N otherwise.Thus f(N) = N exactly when 4 does not divide N and 5 does not divide N.Source: §A.4.3 · p. 47
• Every term is divisible by 6 and no term is divisible by 5.The argument excludes odd terms and even terms coprime to 3, then rules out divisibility by 5.Source: §A.4.3 · pp. 48–49
• For any term, the update is either a fixed step a_{n+1} = a_n or a_{n+1} = (13/12)a_n, with the latter occurring precisely when 12 divides a_n.This follows from the divisor formula for multiples of 6, distinguishing divisibility by 4 and 5.Source: §A.4.3 · p. 49
• The sequence stabilizes after finitely many non-fixed steps at a fixed multiple of 6 divisible by neither 4 nor 5.Every non-fixed step multiplies the current term by 13/12, and only finitely many such steps can occur.Source: §A.4.3 · p. 49
• The initial value is valid if and only if a1 = 2^(2t+1)3^b m, with t ≥ 0, b ≥ t + 1, and gcd(m, 30) = 1.For such an initial value, exactly t transitions multiply by 13/12 before the sequence becomes constant.Source: §A.4.3 · p. 50

A.5 Problem 5

• Problem 5 defines an inekoalaty game parameterized by a positive real λ, with Alice choosing on odd turns and Bazza on even turns.Each player selects a nonnegative real number subject to the cumulative quadratic constraint, and all choices are publicly known.Source: §A.5 · p. 50
• The game ends when a player cannot choose a suitable number, giving the other player the win; if play continues forever, neither player wins.The problem asks to determine all λ for which Alice or Bazza has a winning strategy.Source: §A.5 · p. 50

Case 1: λ > √2

• For λ > √2, Alice wins by choosing a sufficiently large m, playing zero on earlier odd turns, and making Bazza’s next move impossible on turn 2m−1.The strategy succeeds against Bazza’s best defense, while Alice’s earlier zero moves remain valid.Source: §A.5.1 · p. 51

Case 2: λ < √2

• For λ < √2, Bazza wins by forcing Alice’s survival sums beyond her budget, so Alice eventually faces an impossible negative move.Alice’s best survival strategy is always playing x_{2k−1} = 0, but the smallest threshold-crossing turn makes her move invalid.Source: §A.5.1 · p. 52

Case 3: λ = √2

• When λ = √2, neither player has a winning strategy, and the game can continue indefinitely as a draw.Bazza cannot force Alice to win, Alice cannot force Bazza to win, and the strategies Alice plays zero while Bazza uses his balancing response provide an indefinite line of play.Source: §A.5.1 · pp. 52–53

Threshold characterization

• The solution proves that Bazza has a winning strategy below the threshold, Alice has one above it, and neither player has a winning strategy at equality.These conclusions are established separately for the two strict inequalities and the boundary case.Source: §A.5.2 · pp. 53, 55

Bazza’s winning regime

• Alice wins below the threshold by choosing zero on odd turns and then using a late odd move to force Bazza’s next constraint to be impossible.An induction bounds the maximum achievable even partial sum, enabling Alice to exceed the relevant threshold on a later odd turn.Source: §A.5.2 · pp. 53–54

Alice’s winning regime

• Above the threshold, Bazza’s greedy even-turn strategy keeps moving while Alice eventually faces a negative allowable move on an odd turn.The induction shows that deviations by Alice increase the relevant even partial sum, making her allowable odd move fail sooner.Source: §A.5.2 · pp. 54–55

Boundary case

• At equality, Alice’s zero choices and Bazza’s greedy responses both remain feasible forever, so the game continues indefinitely.The proof maintains the even- and odd-turn bounds needed for both players to keep moving.Source: §A.5.2 · p. 55

A.5.3 Solution by GPT-5

• For the game, Alice wins iff λ > 1/√2, Bazza wins iff λ < 1/√2, and λ = 1/√2 yields a draw.The strategies use Alice’s zero moves and a decisive odd move above the threshold, or Bazza’s even-turn response strategy below it.Source: §A.5.3 · p. 58

A.6 Problem 6

• Problem 6 asks for the minimum number of rectangular tiles covering a 2025 × 2025 grid so that every row and column has exactly one uncovered square.Tiles may have different sizes, must align with grid lines, and cannot overlap.Source: §A.6 · p. 58

A.6.1 Flawed Solution by Gemini 2.5 Pro

• Gemini 2.5 Pro’s solution claims every permutation of uncovered squares requires exactly 2N − 2 tiles, giving 4048 tiles when N = 2025.It partitions covered cells into left and right regions, proves each requires N − 1 tiles, and combines the two bounds.Source: §A.6.1 · p. 60

A.6.2 Flawed Solution by Grok-4

• Grok-4’s solution uses diagonal uncovered squares and separately tiles the two triangular regions with n − 1 rectangles each, claiming the lower bound 2(n − 1).Its lower-bound argument selects n − 1 near-diagonal squares in each triangle and shows no rectangle can contain two selected squares.Source: §A.6.2 · pp. 60–61

A.7 Flawed Solution by GPT-5

• GPT-5’s solution constructs 2n − 2 tiles around an anti-diagonal of holes and proposes a matching lower bound using 2n − 2 covered points forming a geometric fooling set.The construction covers every non-hole cell exactly once, while the lower-bound argument asserts every pair of selected points has a bounding box containing a hole.Source: §A.7 · pp. 61–62
• Each tile contains at most one element of S because any tile containing two elements would contain their bounding box, including a hole.The argument checks three cases for pairs of elements in S and shows that every corresponding bounding box contains a hole.Source: §A.7 · pp. 62–63
• t ≥ 2n − 2 because S contains 2n − 2 distinct covered cells and each tile contains at most one of them.This establishes the lower bound used in the final equality.Source: §A.7 · p. 63
• t = 2n − 2 follows by combining the bounds t ≤ 2n − 2 and t ≥ 2n − 2.The passage states this conclusion for the solution, but the subsequent numerical specialization is truncated.Source: §A.7 · p. 63

B Hint-Based Solutions from Initial Experiments

• Gemini 2.5 Pro was prompted to solve Problem 1 by induction and Problem 2 by analytic geometry.These hint-based prompts define the initial-experiment solutions summarized here.Source: §B.1 · p. 63, §B.2 · p. 66

B.1 Solution to Problem 1 by Gemini 2.5 Pro

• For Problem 1, the configuration asks which k allow n distinct lines covering S_n with exactly k sunny lines.A sunny line has slope different from 0, ∞, and −1.Source: §B.1 · p. 63
• The reduction repeatedly removes principal boundary lines while preserving the number of sunny lines, eventually forcing every remaining line to be sunny.The core problem becomes covering S_k with k distinct sunny lines without principal boundary lines.Source: §B.1 · pp. 63–64
• For every n ≥3, the possible numbers of sunny lines are exactly {0, 1, 3}.Explicit constructions establish k = 0, 1, and 3, while the permutation argument excludes k = 2 and all k ≥4.Source: §B.1 · pp. 65–66

B.2 Solution to Problem 2 by Gemini 2.5 Pro

• For Problem 2, the analytic setup places the common chord on the y-axis, the line of centers on the x-axis, and the circle intersections at A(0, a) and B(0, −a).The circle centers are M(m, 0) and N(n, 0), with C, M, N, D ordered on the x-axis.Source: §B.2 · p. 66
• The geometric preliminaries establish c + d ≠ 0 and a^2 + cd < 0 under the radius and ordering conditions.These inequalities support the subsequent coordinate calculations for the circumcenter P and orthocenter H.Source: §B.2 · p. 66
• The solution computes P, H, the intersections E and F, and the circumcircle of triangle BEF using coordinates and auxiliary algebraic identities.The circumcenter K and radius are then expressed in terms of a, c, and d.Source: §B.2 · pp. 66–68
• The line through H parallel to AP is tangent to the circumcircle of triangle BEF because its squared distance from the circle’s center equals the squared radius.The proof concludes by verifying equality of the tangency condition’s two sides.Source: §B.2 · p. 68