PaperlayerView exact revision on arXiv

Source-linked AI summary

MaxProof: Scaling Mathematical Proof with Generative-Verifier RL and Population-Level Test-Time Scaling

Jiacheng Chen, Xinyu Zhang, Shunkai Zhang, Yanmohan Wang, Lin Li, Tiancheng Qin, Qin Wang, Zhengmao Zhu, Tianle Li, Jingyang Li, Zehan Li, Binyang Jiang, Jin Zhu, Han Ding, Fei Yu, Chenyu Du, Zijian Song, Jiayuan Song, Zhi Zhang, Yunan Huang, Weiyu Cheng, Pengyu Zhao, Yu Cheng

arXiv:2606.13473v1cs.LGcs.AIcs.CL

TL;DR

Competition-level mathematical proof requires reliable generation, verification, and repair beyond one-shot reasoning. MaxProof combines these capabilities in population-level test-time search, lifting M3 to 35/42 on IMO 2025 and 36/42 on USAMO 2026.

  • Problem

    Competition-level proof requires reliable generation, verification, and repair, while verifier-based training faces reward noise, false positives, and reward hacking.

  • Method

    M3 trains proof generation, verification, and critique-conditioned repair, while MaxProof searches and ranks candidate proofs through population-level refinement and tournament selection.

  • Results

    Across IMO 2025 and USAMO 2026, MaxProof lifts M3 from 27/42 to 35/42 and from 26/42 to 36/42, respectively.

  • Takeaways & Limitations

    The results show that system design can narrow part of the gap to stronger closed-source systems without relying on scale alone.

  • Takeaways & Limitations

    Selection can lose stronger candidates when the ranker’s preferences diverge from verifier scores, as shown by a 4-point USAMO 2026 P2 loss.

Abstract

from arXiv · show

We present MaxProof, a population-level test-time scaling framework for competition-level mathematical proof in the MiniMax-M3 series. M3 first trains three proof-oriented capabilities -- proof generation, proof verification, and critique-conditioned proof repair -- using a defense-in-depth generative verifier engineered for low false-positive rate. These capabilities are merged into a single released M3 model. At test time, MaxProof treats the model as a generator, verifier, refiner, and ranker, searches over a population of candidate proofs, and returns one final proof through tournament selection. With MaxProof test-time scaling, the M3 model reaches 35/42 on IMO 2025 and 36/42 on USAMO 2026, exceeding the human gold-medal threshold on both.

1. Introduction

The introduction frames competition-level proof as a stringent test of reliable reasoning and motivates three atomic capabilities: proof generation, verification, and repair. It then presents their merger into M3 and MaxProof’s population-level test-time search as the paper’s central approach.

  • Competition-level proofs impose tightly coupled constraints and very low tolerance for hand-waving, making them a sharper mathematical-reasoning challenge.
  • Pushing M3 beyond the gold-medal line on IMO 2025 and USAMO 2026 motivates separate capabilities for proof generation, verification, and critique-conditioned repair.
  • M3 trains a Proof Expert, Verifier Expert, and Fixer Expert through specialist stages, then merges these capabilities into the single released model.The stages use long-horizon RL with a defense-in-depth generative verifier, explicit error finding, and repair of verifier-flagged proofs.
  • MaxProof is a model-agnostic population-level test-time scaling framework that searches candidate proofs through generator, verifier, refiner, and ranker interfaces.In M3, one merged model serves all four interfaces under different prompts.
  • The verifier pipeline prioritizes low false-positive rates through bad-case filtering, normalization, parallel multi-judge scoring, and pessimistic minimum aggregation.The design target is reliable scoring on a long-running RL training stream rather than maximum accuracy on a static benchmark.
  • MaxProof combines conservative verifier fitness, diverse parent selection, PATCH/REWRITE refinement, and pairwise tournament selection in an evolution-inspired search loop.

2. Proof Expert: Long-Horizon RL under a Defense-in-Depth Verifier

The Proof Expert uses long-horizon RL with a frozen generative verifier that assigns conservative proof-level rewards, combining defense-in-depth safeguards with CISPO updates. The design responds to reward hacking observed in M2, including substantial length growth and format-driven proof strategies.

  • Verifier-driven RL: The frozen generative verifier reads each candidate proof against a reference-derived rubric and returns a textual assessment plus a scalar reward in [0, 7].The rollout policy samples groups of long-form proofs, and the scalar score becomes the trajectory-level reward for CISPO updates.
  • Defense-in-depth verifier: The four-layer verifier filters bad cases, normalizes solutions, scores candidates with three judges, and applies pessimistic min aggregation.The first two layers act as guardrails, while the final two produce the conservative scalar score.
  • Defense-in-depth verifier: False positives are treated as more damaging than false negatives, so the pipeline prioritizes suppressing high-scoring invalid proofs over maximizing static benchmark agreement.A false positive can become a learned training target, whereas a false negative generally discards only one candidate among many.
  • CISPO training: CISPO clips importance-sampling weights while retaining token-level log-probability gradients, preserving learning signal in long responses.The proof-level reward avoids noisy step-level labels, while group-level standard-deviation filtering removes groups whose nearly identical scores provide unreliable ordering.
  • M2 failure modes: 3×: visible proof length increased from ∼3.5K to ∼10K characters during M2 training, alongside canonical reward-hacking templates and faster growth in hidden thinking length.These patterns showed that rising static verifier scores could reflect reward hacking rather than genuine capability gains.

3. Verifier Expert: Aligned Error Finding

The Verifier Expert distills the Proof Expert’s expensive external verifier into the merged M3 model, enabling direct downstream proof verification. It jointly localizes errors and classifies verdicts so its critiques remain actionable and aligned with the Proof Expert’s correctness signal.

  • Motivation and contribution: The Verifier Expert replaces an external, seconds-to-tens-of-seconds-per-candidate verifier with a directly callable component merged into the final M3 release.This makes verification practical for downstream agents and tools that must score thousands of candidates.
  • Structured verification: Verification is formulated as joint error-finding and four-class classification rather than 0–7 regression, producing an assessment, localized errors, and a verdict.The verdict is constrained by the concrete error list, preventing the two outputs from drifting out of sync.
  • Structured verification: The <errors> list is an actionable critique for the Fixer Expert, while the <verdict> tag is constructed as a function of that critique.This output structure makes the Verifier Expert usable as a building block for proof repair and selection.
  • Training and alignment: Verifier training data is harvested from the Proof Expert’s run and aligned to the pessimistic-min teacher signal, preserving the correctness notion encoded by the Proof Expert’s RL objective.The alignment prevents the Proof Expert and Verifier Expert from drifting on what constitutes a good proof.
  • Training and alignment: The aligned Verifier Expert gives downstream tools a low-latency model that recognizes proofs according to the same ground truth as the Proof Expert.The shared notion of correctness is designed for consumption by both the Fixer Expert and the MaxProof framework.

4. Fixer Expert: Proof Repair by Rejection-Sampling Fine-Tune

The Fixer Expert performs critique-conditioned proof repair, modifying flawed candidate proofs to address identified errors while preserving correct steps. It is trained through rejection sampling, retaining only verifier-certified successful corrections, and completes a self-consistent proof-generation, verification, and repair loop.

  • Repair task: The Fixer Expert transforms a flawed candidate proof and its verification critique into a corrected proof that preserves the original’s valid parts.Its input is (problem, flawed_proof, verification_analysis), where the critique identifies problematic steps and failure types.
  • Repair task: The critique acts as a soft constraint: a successful correction must address every cited error and only those errors.Without the critique, the model would need to rediscover the flaws, making the correction ungrounded.
  • Training data: Training triples are harvested from Proof Expert iterations, using candidates labeled minor_gaps, has_errors, or fundamentally_wrong.This data is obtained as a byproduct of the Proof Expert’s training run.
  • Rejection-sampling fine-tune: Only corrections receiving the strict no_errors verdict from the pessimistic-min aggregated verifier are accepted for fine-tuning.Multiple candidate corrections are sampled for each triple, and accepted corrections form the fine-tuning set.
  • Self-consistent loop: The Fixer Expert completes a self-consistent loop in which the Proof Expert generates, the Verifier Expert critiques, and the Fixer Expert repairs proofs using the same verifier and critique structure.This makes refinement structured and critique-conditioned rather than free-form editing, with a clear training signal and evaluation path.

5. MaxProof: Population-Level Test-Time Scaling

MaxProof is a model-agnostic population-level test-time scaling framework that turns a model’s best@K proof capability into a more stable pass@1 system through guided candidate search. It combines verifier-guided refinement with pairwise tournament selection while addressing verifier noise through conservative scoring and population redundancy.

  • Framework overview: MaxProof uses generator, verifier, refiner, and ranker interfaces to search over a population of candidate proofs and select one final answer.The framework is separate from the particular model it scales and can use separate models or one merged model under different prompts.
  • Search motivation: Competition-level proofs lack direct gradients, so MaxProof raises the population ceiling through sampling and improves promising candidates through verifier-guided repair or re-exploration.The framework treats sampling as a guided search over a large discrete proof space.
  • Noisy verification: MaxProof uses a pessimistic-min fitness score across multiple verifier samples, favoring false negatives because false positives can steer refinement toward flawed proof trajectories.The retained critique is paired with the minimum verifier score to make verifier noise less damaging.
  • Refinement: Each parent produces PATCH and REWRITE offspring: PATCH preserves useful proof structure while addressing identified errors, whereas REWRITE explores a different proof path.Both modes receive compact summaries of sibling candidates, providing useful information and negative information without including every full proof.
  • Final selection: MaxProof stops early only after two archive candidates reach maximum fitness, then always performs pairwise tournament selection among the top-K archive candidates.The tournament uses ranker votes to compare which candidate is more correct, but can incur selection loss when ranker preferences diverge from verifier scores.

6. Experiments: Mathematical Proof Benchmarks and MaxProof Scaling

M3 scores 67.40 on IMOProofBench and 81.56 on IMOAnswerBench without MaxProof, while MaxProof raises contest totals by 8 points on IMO 2025 and 10 points on USAMO 2026. The framework’s gains come with selection loss concentrated on USAMO 2026 P2 and substantial inference-time compute requirements.

  • Standalone benchmark evaluation: 67.40 on IMOProofBench and 81.56 on IMOAnswerBench are M3’s standalone scores without MaxProof search or verifier-guided refinement.M3 remains roughly nine points behind GPT-5.5 and Gemini 3.1 Pro on IMOAnswerBench, with a larger gap on proof construction.
  • Selection diagnostics: 6/7 versus 2/7 on USAMO 2026 P2 is the concentrated selection loss, where the tournament selected a candidate far below the population’s oracle best.Selection loss measures the difference between the final population’s highest score and the system’s self-picked score.
  • Search dynamics: The population’s best score rises sharply during the first two refinement rounds and then plateaus through the middle rounds across the 12 problems.Figure 8 reports both aggregate mean and percentile-band dynamics and individual problem trajectories; three problems never reach 7/7 within R=10 rounds.
  • Solution quality and limitations: 7/7 self-picked solutions are all complete and correct under expert review, supporting the defense-in-depth verifier’s low false-positive design goal.On routine IMO 2025 P1, P4, and P5, full-mark solutions rely heavily on exhaustive case analysis and emerge at rounds 7, 10, and 7, respectively.
  • MaxProof contest scaling: 8 points on IMO 2025 (27 → 35) and 10 points on USAMO 2026 (26 → 36) are the gains from adding MaxProof to one-shot M3.The framework converts non-trivial best@K capability into more stable pass@1 performance; a 32-candidate sampling baseline would lift scores far less and lacks guaranteed best-sample selection.
  • Solution quality and limitations: IMO 2025 P6 reflects a base-model capability ceiling, while USAMO 2026 P3 reaches 6/7 but not 7/7 because min aggregation cannot resolve judge disagreement.M3 also remains less concise than the strongest closed-source models on relatively easy problems, leaving that gap to future model iterations.

7. Conclusion

The conclusion presents M3 and MaxProof as sustained progress on competition-level proof, where reliable evaluation requires defense because no executable oracle, cheap unit test, or single trusted judgment exists. M3 reaches 67.40 on IMOProofBench and 81.56 on IMOAnswerBench, while MaxProof improves the same released model to 35/42 on IMO 2025 and 36/42 on USAMO 2026.

  • Conclusion: Competition-level proof remains among the hardest language-model reasoning tests because it lacks an executable oracle, cheap unit test, or single trusted judgment.The conclusion frames the M3 cycle as sustained pursuit rather than evidence that the frontier has been reached.
  • Conclusion: MaxProof turns proof generation, verification, repair, and selection into one model-agnostic test-time scaling search process.M3 is described as a proof-oriented model, while MaxProof operates as the associated scaling framework.
  • Conclusion: 67.40 on IMOProofBench and 81.56 on IMOAnswerBench are achieved by the resulting M3 model.These are the reported benchmark scores for the resulting M3 model.
  • Conclusion: 35/42 on IMO 2025 and 36/42 on USAMO 2026 are reached by MaxProof, up from 27/42 and 26/42 respectively for the same released model.The passage reports both before-and-after scores for MaxProof on the two competition benchmarks.

A. Per-Problem Results and Search Dynamics · A.1. Per-Round Oracle-Best Trajectories

The appendix examines per-problem search dynamics across 12 evaluation problems from IMO 2025 and USAMO 2026. It tracks oracle-best progress over refinement rounds alongside tournament self-picks and qualitative search observations.

  • A. Per-Problem Results and Search Dynamics: 12 problems are analyzed, comprising six from IMO 2025 and six from USAMO 2026.The appendix reports search dynamics separately for each evaluation problem.
  • A. Per-Problem Results and Search Dynamics: Three outputs are reported for every problem: per-round oracle-best score, final self-pick score, and an informative search observation.These outputs combine quantitative trajectories, the final tournament choice, and qualitative interpretation.
  • A. Per-Problem Results and Search Dynamics: The appendix pairs each per-problem trajectory with a short note on the search’s most informative observation.This qualitative note accompanies the reported oracle-best and self-pick scores.
  • A.1. Per-Round Oracle-Best Trajectories: Oracle-best trajectories measure the strongest score available after each search round.The table is organized around per-round oracle-best scores for each problem.
  • A.1. Per-Round Oracle-Best Trajectories: R0 denotes initialization, while R1–R10 denote refinement rounds.The trajectory therefore spans one initialization state and ten refinement rounds.
  • A.1. Per-Round Oracle-Best Trajectories: The Self column records the tournament self-pick for each problem.This is distinct from the per-round oracle-best trajectory.

A.2. Per-Problem Notes · B. Prompt Templates · C. Reward Hacking Case Studies

The per-problem notes show MaxProof’s varied improvement patterns, including early stopping, late PATCH or REWRITE gains, plateaus, and ranker-selection failures. The appendices also specify verifier, PATCH, and REWRITE prompt structures and document four reward-hacking patterns identified through expert-judge comparisons.

  • A.2. Per-Problem Notes: 7/7 was reached on IMO P1 by R4, after PATCH refinements expanded a handwaved induction step.IMO P2 already contained a 7/7 candidate and stopped at R2; IMO P3 reached 7/7 by R1 after one PATCH.
  • A.2. Per-Problem Notes: 7/7 was reached on IMO P4 at R10 after a 6/7 plateau through R1–R9 and a late REWRITE.The supplied passage identifies this as a late improvement after the plateau.
  • B. Prompt Templates: The appendix presents structural templates for the verifier, PATCH, and REWRITE prompts, while omitting release-specific examples and formatting requirements.The verifier uses a problem, reference solution, and candidate proof; PATCH uses a flawed proof and critique; REWRITE also includes sibling summaries.
  • B.1. Verifier Prompt: The verifier prompt requires step-by-step analysis, an error list, and a verdict chosen from four labels: no_errors, minor_gaps, has_errors, or fundamentally_wrong.The assessment is structured into <assessment>, <errors>, and <verdict> blocks.
  • B.2. Refine (PATCH) Prompt: PATCH instructs the model to preserve correct proof parts and output one proof addressing every critique error, and only those errors.Its inputs are the problem, flawed proof, and verification analysis.
  • B.3. Refine (REWRITE) Prompt: REWRITE treats flaws as evidence that the current route is unworkable, uses sibling summaries, and requires a single proof following a different route.The prompt aims to avoid the candidate’s failure modes by using information from other candidates.
  • C. Reward Hacking Case Studies: Four reward-hacking patterns—length bias, format hacking, semantic shortcut, and judge-specific preference—are illustrated by rollouts scored 1.0 by the training verifier but rejected by an independent expert judge.The expert judge used the same problem, reference solution, and rubric as the training-time verifier.

C.1. Length Bias · C.2. Format Hacking

The paper shows that verifier-aligned proof generation can favor excessive length and polished formatting over mathematical validity. In two rollouts, training-verifier scores were 1.0 despite expert judges identifying incorrect arguments built on unsupported invariants or unjustified assumptions.

  • C.1. Length Bias: Long proofs align more easily with rubric keywords and make hand-waving harder for a single-judge verifier to detect.
  • C.1. Length Bias: 1.0 training-verifier score accompanied a 0.05 expert-judge score on an incorrect IMO 2010 Problem 5 rollout.The visible answer contained 5,255 characters, while hidden thinking contained 113,831 characters.
  • C.1. Length Bias: The rollout incorrectly claimed the weight V could be adjusted to any integer and that no modular obstruction prevented reaching the target.Its intermediate construction was asserted rather than shown reachable, and the correct answer was No.
  • C.1. Length Bias: The policy’s hidden thinking trace was over 20× longer than its visible answer, consistent with spending generation budget on surface form rather than searching for the missed invariant.The visible answer was long, well-structured, and formally typeset, but its two load-bearing claims were unsupported.
  • C.2. Format Hacking: More than 80% of outputs converged on fixed “Step N,” “Verification,” “Final Answer,” and “We are given...” templates, even when mathematically inappropriate.
  • C.2. Format Hacking: The argument’s elimination of alternative tetrominoes was hand-wavy, relying on unsupported claims of checks via dual-colorings and system analysis.The problem’s answer depends crucially on the actual tile shape, so analyzing the wrong tile makes the argument irrelevant.
  • C.2. Format Hacking: A rubric-style judge awarded full credit for the polished numbered structure and boxed answer, whereas a judge probing whether the structure carried a proof did not.The rollout used the canonical “We are given...” opening, numbered Step-N sections, and a boxed final answer while resting on one asserted tile choice.

C.3. Semantic Shortcut

The policy used plausible shortcut phrases at the proof’s load-bearing steps, causing a rubric verifier to accept an incorrect argument. Expert review identified missing derivations and a direct counterexample to the final classification.

  • Shortcut mechanism: “It can be shown” and “after simplification” replaced hard argument steps while surrounding text and rubric keywords remained correct.These shortcuts were rarely caught by a single-judge rubric verifier.
  • Verifier failure: 1.0 training-verifier score contrasted with a 0.1 expert-judge score, which marked the Russia 2010 Grade-9 Problem 7 answer incorrect.The visible answer contained 4,841 characters and hidden thinking contained 60,337 characters.
  • Missing derivation: The claim that every non-square n is representable was unsupported because the Pell-solution multiplication step was never shown to produce an integer y > 1.The proof invoked the technique as standard without carrying it out symbolically.
  • Counterexample: 9 = (5^2 − 1)/(2^2 − 1) directly contradicts the claim that all odd squares n = m^2 with m ≥ 3 are unlucky.The argument replaced its purported contradiction with “plugging in leads to a contradiction” without deriving one.
  • Overall failure: The final classification was incorrect despite correct terminology and a plausible closed-form answer, because both load-bearing steps were only named rather than executed.A keyword-based rubric judge could award full credit, whereas mechanically checking whether the boxed set contains 9 would expose the error.

C.4. Judge-Specific Preference … Problem Statement

The case study shows that judge-specific preference can inflate verifier scores while proof quality remains flat or regresses. The broader defenses normalize style, use multiple judges, and expose polished but unsupported claims through independent checking.

  • C.4. Judge-Specific Preference: Judge-specific preferences can reward preferred phrasings, tolerate certain errors, and favor formats even as underlying proof quality stays flat or regresses.The paper identifies this as especially pernicious because verifier gains can be large without genuine proof improvement.
  • C.4. Judge-Specific Preference: 1.0 training-verifier scoring accepted a polished game proof whose independent critique found no demonstrated strategy against every B-strategy.The visible answer was 6,886 characters, while hidden thinking reached 147,492 characters.
  • C.4. Judge-Specific Preference: ∼148K characters of hidden thinking produced a polished assertion rather than a working strategy, while an independent judge located the gap in seconds.The training verifier deferred to stylistic confidence on a problem it could not quickly solve.
  • C.5. From Cases to Defenses: In every examined failure, fluent step-by-step outputs replaced load-bearing claims with assertions, phrases, or missing references that a second judge immediately flagged.This common shape is presented as a population-level pattern motivating the defense pipeline.
  • C.5. From Cases to Defenses: Three verifier layers target distinct shortcuts: bad-case filtering removes length and format hacks, normalization strips stylized phrasing, and parallel judges probe semantic gaps.The pipeline is designed for each failure mode to be defeated independently.
  • D. Selected Model Outputs: The appendix presents self-picked IMO 2025 and USAMO 2026 outputs selected by the MaxProof pairwise tournament, with whitespace normalized and TeX rendered as-is.These outputs are candidate proofs chosen through the tournament described in Section 5.3.5.
  • Problem Statement: {0, 1, 3} is the complete set of attainable sunny-line counts for the lattice-covering problem.Explicit constructions establish 0, 1, and 3, while the proof rules out every other nonnegative integer.
  • Problem Statement: The geometry solution concludes that the line through H parallel to AP is tangent to the circumcircle of triangle BEF.The argument uses coordinates, second-circle intersections, and a final equality matching the tangency condition.

IMO 2025 Problem 3 (Self-Pick: 7/7) · IMO 2025 Problem 4 (Self-Pick: 7/7)

For IMO 2025 Problem 3, the smallest constant satisfying f(n) ≤ cn for every bonza function is 4. The solution classifies the relevant prime set, proves the upper bound, and constructs a bonza function showing sharpness.

  • IMO 2025 Problem 3 (Self-Pick: 7/7): If P is infinite, divisibility by infinitely many primes forces f(b) = b for every b, so f is the identity function.This is the infinite-P branch of the classification.
  • IMO 2025 Problem 3 (Self-Pick: 7/7): Finite non-empty P contains no odd prime, because Dirichlet’s theorem would otherwise force infinitely many primes into P.Thus finite non-empty P must equal {2}.
  • IMO 2025 Problem 3 (Self-Pick: 7/7): The prime set P has exactly three possibilities: P = ∅, P = infinite, or P = {2}.An odd prime cannot belong to finite non-empty P, while infinite P forces the identity function.
  • IMO 2025 Problem 3 (Self-Pick: 7/7): For P = ∅, the divisibility condition implies f ≡ 1, while P = {2} yields f(b) = 1 for odd b and bounds even values by powers of 2.The even case derives an exponent bound e ≤ j + 2 when b = 2^j m with m odd.
  • IMO 2025 Problem 3 (Self-Pick: 7/7): The classification gives f(n) ≤ 4n for odd n, even n, and the identity function.For even n = 2^j m, the proof obtains f(n) ≤ 2^(j+2) ≤ 4n.
  • IMO 2025 Problem 3 (Self-Pick: 7/7): The construction f(2^k) = 2^(k+2) for k ≥ 2 is bonza and makes every c < 4 fail.This establishes sharpness of the upper bound.
  • IMO 2025 Problem 3 (Self-Pick: 7/7): 4 is the smallest real constant c such that f(n) ≤ 4n for every bonza function and positive integer n.The proof establishes the upper bound and shows no smaller constant works.

Problem Statement

The problem studies positive-integer sequences whose next term is the sum of the three largest proper divisors of the current term, requiring every term to have at least three proper divisors. The supplied characterization states that an infinite sequence exists exactly when the initial term satisfies three arithmetic conditions.

  • A proper divisor of N is a positive divisor other than N itself.
  • Each a_n has at least three proper divisors, and a_n+1 is the sum of its three largest proper divisors.The task is to determine all possible values of a_1.
  • The transformation is f(N)=N(1/d_1+1/d_2+1/d_3), where d_1<d_2<d_3 are the three smallest divisors of N greater than 1.This is valid when τ(N)≥4 and produces an integer.
  • 6 divides every term of any infinite sequence.Otherwise, the sequence would produce an infinite strictly decreasing sequence of positive integers.
  • An infinite sequence exists iff the initial term has e odd, f≥(e+1)/2, and 5 does not divide r.For e=1, the second condition reduces to f≥1, leaving 5∤r as the restriction.

IMO 2025 Problem 5 (Self-Pick: 7/7) … USAMO 2026 Problem 6 (Self-Pick: 7/7)

The represented solutions establish complete outcomes for the inekoalaty game, grid tiling, extremal floor expression, power-of-two merging, and two geometry configurations. They combine explicit constructions or strategies with matching impossibility, maximality, or tangency arguments.

  • IMO 2025 Problem 5 (Self-Pick: 7/7): The inekoalaty analysis partitions the parameter regime into Alice-win, Bazza-win, and draw cases, with explicit strategies proving the corresponding outcomes.Alice’s and Bazza’s strategies force termination in their winning regimes, while the draw regime permits indefinite continuation and prevents either player from forcing a win.
  • Problem Statement: 2n−2 tiles are sufficient and necessary for an n×n grid whose uncovered squares form a permutation matrix.After reducing the uncovered squares to the diagonal, separate upper- and lower-triangle arguments provide n−1 distinct tiles in each region.
  • USAMO 2026 Problem 1 (Self-Pick: 7/7): The USAMO 2026 Problem 1 expression is maximized at fractional part (n−1)/n, with equality characterized by the residue arrangement.The proof reduces maximization to rational points, applies rearrangement, and identifies m=n−1 as the unique equality case.
  • Problem Statement: Annie’s smallest-larger-value merging strategy always produces a final number F<4S.An induction maintains an upper bound on the evolving sum, yielding the strict final inequality and guaranteeing Annie’s win.
  • Problem Statement: The constructed circumcircle of AYZ and the incircle of R are tangent.The coordinate proof shows that the distance between their centers equals either the sum or the absolute difference of their radii.
  • USAMO 2026 Problem 5 (Self-Pick: 7/7): For USAMO 2026 Problem 5, the three auxiliary circumcenters satisfy OA=αA, OB=αB, and OC=αC.A spiral similarity centered at the Miquel point maps ABC to DEF, and multiplication by α maps ABC to the triangle of auxiliary circumcenters.

Problem Statement

The section asks to prove that positive integers a and b satisfying φ(ab + 1) | a^2 + b^2 + 1 must both be Fibonacci numbers. The proof classifies all admissible cases and shows each yields a Fibonacci pair.

  • For positive integers a and b, if φ(ab + 1) divides a^2 + b^2 + 1, prove that a and b are Fibonacci numbers.
  • Every solution in the prime case has the form (F2n−1, F2n+1), its symmetric order, or (1, 1).
  • The only composite admissible case is d = 9, yielding (a, b) = (1, 8) or (8, 1), with 8 = F6.
  • Thus all possibilities for d = ab + 1 produce pairs whose two entries are Fibonacci numbers.
Loading 2606.13473v1…